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--intel--ixgb--ixgb.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.: 236 340 2331 21157
Removed infinite loop in ixgb_setup_fc
Removed infinite loop in ixgb_read_phy_reg
Removed infinite loop in ixgb_write_phy_reg
Removed infinite loop in napi_enable
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_unmap_page
Removed infinite loop in ixgb_hash_mc_addr
Removed infinite loop in dma_map_page
Removed infinite loop in ixgb_validate_option
Removed infinite loop in ixgb_wait_eeprom_command
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.734391927719
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to 'netdev_err' (function is undefined)
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'skb_trim' (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
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function __phys_addr as symbolic
Defining function find_first_bit as symbolic
Defining function find_next_bit as symbolic
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function queue_work_on as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function dma_alloc_attrs as symbolic
Removed calls to 'pci_set_master' (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 'netdev_info' (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)
Defining function cancel_work_sync 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)
Defining function register_netdev as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function __napi_alloc_skb as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Defining function ethtool_op_get_link as symbolic
Defining function strlcpy 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_suspend_7 as symbolic
Defining function ldv_release_7 as symbolic
Defining function ldv_probe_7 as symbolic
Defining function ldv_ndo_init_5 as symbolic
Defining function ldv_ndo_uninit_5 as symbolic
Defining function __pci_register_driver as symbolic
Defining function queue_delayed_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:
  strcpy
  strncpy
  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.69132900238
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 209 259 1217 11815
INFO: Starting verification
KLEE: WARNING ONCE: function "ixgb_open" has inline asm
KLEE: WARNING ONCE: function "ixgb_xmit_frame" has inline asm
KLEE: WARNING ONCE: function "ixgb_set_multi" has inline asm
KLEE: WARNING ONCE: function "ixgb_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "ixgb_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "ixgb_down" has inline asm
KLEE: WARNING ONCE: function "ixgb_up" has inline asm
KLEE: WARNING ONCE: function "ixgb_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_adapter_stop" has inline asm
KLEE: WARNING ONCE: function "ixgb_init_hw" has inline asm
KLEE: WARNING ONCE: function "ixgb_mac_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_rar_set" has inline asm
KLEE: WARNING ONCE: function "ixgb_check_for_link" has inline asm
KLEE: WARNING ONCE: function "ixgb_link_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "ixgb_read_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_shift_out_bits" has inline asm
KLEE: WARNING ONCE: function "ixgb_standby_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_phy_reg" has inline asm
KLEE: WARNING ONCE: function "ixgb_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "ixgb_intr" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "ixgb_clean_tx_ring" has inline asm
KLEE: WARNING ONCE: function "ixgb_clean_rx_ring" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "ixgb_mc_addr_list_update" has inline asm
KLEE: WARNING ONCE: function "ixgb_maybe_stop_tx" has inline asm
KLEE: WARNING ONCE: function "ixgb_probe" has inline asm
KLEE: WARNING ONCE: function "ixgb_watchdog" has inline asm
KLEE: WARNING ONCE: function "ixgb_check_for_bad_link" has inline asm
KLEE: WARNING ONCE: function "ixgb_update_stats" has inline asm
KLEE: WARNING ONCE: function "ixgb_io_slot_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_get_regs" has inline asm
KLEE: WARNING ONCE: function "ixgb_set_phys_id" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_vfta" has inline asm
KLEE: WARNING ONCE: function "ixgb_led_on" has inline asm
KLEE: WARNING ONCE: function "ixgb_led_off" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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-aLRJ5L/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "ixgb_open" has inline asm
KLEE: WARNING ONCE: function "ixgb_xmit_frame" has inline asm
KLEE: WARNING ONCE: function "ixgb_set_multi" has inline asm
KLEE: WARNING ONCE: function "ixgb_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "ixgb_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "ixgb_down" has inline asm
KLEE: WARNING ONCE: function "ixgb_up" has inline asm
KLEE: WARNING ONCE: function "ixgb_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_adapter_stop" has inline asm
KLEE: WARNING ONCE: function "ixgb_init_hw" has inline asm
KLEE: WARNING ONCE: function "ixgb_mac_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_rar_set" has inline asm
KLEE: WARNING ONCE: function "ixgb_check_for_link" has inline asm
KLEE: WARNING ONCE: function "ixgb_link_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "ixgb_read_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_shift_out_bits" has inline asm
KLEE: WARNING ONCE: function "ixgb_standby_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_phy_reg" has inline asm
KLEE: WARNING ONCE: function "ixgb_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "ixgb_intr" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "ixgb_clean_tx_ring" has inline asm
KLEE: WARNING ONCE: function "ixgb_clean_rx_ring" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "ixgb_mc_addr_list_update" has inline asm
KLEE: WARNING ONCE: function "ixgb_maybe_stop_tx" has inline asm
KLEE: WARNING ONCE: function "ixgb_probe" has inline asm
KLEE: WARNING ONCE: function "ixgb_watchdog" has inline asm
KLEE: WARNING ONCE: function "ixgb_check_for_bad_link" has inline asm
KLEE: WARNING ONCE: function "ixgb_update_stats" has inline asm
KLEE: WARNING ONCE: function "ixgb_io_slot_reset" has inline asm
KLEE: WARNING ONCE: function "ixgb_get_regs" has inline asm
KLEE: WARNING ONCE: function "ixgb_set_phys_id" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_eeprom" has inline asm
KLEE: WARNING ONCE: function "ixgb_write_vfta" has inline asm
KLEE: WARNING ONCE: function "ixgb_led_on" has inline asm
KLEE: WARNING ONCE: function "ixgb_led_off" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
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: 1.63473391533
