bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--sbe-2t3e3--sbe-2t3e3.ko-main.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.: 114 234 1487 10292
INFO: Compilation, preparation and instrumentation time: 0.489289999008
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Defining function del_timer as symbolic
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'unregister_hdlc_device' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'dev_kfree_skb_any' (function is undefined)
Defining function dev_set_drvdata as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function dev_get_drvdata as symbolic
Defining function pci_get_subsys as symbolic
Defining function dev_err as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function alloc_hdlcdev as symbolic
Defining function printk as symbolic
Defining function netdev_warn as symbolic
Defining function request_threaded_irq as symbolic
Defining function dev_warn as symbolic
Defining function _dev_info as symbolic
Defining function skb_put as symbolic
Defining function netif_rx as symbolic
Defining function __phys_addr as symbolic
Defining function __netdev_alloc_skb as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__netif_schedule' (function is undefined)
Defining function netpoll_trap as symbolic
Defining function pci_bus_read_config_byte as symbolic
Defining function pci_bus_write_config_dword as symbolic
Defining function pci_bus_read_config_dword as symbolic
Defining function register_netdev as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function __pci_register_driver as symbolic
Removed calls to 'hdlc_close' (function is undefined)
Removed calls to 'module_put' (function is undefined)
Removed calls to 'might_fault' (function is undefined)
Defining function hdlc_change_mtu as symbolic
Defining function hdlc_start_xmit as symbolic
Defining function ldv_t3e3_ops_ndo_init_1 as symbolic
Defining function ldv_t3e3_ops_ndo_uninit_1 as symbolic
Defining function hdlc_open as symbolic
Defining function try_module_get as symbolic
Defining function hdlc_ioctl as symbolic
Defining function capable as symbolic
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function netdev_err as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_trylock as symbolic
Defining function netdev_info as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_error
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
INFO: After-slicing optimizations and preparation time: 0.449281930923
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 175 236 1023 7586
INFO: Starting verification
KLEE: WARNING ONCE: function "cpld_write" has inline asm
KLEE: WARNING ONCE: function "dc_clear_descriptor_list" has inline asm
KLEE: WARNING ONCE: function "dc_intr" has inline asm
KLEE: WARNING ONCE: function "exar7250_intr" has inline asm
KLEE: WARNING ONCE: function "dc_intr_rx" has inline asm
KLEE: WARNING ONCE: function "dc_receiver_onoff" has inline asm
KLEE: WARNING ONCE: function "dc_start_intr" has inline asm
KLEE: WARNING ONCE: function "exar7250_write" has inline asm
KLEE: WARNING ONCE: function "bootrom_read" has inline asm
KLEE: WARNING ONCE: function "dc_intr_tx_underflow" has inline asm
KLEE: WARNING ONCE: function "dc_intr_tx" has inline asm
KLEE: WARNING ONCE: function "dc_stop" has inline asm
KLEE: WARNING ONCE: function "dc_reset" has inline asm
KLEE: WARNING ONCE: function "dc_init" has inline asm
KLEE: WARNING ONCE: function "dc_transmitter_onoff" has inline asm
KLEE: WARNING ONCE: function "dc_set_output_port" has inline asm
KLEE: WARNING ONCE: function "exar7300_write" has inline asm
KLEE: WARNING ONCE: function "t3e3_if_start_xmit" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "t3e3_open" has inline asm
KLEE: WARNING ONCE: function "t3e3_reg_read" has inline asm
KLEE: WARNING ONCE: function "t3e3_reg_write" has inline asm
KLEE: WARNING ONCE: function "exar7300_read" has inline asm
KLEE: WARNING ONCE: function "t3e3_set_loopback" has inline asm
KLEE: WARNING ONCE: function "cpld_clear_bit" has inline asm
KLEE: WARNING ONCE: function "cpld_set_bit" has inline asm
KLEE: WARNING ONCE: function "bootrom_write" has inline asm
KLEE: WARNING ONCE: function "dc_stop_intr" has inline asm
KLEE: WARNING ONCE: function "dc_set_loopback" has inline asm
KLEE: WARNING ONCE: function "t3e3_eeprom_read_word" has inline asm
KLEE: ERROR: /tmp/symbiotic-0DmA5A/32_7a_cilled_true-unreach-call_linux-3.8-rc1-drivers--staging--sbe-2t3e3--sbe-2t3e3.ko-main.cil.out.c:4989: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 20139 states (over memory cap)
KLEE: WARNING: killing 15757 states (over memory cap)
KLEE: WARNING: killing 15530 states (over memory cap)
KLEE: WARNING: killing 15447 states (over memory cap)
KLEE: WARNING: killing 15511 states (over memory cap)
KLEE: WARNING: killing 15575 states (over memory cap)
KLEE: WARNING: killing 15785 states (over memory cap)
KLEE: WARNING: killing 15857 states (over memory cap)
KLEE: WARNING: killing 15921 states (over memory cap)
KLEE: WARNING: killing 15570 states (over memory cap)
KLEE: WARNING: killing 15780 states (over memory cap)
KLEE: WARNING: killing 16136 states (over memory cap)
KLEE: WARNING: killing 15796 states (over memory cap)
KLEE: WARNING: killing 16145 states (over memory cap)
KLEE: WARNING: killing 15805 states (over memory cap)
KLEE: WARNING: killing 16026 states (over memory cap)
KLEE: WARNING: killing 16101 states (over memory cap)
KLEE: WARNING: killing 15895 states (over memory cap)
KLEE: WARNING: killing 15705 states (over memory cap)
KLEE: WARNING: killing 16188 states (over memory cap)
KLEE: WARNING: killing 15728 states (over memory cap)
KLEE: WARNING: killing 15801 states (over memory cap)
KLEE: WARNING: killing 16144 states (over memory cap)
KLEE: WARNING: killing 15816 states (over memory cap)
KLEE: WARNING: killing 15895 states (over memory cap)
KLEE: WARNING: killing 15700 states (over memory cap)
KLEE: WARNING: killing 15777 states (over memory cap)
KLEE: WARNING: killing 15322 states (over memory cap)
KLEE: WARNING: killing 15402 states (over memory cap)
KLEE: WARNING: killing 15732 states (over memory cap)
KLEE: WARNING: killing 15420 states (over memory cap)
KLEE: WARNING: killing 15492 states (over memory cap)
KLEE: WARNING: killing 15437 states (over memory cap)
KLEE: WARNING: killing 15510 states (over memory cap)
KLEE: WARNING: killing 15579 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15474 states (over memory cap)
KLEE: WARNING: killing 15555 states (over memory cap)
KLEE: WARNING: killing 15630 states (over memory cap)
KLEE: WARNING: killing 15710 states (over memory cap)
KLEE: WARNING: killing 15534 states (over memory cap)
KLEE: WARNING: killing 15357 states (over memory cap)
KLEE: WARNING: killing 15556 states (over memory cap)
KLEE: WARNING: killing 15509 states (over memory cap)
KLEE: WARNING: killing 15461 states (over memory cap)
KLEE: WARNING: killing 15660 states (over memory cap)
KLEE: WARNING: killing 15242 states (over memory cap)
KLEE: WARNING: killing 15439 states (over memory cap)
KLEE: WARNING: killing 15393 states (over memory cap)
KLEE: WARNING: killing 15349 states (over memory cap)
KLEE: WARNING: killing 15420 states (over memory cap)
KLEE: WARNING: killing 15249 states (over memory cap)
KLEE: WARNING: killing 15207 states (over memory cap)
KLEE: WARNING: killing 15157 states (over memory cap)
KLEE: WARNING: killing 15358 states (over memory cap)
KLEE: WARNING: killing 15556 states (over memory cap)
KLEE: WARNING: killing 15150 states (over memory cap)
KLEE: WARNING: killing 15592 states (over memory cap)
KLEE: WARNING: killing 15302 states (over memory cap)
KLEE: WARNING: killing 15140 states (over memory cap)
KLEE: WARNING: killing 15338 states (over memory cap)
KLEE: WARNING: killing 15179 states (over memory cap)
KLEE: WARNING: killing 15613 states (over memory cap)
KLEE: WARNING: killing 15216 states (over memory cap)
KLEE: WARNING: killing 15284 states (over memory cap)
KLEE: WARNING: killing 15244 states (over memory cap)
KLEE: WARNING: killing 15207 states (over memory cap)
KLEE: WARNING: killing 15168 states (over memory cap)
KLEE: WARNING: killing 15005 states (over memory cap)
KLEE: WARNING: killing 15077 states (over memory cap)
KLEE: WARNING: killing 15272 states (over memory cap)
KLEE: WARNING: killing 15347 states (over memory cap)
KLEE: WARNING: killing 15307 states (over memory cap)
KLEE: WARNING: killing 15500 states (over memory cap)
KLEE: WARNING: killing 15342 states (over memory cap)
KLEE: WARNING: killing 15075 states (over memory cap)
KLEE: WARNING: killing 15148 states (over memory cap)
KLEE: WARNING: killing 15228 states (over memory cap)
KLEE: WARNING: killing 15423 states (over memory cap)
KLEE: WARNING: killing 15154 states (over memory cap)
KLEE: WARNING: killing 15112 states (over memory cap)
KLEE: WARNING: killing 15185 states (over memory cap)
KLEE: WARNING: killing 15041 states (over memory cap)
KLEE: WARNING: killing 15345 states (over memory cap)
KLEE: WARNING: killing 15074 states (over memory cap)
KLEE: WARNING: killing 15153 states (over memory cap)
KLEE: WARNING: killing 15214 states (over memory cap)
KLEE: WARNING: killing 15070 states (over memory cap)
KLEE: WARNING: killing 15253 states (over memory cap)
KLEE: WARNING: killing 15217 states (over memory cap)
KLEE: WARNING: killing 15175 states (over memory cap)
KLEE: WARNING: killing 15251 states (over memory cap)
KLEE: WARNING: killing 15099 states (over memory cap)
KLEE: WARNING: killing 15063 states (over memory cap)
KLEE: WARNING: killing 15143 states (over memory cap)
KLEE: WARNING: killing 15104 states (over memory cap)
KLEE: WARNING: killing 15514 states (over memory cap)
KLEE: WARNING: killing 15260 states (over memory cap)
KLEE: WARNING: killing 15220 states (over memory cap)
KLEE: WARNING: killing 14853 states (over memory cap)
KLEE: WARNING: killing 14820 states (over memory cap)
KLEE: WARNING: killing 14999 states (over memory cap)
KLEE: WARNING: killing 15181 states (over memory cap)
KLEE: WARNING: killing 15144 states (over memory cap)
KLEE: WARNING: killing 15431 states (over memory cap)
KLEE: WARNING: killing 15073 states (over memory cap)
KLEE: WARNING: killing 14933 states (over memory cap)
KLEE: WARNING: killing 15229 states (over memory cap)
KLEE: WARNING: killing 14978 states (over memory cap)
KLEE: WARNING: killing 15157 states (over memory cap)
KLEE: WARNING: killing 15221 states (over memory cap)
KLEE: WARNING: killing 15087 states (over memory cap)
KLEE: WARNING: killing 15159 states (over memory cap)
KLEE: WARNING: killing 15222 states (over memory cap)
KLEE: WARNING: killing 14877 states (over memory cap)
