bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c


--------------------------------------------------------------------------------


5.0.0-KLEE:86e6f6f8-dg:03407af1-symbiotic:a8aa8ad6-minisat:3db58943-stp:17249213-sbt-instrumentation:dd7e4312
INFO: After compilation stats: Globals/Functions/Blocks/Instr.: 99 99 1153 7148
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.299271821976
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'tty_wakeup' (function is undefined)
Removed calls to 'tty_kref_put' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function tty_port_tty_get as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function mod_timer as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'tty_port_init' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'tty_unregister_device' (function is undefined)
Removed calls to 'tty_port_destroy' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function dev_err as symbolic
Defining function _dev_info as symbolic
Defining function pci_request_region as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'tty_hangup' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'do_SAK' (function is undefined)
Removed calls to 'tty_flip_buffer_push' (function is undefined)
Defining function tty_port_register_device as symbolic
Defining function request_firmware as symbolic
Defining function dev_warn as symbolic
Defining function request_threaded_irq as symbolic
Defining function printk as symbolic
Defining function tty_prepare_flip_string as symbolic
Defining function tty_insert_flip_string_flags as symbolic
Removed calls to 'tty_port_close' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'tty_port_hangup' (function is undefined)
Defining function capable as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function tty_port_open as symbolic
Removed calls to 'tty_port_free_xmit_buf' (function is undefined)
Defining function tty_port_alloc_xmit_buf as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'put_tty_driver' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'tty_set_operations' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_disconnect_3 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_setup_3 as symbolic
Defining function ldv_destruct_2 as symbolic
Defining function tty_register_driver as symbolic
Defining function __pci_register_driver as symbolic
Defining function tty_unregister_driver as symbolic
Defining function __tty_alloc_driver as symbolic
Defining function del_timer_sync as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_uchar_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.363523006439
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 157 101 597 4205
INFO: Starting verification
KLEE: WARNING ONCE: function "isicom_tx" has inline asm
KLEE: WARNING ONCE: function "isicom_probe" has inline asm
KLEE: WARNING ONCE: function "isicom_interrupt" has inline asm
KLEE: WARNING ONCE: function "WaitTillCardIsFree" has inline asm
KLEE: WARNING ONCE: function "isicom_throttle" has inline asm
KLEE: WARNING ONCE: function "isicom_unthrottle" has inline asm
KLEE: WARNING ONCE: function "isicom_send_break" has inline asm
KLEE: WARNING ONCE: function "isicom_tiocmset" has inline asm
KLEE: WARNING ONCE: function "raise_dtr" has inline asm
KLEE: WARNING ONCE: function "drop_dtr" has inline asm
KLEE: WARNING ONCE: function "lock_card" has inline asm
KLEE: WARNING ONCE: function "isicom_config_port" has inline asm
KLEE: WARNING ONCE: function "isicom_dtr_rts" has inline asm
KLEE: WARNING ONCE: function "isicom_shutdown" has inline asm
KLEE: WARNING ONCE: function "isicom_activate" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: Type for boot_tvec_bases is not sized
KLEE: WARNING: Unable to find size for global variable: boot_tvec_bases (use will result in out of bounds access)
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_d05ddbde-fa62-4182-af96-e7b0341d6317/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6210: memory error: object read only
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: flushing 71168 bytes on read, may be slow and/or crash: MO50[71168] allocated at global:isi_ports
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6210: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6211: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6212: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6213: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6214: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xXLp7S/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--tty--isicom.ko-entry_point_true-unreach-call.cil.out.c:6217: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
