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-08_1a-drivers--net--ethernet--intel--e1000--e1000.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.: 512 501 6916 47264
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_sync_single_for_cpu
Removed infinite loop in dma_map_page
Removed infinite loop in dma_unmap_page
Removed infinite loop in dql_queued
Removed infinite loop in __skb_put
Removed infinite loop in e1000_check_options
Removed infinite loop in e1000_validate_option
Removed infinite loop in e1000_check_copper_options
Removed infinite loop in dma_unmap_single_attrs___0
Removed infinite loop in dma_sync_single_for_device
Removed infinite loop in dma_sync_single_for_cpu___0
Removed infinite loop in dma_map_single_attrs___0
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 1.42848014832
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'usleep_range' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'netdev_err' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'netdev_warn' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to 'skb_clone_tx_timestamp' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Defining function eth_validate_addr as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'synchronize_irq' (function is undefined)
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Removed calls to 'pci_clear_mwi' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function find_first_bit as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'ioread16_rep' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to '__udelay' (function is undefined)
Defining function pcix_set_mmrbc as symbolic
Defining function pcix_get_mmrbc as symbolic
Defining function pci_set_mwi as symbolic
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to '__free_page_frag' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
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
Defining function netdev_alloc_frag as symbolic
Defining function build_skb as symbolic
Defining function skb_put as symbolic
Defining function eth_type_trans as symbolic
Defining function napi_gro_receive as symbolic
Defining function __napi_alloc_skb as symbolic
Defining function alloc_pages_current as symbolic
Defining function napi_get_frags as symbolic
Defining function napi_gro_frags as symbolic
Defining function ___pskb_trim as symbolic
Defining function find_next_bit as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'dql_reset' (function is undefined)
Defining function cancel_work_sync as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to '__napi_schedule' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Defining function queue_work_on as symbolic
Defining function printk as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function net_ratelimit as symbolic
Defining function csum_ipv6_magic as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_pad as symbolic
Removed calls to 'vfree' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function request_threaded_irq as symbolic
Defining function vzalloc as symbolic
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 '__raw_spin_lock_init' (function is undefined)
Removed calls to 'print_hex_dump' (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 '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_selected_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Defining function pci_wake_from_d3 as symbolic
Defining function pci_set_power_state as symbolic
Defining function pci_save_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_enable_device_mem as symbolic
Defining function __pci_enable_wake as symbolic
Defining function pci_prepare_to_sleep as symbolic
Defining function pci_select_bars as symbolic
Defining function pci_request_selected_regions as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function pci_ioremap_bar as symbolic
Removed calls to 'dql_completed' (function is undefined)
Removed calls to 'netif_schedule_queue' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'dev_warn' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Defining function device_set_wakeup_enable as symbolic
Defining function register_netdev as symbolic
Defining function ioremap_nocache as symbolic
Defining function dma_set_mask as symbolic
Defining function dma_supported as symbolic
Defining function pci_bus_read_config_word as symbolic
Removed calls to 'debug_dma_sync_single_for_device' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Defining function ethtool_op_get_ts_info as symbolic
Defining function dev_close as symbolic
Defining function dev_open as symbolic
Defining function msleep_interruptible as symbolic
Defining function __alloc_skb as symbolic
Removed calls to 'iowrite16_rep' (function is undefined)
Defining function strlcpy as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'pci_unregister_driver' (function is undefined)
Defining function ldv_suspend_late_9 as symbolic
Defining function ldv_resume_early_9 as symbolic
Defining function ldv_ndo_init_8 as symbolic
Defining function ldv_ndo_uninit_8 as symbolic
Defining function ldv_suspend_10 as symbolic
Defining function ldv_release_10 as symbolic
Defining function ldv_probe_10 as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Linked our definitions to these undefined functions:
  strcpy
  strncpy
  __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: 1.45471405983
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 392 331 3058 24551
INFO: Starting verification
KLEE: WARNING ONCE: function "e1000_open" has inline asm
KLEE: WARNING ONCE: function "e1000_close" has inline asm
KLEE: WARNING ONCE: function "e1000_xmit_frame" has inline asm
KLEE: WARNING ONCE: function "e1000_set_rx_mode" has inline asm
KLEE: WARNING ONCE: function "e1000_change_mtu" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "e1000_set_features" has inline asm
KLEE: WARNING ONCE: function "e1000_reinit_locked" has inline asm
KLEE: WARNING ONCE: function "e1000_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_reset_hw" has inline asm
KLEE: WARNING ONCE: function "e1000_init_hw" has inline asm
KLEE: WARNING ONCE: function "e1000_update_mng_vlan" has inline asm
KLEE: WARNING ONCE: function "e1000_reset_adaptive" has inline asm
KLEE: WARNING ONCE: function "e1000_read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "e1000_write_phy_reg_ex" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_out_mdi_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_set_media_type" has inline asm
KLEE: WARNING ONCE: function "e1000_rar_set" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_link" has inline asm
KLEE: WARNING ONCE: function "e1000_phy_hw_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_config_mac_to_phy" has inline asm
KLEE: WARNING ONCE: function "e1000_check_for_link" has inline asm
KLEE: WARNING ONCE: function "e1000_get_speed_and_duplex" has inline asm
KLEE: WARNING ONCE: function "e1000_force_mac_fc" has inline asm
KLEE: WARNING ONCE: function "e1000_init_eeprom_params" has inline asm
KLEE: WARNING ONCE: function "e1000_acquire_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_release_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_standby_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_out_ee_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_in_ee_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_down" has inline asm
KLEE: WARNING ONCE: function "e1000_up" has inline asm
KLEE: WARNING ONCE: function "e1000_configure" has inline asm
KLEE: WARNING ONCE: function "napi_enable" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_filter_on_off" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_rctl" has inline asm
KLEE: WARNING ONCE: function "e1000_configure_rx" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_jumbo_rx_irq" has inline asm
KLEE: WARNING ONCE: function "e1000_alloc_jumbo_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "e1000_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_page" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_page" has inline asm
KLEE: WARNING ONCE: function "e1000_down_and_stop" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_tx_ring" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_rx_ring" has inline asm
KLEE: WARNING ONCE: function "e1000_intr" has inline asm
KLEE: WARNING ONCE: function "e1000_write_vfta" has inline asm
KLEE: WARNING ONCE: function "e1000_enter_82542_rst" has inline asm
KLEE: WARNING ONCE: function "e1000_leave_82542_rst" has inline asm
KLEE: WARNING ONCE: function "e1000_maybe_stop_tx" has inline asm
KLEE: WARNING ONCE: function "e1000_power_down_phy" has inline asm
KLEE: WARNING ONCE: function "e1000_probe" has inline asm
KLEE: WARNING ONCE: function "e1000_remove" has inline asm
KLEE: WARNING ONCE: function "e1000_resume" has inline asm
KLEE: WARNING ONCE: function "__e1000_shutdown" has inline asm
KLEE: WARNING ONCE: function "e1000_get_bus_info" has inline asm
KLEE: WARNING ONCE: function "e1000_read_mac_addr" has inline asm
KLEE: WARNING ONCE: function "e1000_watchdog" has inline asm
KLEE: WARNING ONCE: function "e1000_82547_tx_fifo_stall_task" has inline asm
KLEE: WARNING ONCE: function "e1000_check_options" has inline asm
KLEE: WARNING ONCE: function "e1000_has_link" has inline asm
KLEE: WARNING ONCE: function "e1000_update_stats" has inline asm
KLEE: WARNING ONCE: function "e1000_update_adaptive" has inline asm
KLEE: WARNING ONCE: function "e1000_io_slot_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_io_resume" has inline asm
KLEE: WARNING ONCE: function "e1000_get_settings" has inline asm
KLEE: WARNING ONCE: function "e1000_set_settings" has inline asm
KLEE: WARNING ONCE: function "e1000_get_regs" has inline asm
KLEE: WARNING ONCE: function "e1000_set_coalesce" has inline asm
KLEE: WARNING ONCE: function "e1000_set_ringparam" has inline asm
KLEE: WARNING ONCE: function "e1000_set_pauseparam" has inline asm
KLEE: WARNING ONCE: function "e1000_diag_test" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_led" has inline asm
KLEE: WARNING ONCE: function "e1000_led_on" has inline asm
KLEE: WARNING ONCE: function "e1000_led_off" has inline asm
KLEE: WARNING ONCE: function "e1000_cleanup_led" has inline asm
KLEE: WARNING ONCE: function "e1000_link_test" has inline asm
KLEE: WARNING ONCE: function "reg_pattern_test" has inline asm
KLEE: WARNING ONCE: function "reg_set_and_check" has inline asm
KLEE: WARNING ONCE: function "e1000_test_intr" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs___0" has inline asm
KLEE: WARNING ONCE: function "e1000_set_phy_loopback" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs___0" has inline asm
KLEE: WARNING ONCE: function "e1000_write_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_wol_exclusion" has inline asm
KLEE: WARNING ONCE: function "e1000_config_collision_dist" has inline asm
KLEE: WARNING ONCE: function "e1000_io_write" has inline asm
KLEE: WARNING ONCE: function "e1000_enable_mng_pass_thru" has inline asm
KLEE: WARNING ONCE: function "ldv_irq_2" has inline asm
KLEE: WARNING ONCE: function "ldv_irq_1" 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-MFeggY/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "e1000_open" has inline asm
KLEE: WARNING ONCE: function "e1000_close" has inline asm
KLEE: WARNING ONCE: function "e1000_xmit_frame" has inline asm
KLEE: WARNING ONCE: function "e1000_set_rx_mode" has inline asm
KLEE: WARNING ONCE: function "e1000_change_mtu" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_rx_add_vid" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_rx_kill_vid" has inline asm
KLEE: WARNING ONCE: function "e1000_set_features" has inline asm
KLEE: WARNING ONCE: function "e1000_reinit_locked" has inline asm
KLEE: WARNING ONCE: function "e1000_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_reset_hw" has inline asm
KLEE: WARNING ONCE: function "e1000_init_hw" has inline asm
KLEE: WARNING ONCE: function "e1000_update_mng_vlan" has inline asm
KLEE: WARNING ONCE: function "e1000_reset_adaptive" has inline asm
KLEE: WARNING ONCE: function "e1000_read_phy_reg" has inline asm
KLEE: WARNING ONCE: function "e1000_write_phy_reg_ex" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_out_mdi_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_set_media_type" has inline asm
KLEE: WARNING ONCE: function "e1000_rar_set" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_link" has inline asm
KLEE: WARNING ONCE: function "e1000_phy_hw_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_config_mac_to_phy" has inline asm
KLEE: WARNING ONCE: function "e1000_check_for_link" has inline asm
KLEE: WARNING ONCE: function "e1000_get_speed_and_duplex" has inline asm
KLEE: WARNING ONCE: function "e1000_force_mac_fc" has inline asm
KLEE: WARNING ONCE: function "e1000_init_eeprom_params" has inline asm
KLEE: WARNING ONCE: function "e1000_acquire_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_release_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_standby_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_out_ee_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_shift_in_ee_bits" has inline asm
KLEE: WARNING ONCE: function "e1000_down" has inline asm
KLEE: WARNING ONCE: function "e1000_up" has inline asm
KLEE: WARNING ONCE: function "e1000_configure" has inline asm
KLEE: WARNING ONCE: function "napi_enable" has inline asm
KLEE: WARNING ONCE: function "e1000_vlan_filter_on_off" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_rctl" has inline asm
KLEE: WARNING ONCE: function "e1000_configure_rx" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_jumbo_rx_irq" has inline asm
KLEE: WARNING ONCE: function "e1000_alloc_jumbo_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "e1000_alloc_rx_buffers" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "dma_map_page" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_page" has inline asm
KLEE: WARNING ONCE: function "e1000_down_and_stop" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_tx_ring" has inline asm
KLEE: WARNING ONCE: function "e1000_clean_rx_ring" has inline asm
KLEE: WARNING ONCE: function "e1000_intr" has inline asm
KLEE: WARNING ONCE: function "e1000_write_vfta" has inline asm
KLEE: WARNING ONCE: function "e1000_enter_82542_rst" has inline asm
KLEE: WARNING ONCE: function "e1000_leave_82542_rst" has inline asm
KLEE: WARNING ONCE: function "e1000_maybe_stop_tx" has inline asm
KLEE: WARNING ONCE: function "e1000_power_down_phy" has inline asm
KLEE: WARNING ONCE: function "e1000_probe" has inline asm
KLEE: WARNING ONCE: function "e1000_remove" has inline asm
KLEE: WARNING ONCE: function "e1000_resume" has inline asm
KLEE: WARNING ONCE: function "__e1000_shutdown" has inline asm
KLEE: WARNING ONCE: function "e1000_get_bus_info" has inline asm
KLEE: WARNING ONCE: function "e1000_read_mac_addr" has inline asm
KLEE: WARNING ONCE: function "e1000_watchdog" has inline asm
KLEE: WARNING ONCE: function "e1000_82547_tx_fifo_stall_task" has inline asm
KLEE: WARNING ONCE: function "e1000_check_options" has inline asm
KLEE: WARNING ONCE: function "e1000_has_link" has inline asm
KLEE: WARNING ONCE: function "e1000_update_stats" has inline asm
KLEE: WARNING ONCE: function "e1000_update_adaptive" has inline asm
KLEE: WARNING ONCE: function "e1000_io_slot_reset" has inline asm
KLEE: WARNING ONCE: function "e1000_io_resume" has inline asm
KLEE: WARNING ONCE: function "e1000_get_settings" has inline asm
KLEE: WARNING ONCE: function "e1000_set_settings" has inline asm
KLEE: WARNING ONCE: function "e1000_get_regs" has inline asm
KLEE: WARNING ONCE: function "e1000_set_coalesce" has inline asm
KLEE: WARNING ONCE: function "e1000_set_ringparam" has inline asm
KLEE: WARNING ONCE: function "e1000_set_pauseparam" has inline asm
KLEE: WARNING ONCE: function "e1000_diag_test" has inline asm
KLEE: WARNING ONCE: function "e1000_setup_led" has inline asm
KLEE: WARNING ONCE: function "e1000_led_on" has inline asm
KLEE: WARNING ONCE: function "e1000_led_off" has inline asm
KLEE: WARNING ONCE: function "e1000_cleanup_led" has inline asm
KLEE: WARNING ONCE: function "e1000_link_test" has inline asm
KLEE: WARNING ONCE: function "reg_pattern_test" has inline asm
KLEE: WARNING ONCE: function "reg_set_and_check" has inline asm
KLEE: WARNING ONCE: function "e1000_test_intr" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs___0" has inline asm
KLEE: WARNING ONCE: function "e1000_set_phy_loopback" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs___0" has inline asm
KLEE: WARNING ONCE: function "e1000_write_eeprom" has inline asm
KLEE: WARNING ONCE: function "e1000_wol_exclusion" has inline asm
KLEE: WARNING ONCE: function "e1000_config_collision_dist" has inline asm
KLEE: WARNING ONCE: function "e1000_io_write" has inline asm
KLEE: WARNING ONCE: function "e1000_enable_mng_pass_thru" has inline asm
KLEE: WARNING ONCE: function "ldv_irq_2" has inline asm
KLEE: WARNING ONCE: function "ldv_irq_1" 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: 3.25127220154
