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--icplus--ipg.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.: 80 160 1077 7743
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.297344923019
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '__mutex_init' (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 'iowrite16' (function is undefined)
Removed calls to 'netdev_info' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function pci_enable_device as symbolic
Defining function printk as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_iomap as symbolic
Defining function register_netdev as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'iowrite32' (function is undefined)
Removed calls to 'iowrite8' (function is undefined)
Defining function ioread16 as symbolic
Defining function ioread8 as symbolic
Defining function ioread32 as symbolic
Removed calls to '__dev_kfree_skb_irq' (function is undefined)
Removed calls to 'netdev_err' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function crc32_le as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Defining function dma_set_mask as symbolic
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function eth_mac_addr as symbolic
Defining function eth_validate_addr as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function generic_mii_ioctl as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Defining function request_threaded_irq as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_rx as symbolic
Defining function mii_nway_restart as symbolic
Defining function mii_ethtool_sset as symbolic
Defining function mii_ethtool_gset 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_ndo_init_4 as symbolic
Defining function ldv_ndo_uninit_4 as symbolic
Defining function ldv_shutdown_3 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:
  __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.355798959732
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 136 126 593 3947
INFO: Starting verification
KLEE: WARNING ONCE: function "ipg_nic_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_open" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_stop" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_hard_start_xmit" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
KLEE: output directory is "/tmp/symbiotic-_8EH_1/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ipg_nic_set_multicast_list" has inline asm
KLEE: WARNING ONCE: function "pci_unmap_single" has inline asm
KLEE: WARNING ONCE: function "pci_map_single" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_open" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_stop" has inline asm
KLEE: WARNING ONCE: function "ipg_nic_hard_start_xmit" has inline asm
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: undefined reference to variable: system_wq
KLEE: ERROR: unable to load symbol(system_wq) while initializing globals.
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 0.778334140778
