bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.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.: 198 293 1994 13752
Removed infinite loop in dma_unmap_page
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_page
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in napi_enable
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.521239042282
Removed calls to 'msleep' (function is undefined)
Removed calls to 'netdev_err' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'netdev_printk' (function is undefined)
Defining function eth_validate_addr as symbolic
Defining function eth_change_mtu as symbolic
Defining function queue_delayed_work_on as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'netdev_info' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'netdev_warn' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function mod_timer as symbolic
Defining function request_threaded_irq as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function strlcpy as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'iounmap' (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_netdev' (function is undefined)
Removed calls to 'destroy_workqueue' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Defining function dev_close as symbolic
Defining function cancel_delayed_work as symbolic
Defining function pci_enable_device as symbolic
Defining function printk as symbolic
Defining function pci_request_regions as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function pci_ioremap_bar as symbolic
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to '__napi_complete' (function is undefined)
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Defining function register_netdev as symbolic
Defining function pci_bus_write_config_word as symbolic
Defining function skb_put as symbolic
Defining function skb_push as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function dma_supported as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_shutdown_6 as symbolic
Defining function ldv_ndo_init_7 as symbolic
Defining function ldv_ndo_uninit_7 as symbolic
Defining function __pci_register_driver as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
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_ulong_named
INFO: After-slicing optimizations and preparation time: 0.6575050354
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 181 165 1207 9114
INFO: Starting verification
KLEE: WARNING ONCE: function "ql3xxx_send" has inline asm
KLEE: WARNING ONCE: function "ql3xxx_set_mac_address" has inline asm
KLEE: WARNING ONCE: function "ql3xxx_tx_timeout" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "ql_adapter_down" has inline asm
KLEE: WARNING ONCE: function "ql_wait_for_drvr_lock" has inline asm
KLEE: WARNING ONCE: function "ql_free_buffer_queues" has inline asm
KLEE: WARNING ONCE: function "ql_free_net_req_rsp_queues" has inline asm
KLEE: WARNING ONCE: function "ql_adapter_up" has inline asm
KLEE: WARNING ONCE: function "ql3xxx_isr" has inline asm
KLEE: WARNING ONCE: function "ql_sem_spinlock" has inline asm
KLEE: WARNING ONCE: function "ql_mii_enable_scan_mode" has inline asm
KLEE: WARNING ONCE: function "ql_this_adapter_controls_port" has inline asm
KLEE: WARNING ONCE: function "ql_mii_write_reg_ex" has inline asm
KLEE: WARNING ONCE: function "ql_mii_read_reg_ex" has inline asm
KLEE: WARNING ONCE: function "ql_mii_write_reg" has inline asm
KLEE: WARNING ONCE: function "ql_mii_disable_scan_mode" has inline asm
KLEE: WARNING ONCE: function "ql_wait_for_mii_ready" has inline asm
KLEE: WARNING ONCE: function "ql_mii_read_reg" has inline asm
KLEE: WARNING ONCE: function "ql_read_page0_reg_l" has inline asm
KLEE: WARNING ONCE: function "ql_get_settings" has inline asm
KLEE: WARNING ONCE: function "ql_get_pauseparam" has inline asm
KLEE: WARNING ONCE: function "ql_get_auto_cfg_status" has inline asm
KLEE: WARNING ONCE: function "ql_is_fiber" has inline asm
KLEE: WARNING ONCE: function "ql3xxx_probe" has inline asm
KLEE: WARNING ONCE: function "ql3xxx_remove" has inline asm
KLEE: WARNING ONCE: function "ql_reset_work" has inline asm
KLEE: WARNING ONCE: function "ql_link_state_machine_work" has inline asm
KLEE: WARNING ONCE: function "ql_port_start" has inline asm
KLEE: WARNING ONCE: function "ql_mac_cfg_soft_reset" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-2RtBB9/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.ko-entry_point_true-unreach-call.cil.out.c:11392: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_253b639c-690c-42e3-907b-130196fb6ece/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2RtBB9/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.ko-entry_point_true-unreach-call.cil.out.c:7242: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2RtBB9/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.ko-entry_point_true-unreach-call.cil.out.c:9012: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2RtBB9/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.ko-entry_point_true-unreach-call.cil.out.c:5944: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-2RtBB9/linux-4.2-rc1.tar.xz-43_2a-drivers--net--ethernet--qlogic--qla3xxx.ko-entry_point_true-unreach-call.cil.out.c:9038: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17091 states (over memory cap)
KLEE: WARNING: killing 10241 states (over memory cap)
KLEE: WARNING: killing 19203 states (over memory cap)
KLEE: WARNING: killing 10168 states (over memory cap)
KLEE: WARNING: killing 18883 states (over memory cap)
KLEE: WARNING: killing 19105 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 19426 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
KLEE: WARNING: killing 19317 states (over memory cap)
KLEE: WARNING: killing 10858 states (over memory cap)
KLEE: WARNING: killing 10545 states (over memory cap)
KLEE: WARNING: killing 20768 states (over memory cap)
KLEE: WARNING: killing 10591 states (over memory cap)
KLEE: WARNING: killing 10471 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 10832 states (over memory cap)
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: WARNING: killing 10608 states (over memory cap)
KLEE: WARNING: killing 10591 states (over memory cap)
KLEE: WARNING: killing 10870 states (over memory cap)
KLEE: WARNING: killing 10756 states (over memory cap)
KLEE: WARNING: killing 10842 states (over memory cap)
KLEE: WARNING: killing 10924 states (over memory cap)
KLEE: WARNING: killing 10521 states (over memory cap)
KLEE: WARNING: killing 10699 states (over memory cap)
KLEE: WARNING: killing 10204 states (over memory cap)
KLEE: WARNING: killing 9993 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10155 states (over memory cap)
KLEE: WARNING: killing 10046 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 10020 states (over memory cap)
KLEE: WARNING: killing 9911 states (over memory cap)
KLEE: WARNING: killing 9896 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 9869 states (over memory cap)
KLEE: WARNING: killing 10235 states (over memory cap)
KLEE: WARNING: killing 9937 states (over memory cap)
KLEE: WARNING: killing 9734 states (over memory cap)
KLEE: WARNING: killing 10099 states (over memory cap)
KLEE: WARNING: killing 10084 states (over memory cap)
KLEE: WARNING: killing 10448 states (over memory cap)
KLEE: WARNING: killing 9967 states (over memory cap)
KLEE: WARNING: killing 9951 states (over memory cap)
KLEE: WARNING: killing 9935 states (over memory cap)
KLEE: WARNING: killing 10390 states (over memory cap)
KLEE: WARNING: killing 10377 states (over memory cap)
KLEE: WARNING: killing 10463 states (over memory cap)
KLEE: WARNING: killing 10169 states (over memory cap)
KLEE: WARNING: killing 10345 states (over memory cap)
KLEE: WARNING: killing 10238 states (over memory cap)
KLEE: WARNING: killing 10038 states (over memory cap)
KLEE: WARNING: killing 10683 states (over memory cap)
KLEE: WARNING: killing 10673 states (over memory cap)
KLEE: WARNING: killing 10101 states (over memory cap)
KLEE: WARNING: killing 10372 states (over memory cap)
KLEE: WARNING: killing 10171 states (over memory cap)
KLEE: WARNING: killing 10162 states (over memory cap)
KLEE: WARNING: killing 10522 states (over memory cap)
KLEE: WARNING: killing 10323 states (over memory cap)
KLEE: WARNING: killing 10123 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10292 states (over memory cap)
KLEE: WARNING: killing 10742 states (over memory cap)
KLEE: WARNING: killing 10364 states (over memory cap)
KLEE: WARNING: killing 10442 states (over memory cap)
KLEE: WARNING: killing 10064 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10224 states (over memory cap)
KLEE: WARNING: killing 9937 states (over memory cap)
KLEE: WARNING: killing 10201 states (over memory cap)
KLEE: WARNING: killing 10462 states (over memory cap)
KLEE: WARNING: killing 10358 states (over memory cap)
KLEE: WARNING: killing 10162 states (over memory cap)
KLEE: WARNING: killing 10065 states (over memory cap)
KLEE: WARNING: killing 9960 states (over memory cap)
KLEE: WARNING: killing 10310 states (over memory cap)
KLEE: WARNING: killing 10298 states (over memory cap)
KLEE: WARNING: killing 10927 states (over memory cap)
KLEE: WARNING: killing 10282 states (over memory cap)
KLEE: WARNING: killing 10266 states (over memory cap)
KLEE: WARNING: killing 10528 states (over memory cap)
KLEE: WARNING: killing 10245 states (over memory cap)
KLEE: WARNING: killing 9870 states (over memory cap)
KLEE: WARNING: killing 10312 states (over memory cap)
KLEE: WARNING: killing 9851 states (over memory cap)
KLEE: WARNING: killing 10383 states (over memory cap)
KLEE: WARNING: killing 10010 states (over memory cap)
KLEE: WARNING: killing 10365 states (over memory cap)
KLEE: WARNING: killing 10353 states (over memory cap)
KLEE: WARNING: killing 10431 states (over memory cap)
KLEE: WARNING: killing 10516 states (over memory cap)
KLEE: WARNING: killing 10144 states (over memory cap)
KLEE: WARNING: killing 10222 states (over memory cap)
KLEE: WARNING: killing 10123 states (over memory cap)
KLEE: WARNING: killing 9933 states (over memory cap)
KLEE: WARNING: killing 10546 states (over memory cap)
KLEE: WARNING: killing 10006 states (over memory cap)
KLEE: WARNING: killing 9992 states (over memory cap)
KLEE: WARNING: killing 10336 states (over memory cap)
KLEE: WARNING: killing 10059 states (over memory cap)
KLEE: WARNING: killing 10049 states (over memory cap)
KLEE: WARNING: killing 9865 states (over memory cap)
KLEE: WARNING: killing 10291 states (over memory cap)
KLEE: WARNING: killing 10285 states (over memory cap)
KLEE: WARNING: killing 10364 states (over memory cap)
KLEE: WARNING: killing 10088 states (over memory cap)
KLEE: WARNING: killing 10519 states (over memory cap)
KLEE: WARNING: killing 10069 states (over memory cap)
KLEE: WARNING: killing 10320 states (over memory cap)
KLEE: WARNING: killing 10400 states (over memory cap)
KLEE: WARNING: killing 10390 states (over memory cap)
KLEE: WARNING: killing 10205 states (over memory cap)
KLEE: WARNING: killing 10193 states (over memory cap)
KLEE: WARNING: killing 10271 states (over memory cap)
KLEE: WARNING: killing 10615 states (over memory cap)
KLEE: WARNING: killing 10169 states (over memory cap)
KLEE: WARNING: killing 10334 states (over memory cap)
KLEE: WARNING: killing 9887 states (over memory cap)
KLEE: WARNING: killing 9613 states (over memory cap)
KLEE: WARNING: killing 9867 states (over memory cap)
KLEE: WARNING: killing 10382 states (over memory cap)
KLEE: WARNING: killing 10366 states (over memory cap)
KLEE: WARNING: killing 10186 states (over memory cap)
KLEE: WARNING: killing 10525 states (over memory cap)
KLEE: WARNING: killing 9994 states (over memory cap)
KLEE: WARNING: killing 10592 states (over memory cap)
KLEE: WARNING: killing 10237 states (over memory cap)
KLEE: WARNING: killing 10311 states (over memory cap)
KLEE: WARNING: killing 10129 states (over memory cap)
KLEE: WARNING: killing 10379 states (over memory cap)
KLEE: WARNING: killing 10024 states (over memory cap)
KLEE: WARNING: killing 9411 states (over memory cap)
KLEE: WARNING: killing 9748 states (over memory cap)
KLEE: WARNING: killing 9996 states (over memory cap)
KLEE: WARNING: killing 10415 states (over memory cap)
KLEE: WARNING: killing 10578 states (over memory cap)
KLEE: WARNING: killing 10832 states (over memory cap)
KLEE: WARNING: killing 10389 states (over memory cap)
KLEE: WARNING: killing 10120 states (over memory cap)
KLEE: WARNING: killing 10286 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10357 states (over memory cap)
KLEE: WARNING: killing 10178 states (over memory cap)
KLEE: WARNING: killing 10507 states (over memory cap)
KLEE: WARNING: killing 9904 states (over memory cap)
KLEE: WARNING: killing 9635 states (over memory cap)
KLEE: WARNING: killing 10475 states (over memory cap)
KLEE: WARNING: killing 9955 states (over memory cap)
KLEE: WARNING: killing 10627 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: WARNING: killing 10263 states (over memory cap)
KLEE: WARNING: killing 10256 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 10406 states (over memory cap)
KLEE: WARNING: killing 10228 states (over memory cap)
KLEE: WARNING: killing 10385 states (over memory cap)
KLEE: WARNING: killing 10289 states (over memory cap)
KLEE: WARNING: killing 10114 states (over memory cap)
KLEE: WARNING: killing 10189 states (over memory cap)
KLEE: WARNING: killing 10013 states (over memory cap)
KLEE: WARNING: killing 10337 states (over memory cap)
KLEE: WARNING: killing 10589 states (over memory cap)
KLEE: WARNING: killing 9735 states (over memory cap)
KLEE: WARNING: killing 9893 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 10460 states (over memory cap)
KLEE: WARNING: killing 10368 states (over memory cap)
KLEE: WARNING: killing 9860 states (over memory cap)
KLEE: WARNING: killing 10103 states (over memory cap)
KLEE: WARNING: killing 10510 states (over memory cap)
KLEE: WARNING: killing 9913 states (over memory cap)
KLEE: WARNING: killing 10570 states (over memory cap)
KLEE: WARNING: killing 10309 states (over memory cap)
KLEE: WARNING: killing 10299 states (over memory cap)
KLEE: WARNING: killing 9875 states (over memory cap)
KLEE: WARNING: killing 10116 states (over memory cap)
KLEE: WARNING: killing 10687 states (over memory cap)
KLEE: WARNING: killing 10432 states (over memory cap)
KLEE: WARNING: killing 10177 states (over memory cap)
KLEE: WARNING: killing 10500 states (over memory cap)
KLEE: WARNING: killing 10242 states (over memory cap)
KLEE: WARNING: killing 10147 states (over memory cap)
KLEE: WARNING: killing 10139 states (over memory cap)
KLEE: WARNING: killing 9968 states (over memory cap)
KLEE: WARNING: killing 10366 states (over memory cap)
KLEE: WARNING: killing 9784 states (over memory cap)
KLEE: WARNING: killing 10019 states (over memory cap)
KLEE: WARNING: killing 10094 states (over memory cap)
KLEE: WARNING: killing 9999 states (over memory cap)
KLEE: WARNING: killing 10237 states (over memory cap)
KLEE: WARNING: killing 10477 states (over memory cap)
KLEE: WARNING: killing 9976 states (over memory cap)
KLEE: WARNING: killing 9722 states (over memory cap)
KLEE: WARNING: killing 10368 states (over memory cap)
KLEE: WARNING: killing 10518 states (over memory cap)
KLEE: WARNING: killing 10268 states (over memory cap)
KLEE: WARNING: killing 10343 states (over memory cap)
KLEE: WARNING: killing 10416 states (over memory cap)
KLEE: WARNING: killing 10324 states (over memory cap)
KLEE: WARNING: killing 10479 states (over memory cap)
KLEE: WARNING: killing 10712 states (over memory cap)
KLEE: WARNING: killing 10216 states (over memory cap)
KLEE: WARNING: killing 10126 states (over memory cap)
KLEE: WARNING: killing 10282 states (over memory cap)
KLEE: WARNING: killing 10196 states (over memory cap)
KLEE: WARNING: killing 10265 states (over memory cap)
KLEE: WARNING: killing 10335 states (over memory cap)
KLEE: WARNING: killing 10246 states (over memory cap)
KLEE: WARNING: killing 10319 states (over memory cap)
KLEE: WARNING: killing 9987 states (over memory cap)
KLEE: WARNING: killing 10378 states (over memory cap)
KLEE: WARNING: killing 10371 states (over memory cap)
KLEE: WARNING: killing 9959 states (over memory cap)
KLEE: WARNING: killing 9543 states (over memory cap)
KLEE: WARNING: killing 9773 states (over memory cap)
KLEE: WARNING: killing 10164 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 10066 states (over memory cap)
KLEE: WARNING: killing 10136 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
KLEE: WARNING: killing 10115 states (over memory cap)
