bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.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.: 270 406 2252 14004
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.557065963745
Defining function printk as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function netpoll_trap as symbolic
Defining function skb_put as symbolic
Defining function netif_rx as symbolic
Defining function __phys_addr as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function __pci_register_driver as symbolic
Defining function hdlc_change_mtu as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'hdlc_close' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function capable as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function hdlc_ioctl as symbolic
Defining function hdlc_open as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Defining function hdlc_start_xmit as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function del_timer as symbolic
Defining function dev_trans_start as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'pci_set_master' (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 'unregister_hdlc_device' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function alloc_hdlcdev as symbolic
Defining function register_netdev as symbolic
Defining function ldv_pre_register_netdev as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_switch_to_interrupt_context' (function is undefined)
Removed calls to 'ldv_switch_to_process_context' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.556918144226
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 254 366 1127 8480
INFO: Starting verification
KLEE: WARNING ONCE: function "lmc_hssi_init" has inline asm
KLEE: WARNING ONCE: function "lmc_hssi_set_clock" has inline asm
KLEE: WARNING ONCE: function "lmc_mii_writereg" has inline asm
KLEE: WARNING ONCE: function "lmc_ssi_get_link_status" has inline asm
KLEE: WARNING ONCE: function "lmc_mii_readreg" has inline asm
KLEE: WARNING ONCE: function "lmc_ssi_init" has inline asm
KLEE: WARNING ONCE: function "lmc_ssi_default" has inline asm
KLEE: WARNING ONCE: function "lmc_ssi_set_clock" has inline asm
KLEE: WARNING ONCE: function "write_av9110" has inline asm
KLEE: WARNING ONCE: function "write_av9110_bit" has inline asm
KLEE: WARNING ONCE: function "lmc_t1_set_clock" has inline asm
KLEE: WARNING ONCE: function "lmc_interrupt" has inline asm
KLEE: WARNING ONCE: function "lmc_running_reset" has inline asm
KLEE: WARNING ONCE: function "lmc_dec_reset" has inline asm
KLEE: WARNING ONCE: function "lmc_reset" has inline asm
KLEE: WARNING ONCE: function "lmc_softreset" has inline asm
KLEE: WARNING ONCE: function "lmc_ioctl" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "lmc_get_stats" has inline asm
KLEE: WARNING ONCE: function "lmc_close" has inline asm
KLEE: WARNING ONCE: function "lmc_driver_timeout" has inline asm
KLEE: WARNING ONCE: function "lmc_init_one" has inline asm
KLEE: WARNING ONCE: function "lmc_start_xmit" has inline asm
KLEE: WARNING ONCE: function "lmc_open" has inline asm
KLEE: WARNING ONCE: function "lmc_watchdog" has inline asm
KLEE: WARNING ONCE: function "lmc_gpio_mkoutput" has inline asm
KLEE: WARNING ONCE: function "lmc_gpio_mkinput" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_3_15" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_4_8" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_5_15" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_5_8" has inline asm
KLEE: WARNING ONCE: function "ldv_dummy_resourceless_instance_callback_6_15" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_lmc___media_dummy_resourceless_instance_3" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_lmc___media_dummy_resourceless_instance_4" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_lmc___media_dummy_resourceless_instance_5" has inline asm
KLEE: WARNING ONCE: function "ldv_struct_lmc___media_dummy_resourceless_instance_6" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c85420ce-7998-4ea3-a586-2dca133a1a62/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 26593 states (over memory cap)
KLEE: WARNING: killing 25124 states (over memory cap)
KLEE: WARNING: killing 24676 states (over memory cap)
KLEE: WARNING: killing 24070 states (over memory cap)
KLEE: WARNING: killing 24822 states (over memory cap)
KLEE: WARNING: killing 24220 states (over memory cap)
KLEE: WARNING: killing 24640 states (over memory cap)
KLEE: WARNING: killing 23725 states (over memory cap)
KLEE: WARNING: killing 24463 states (over memory cap)
KLEE: WARNING: killing 24218 states (over memory cap)
KLEE: WARNING: killing 24799 states (over memory cap)
KLEE: WARNING: killing 24540 states (over memory cap)
KLEE: WARNING: killing 24779 states (over memory cap)
KLEE: WARNING: killing 24541 states (over memory cap)
KLEE: WARNING: killing 25924 states (over memory cap)
KLEE: WARNING: killing 25845 states (over memory cap)
KLEE: WARNING: killing 25445 states (over memory cap)
KLEE: WARNING: killing 27147 states (over memory cap)
KLEE: WARNING: killing 27868 states (over memory cap)
KLEE: WARNING: killing 26349 states (over memory cap)
KLEE: WARNING: killing 27081 states (over memory cap)
KLEE: WARNING: killing 26860 states (over memory cap)
KLEE: WARNING: killing 27271 states (over memory cap)
KLEE: WARNING: killing 27195 states (over memory cap)
KLEE: WARNING: killing 26497 states (over memory cap)
KLEE: WARNING: killing 27392 states (over memory cap)
KLEE: WARNING: killing 27485 states (over memory cap)
KLEE: WARNING: killing 26951 states (over memory cap)
KLEE: WARNING: killing 26560 states (over memory cap)
KLEE: WARNING: killing 24623 states (over memory cap)
KLEE: WARNING: killing 25343 states (over memory cap)
KLEE: WARNING: killing 25285 states (over memory cap)
KLEE: WARNING: killing 24762 states (over memory cap)
KLEE: WARNING: killing 25316 states (over memory cap)
KLEE: WARNING: killing 24954 states (over memory cap)
KLEE: WARNING: killing 25056 states (over memory cap)
KLEE: WARNING: killing 24692 states (over memory cap)
KLEE: WARNING: killing 26020 states (over memory cap)
KLEE: WARNING: killing 25648 states (over memory cap)
KLEE: WARNING: killing 25111 states (over memory cap)
KLEE: WARNING: killing 25209 states (over memory cap)
KLEE: WARNING: killing 26073 states (over memory cap)
KLEE: WARNING: killing 25708 states (over memory cap)
KLEE: WARNING: killing 25948 states (over memory cap)
KLEE: WARNING: killing 25585 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:10936: invalid function pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25221 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:6708: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 26217 states (over memory cap)
KLEE: WARNING: killing 25425 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:5697: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25957 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:5712: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 26212 states (over memory cap)
KLEE: WARNING: killing 25715 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:5932: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25801 states (over memory cap)
KLEE: WARNING: killing 26211 states (over memory cap)
KLEE: WARNING: killing 25859 states (over memory cap)
KLEE: WARNING: killing 25658 states (over memory cap)
KLEE: WARNING: killing 25007 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:6664: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24808 states (over memory cap)
KLEE: WARNING: killing 25349 states (over memory cap)
KLEE: WARNING: killing 25885 states (over memory cap)
KLEE: WARNING: killing 25833 states (over memory cap)
KLEE: WARNING: killing 25492 states (over memory cap)
KLEE: WARNING: killing 25735 states (over memory cap)
KLEE: WARNING: killing 25835 states (over memory cap)
KLEE: WARNING: killing 25641 states (over memory cap)
KLEE: WARNING: killing 25888 states (over memory cap)
KLEE: WARNING: killing 25392 states (over memory cap)
KLEE: WARNING: killing 24910 states (over memory cap)
KLEE: WARNING: killing 25574 states (over memory cap)
KLEE: WARNING: killing 25234 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:5539: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25033 states (over memory cap)
KLEE: WARNING: killing 25568 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:10268: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25373 states (over memory cap)
KLEE: WARNING: killing 24610 states (over memory cap)
KLEE: WARNING: killing 25425 states (over memory cap)
KLEE: WARNING: killing 25801 states (over memory cap)
KLEE: WARNING: killing 25035 states (over memory cap)
KLEE: WARNING: killing 25983 states (over memory cap)
KLEE: WARNING: killing 14117 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:5653: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24517 states (over memory cap)
KLEE: WARNING: killing 25883 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:6477: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 25553 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-TX_sf_/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-wan-lmc-lmc_true-unreach-call.cil.c:6708: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24915 states (over memory cap)
