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--sfc--sfc.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.: 1223 1853 18616 120860
Removed infinite loop in falcon_probe_nic
Removed infinite loop in falcon_monitor
Removed infinite loop in falcon_reconfigure_port
Removed infinite loop in efx_farch_tx_write
Removed infinite loop in efx_farch_filter_table_clear_entry
Removed infinite loop in efx_farch_filter_build
Removed infinite loop in efx_farch_rx_push_indir_table
Removed infinite loop in efx_enable_interrupts
Removed infinite loop in efx_start_all
Removed infinite loop in efx_start_port
Removed infinite loop in _efx_mcdi_rpc_finish
Removed infinite loop in efx_mcdi_send_request
Removed infinite loop in napi_enable
Removed infinite loop in dma_map_page___0
Removed infinite loop in get_page
Removed infinite loop in dma_unmap_page___0
Removed infinite loop in efx_soft_enable_interrupts
Removed infinite loop in efx_mcdi_flush_async
Removed infinite loop in efx_stop_datapath
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_unmap_page
Removed infinite loop in siena_probe_nic
Removed infinite loop in efx_siena_sriov_fini
Removed infinite loop in efx_siena_sriov_reset_tx_filter
Removed infinite loop in efx_siena_sriov_reset_rx_filter
Removed infinite loop in efx_siena_sriov_reset_vf
Removed infinite loop in efx_siena_sriov_peer_work
Removed infinite loop in efx_mcdi_fini
Removed infinite loop in efx_ef10_tx_write
Removed infinite loop in dma_sync_single_for_cpu
Removed infinite loop in efx_loopback_rx_packet
Removed infinite loop in __skb_put
Removed infinite loop in efx_ef10_link_piobufs
Removed infinite loop in efx_test_loopbacks
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in dql_queued
Removed infinite loop in dma_map_page
Removed infinite loop in efx_memcpy_toio_aligned
Removed infinite loop in efx_unregister_netdev
Removed infinite loop in efx_pci_remove_main
Removed infinite loop in efx_monitor
Removed infinite loop in efx_ptp_rx
Removed infinite loop in efx_alloc_special_buffer
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 3.7245759964
Removed calls to 'netdev_err' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'pci_dev_put' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Removed calls to 'netdev_info' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Removed calls to 'netif_schedule_queue' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to 'vfree' (function is undefined)
Removed calls to 'dump_stack' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Defining function schedule_timeout as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Defining function schedule_timeout_uninterruptible as symbolic
Defining function rps_may_expire_flow as symbolic
Removed calls to 'pci_clear_master' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function queue_work_on as symbolic
Removed calls to 'netdev_warn' (function is undefined)
Removed calls to 'down_read' (function is undefined)
Removed calls to 'up_read' (function is undefined)
Defining function rtnl_is_locked as symbolic
Removed calls to 'enable_irq' (function is undefined)
Removed calls to 'netif_tx_wake_queue' (function is undefined)
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function queue_delayed_work_on as symbolic
Removed calls to 'napi_disable' (function is undefined)
Removed calls to 'usleep_range' (function is undefined)
Removed calls to 'put_page' (function is undefined)
Removed calls to 'debug_dma_map_page' (function is undefined)
Removed calls to '__free_pages' (function is undefined)
Removed calls to 'dump_page' (function is undefined)
Defining function mod_timer as symbolic
Defining function snprintf as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to 'schedule' (function is undefined)
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Defining function __get_page_tail as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function iommu_present 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 'synchronize_irq' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function del_timer_sync as symbolic
Removed calls to 'dql_reset' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'skb_queue_purge' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Defining function skb_dequeue as symbolic
Defining function netif_receive_skb_sk as symbolic
Defining function cancel_work_sync as symbolic
Defining function cancel_delayed_work_sync as symbolic
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'pci_disable_sriov' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Defining function net_ratelimit as symbolic
Defining function pci_enable_sriov as symbolic
Defining function pci_find_ext_capability as symbolic
Defining function pci_bus_read_config_word as symbolic
Defining function dma_alloc_attrs as symbolic
Removed calls to 'getnstimeofday64' (function is undefined)
Removed calls to 'set_normalized_timespec' (function is undefined)
Defining function ns_to_timespec as symbolic
Removed calls to 'mtd_erase_callback' (function is undefined)
Defining function mtd_device_parse_register as symbolic
Defining function mtd_device_unregister as symbolic
Defining function pci_wake_from_d3 as symbolic
Defining function crc32_le as symbolic
Defining function find_first_bit as symbolic
Defining function find_next_bit as symbolic
Defining function strlcpy as symbolic
Defining function __phys_addr as symbolic
Defining function pci_reset_function as symbolic
Removed calls to 'hwmon_device_unregister' (function is undefined)
Removed calls to 'free_pages' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function hwmon_device_register_with_groups as symbolic
Defining function sprintf as symbolic
Removed calls to 'iounmap' (function is undefined)
Removed calls to 'device_remove_file' (function is undefined)
Removed calls to 'warn_slowpath_fmt' (function is undefined)
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Removed calls to 'down_write' (function is undefined)
Removed calls to 'up_write' (function is undefined)
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to 'pci_set_master' (function is undefined)
Defining function dev_close as symbolic
Defining function autoremove_wake_function as symbolic
Removed calls to 'dql_completed' (function is undefined)
Removed calls to 'debug_dma_sync_single_for_cpu' (function is undefined)
Defining function eth_type_trans as symbolic
Defining function napi_get_frags as symbolic
Defining function napi_gro_frags as symbolic
Defining function ioremap_nocache as symbolic
Defining function ioremap_wc as symbolic
Removed calls to 'destroy_workqueue' (function is undefined)
Defining function ptp_clock_unregister as symbolic
Defining function device_create_file as symbolic
Defining function __alloc_workqueue_key as symbolic
Removed calls to 'skb_queue_head' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Defining function ptp_clock_register as symbolic
Removed calls to 'ptp_clock_event' (function is undefined)
Defining function skb_checksum_help as symbolic
Defining function __pskb_pull_tail as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function pci_vfs_assigned as symbolic
Defining function pci_sriov_get_totalvfs as symbolic
Defining function pci_num_vf as symbolic
Defining function ethtool_op_get_link as symbolic
Defining function ptp_clock_index as symbolic
Defining function dev_open as symbolic
Defining function skb_put as symbolic
Removed calls to '__iowrite64_copy' (function is undefined)
Defining function skb_pad as symbolic
Removed calls to 'netif_napi_add' (function is undefined)
Removed calls to 'napi_hash_add' (function is undefined)
Removed calls to 'netif_napi_del' (function is undefined)
Removed calls to 'napi_hash_del' (function is undefined)
Defining function _raw_spin_trylock_bh as symbolic
Defining function mdio45_nway_restart as symbolic
Removed calls to 'mdio45_ethtool_gset_npage' (function is undefined)
Defining function mdio_set_flag as symbolic
Defining function mdio45_links_ok as symbolic
Defining function eth_validate_addr as symbolic
Defining function netif_set_real_num_tx_queues as symbolic
Removed calls to '__might_fault' (function is undefined)
Defining function mdio_mii_ioctl as symbolic
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Defining function scnprintf as symbolic
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'pci_release_region' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to '__bitmap_or' (function is undefined)
Removed calls to 'free_cpumask_var' (function is undefined)
Removed calls to 'netdev_rss_key_fill' (function is undefined)
Removed calls to '__init_rwsem' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Defining function pci_disable_pcie_error_reporting as symbolic
Removed calls to 'free_irq_cpu_rmap' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'pci_disable_msi' (function is undefined)
Removed calls to 'pci_disable_msix' (function is undefined)
Defining function alloc_etherdev_mqs as symbolic
Defining function pci_enable_pcie_error_reporting as symbolic
Defining function dev_alloc_name as symbolic
Defining function register_netdevice as symbolic
Defining function irq_cpu_rmap_add as symbolic
Defining function alloc_cpu_rmap as symbolic
Defining function request_threaded_irq as symbolic
Defining function netif_set_real_num_rx_queues as symbolic
Defining function pci_enable_msix_range as symbolic
Defining function pci_enable_msi_range as symbolic
Defining function zalloc_cpumask_var as symbolic
Defining function pci_enable_device as symbolic
Defining function dma_supported as symbolic
Defining function pci_request_region as symbolic
Defining function dma_set_mask as symbolic
Defining function pci_read_vpd as symbolic
Defining function pci_vpd_find_tag as symbolic
Defining function pci_vpd_find_info_keyword as symbolic
Defining function mutex_trylock as symbolic
Defining function pci_cleanup_aer_uncorrect_error_status as symbolic
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_set_power_state as symbolic
Removed calls to 'i2c_unregister_device' (function is undefined)
Defining function i2c_smbus_read_byte_data as symbolic
Defining function i2c_new_device as symbolic
Defining function i2c_smbus_write_byte_data as symbolic
Defining function i2c_new_dummy as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function _cond_resched as symbolic
Defining function round_jiffies_up as symbolic
Defining function pci_dev_get as symbolic
Defining function pci_get_device as symbolic
Defining function i2c_bit_add_bus 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_suspend_late_33 as symbolic
Defining function ldv_restore_early_33 as symbolic
Defining function ldv_resume_early_33 as symbolic
Defining function ldv_thaw_early_33 as symbolic
Defining function ldv_resume_noirq_33 as symbolic
Defining function ldv_freeze_noirq_33 as symbolic
Defining function ldv_prepare_33 as symbolic
Defining function ldv_freeze_late_33 as symbolic
Defining function ldv_thaw_noirq_33 as symbolic
Defining function ldv_poweroff_noirq_33 as symbolic
Defining function ldv_poweroff_late_33 as symbolic
Defining function ldv_restore_noirq_33 as symbolic
Defining function ldv_suspend_noirq_33 as symbolic
Defining function ldv_complete_33 as symbolic
Defining function ldv_suspend_32 as symbolic
Defining function ldv_release_32 as symbolic
Defining function ldv_probe_32 as symbolic
Defining function ldv_shutdown_31 as symbolic
Defining function ldv_ndo_uninit_38 as symbolic
Defining function ldv_ndo_init_38 as symbolic
Defining function ldv_release_34 as symbolic
Defining function ldv_setup_34 as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function unregister_netdevice_notifier as symbolic
Defining function __pci_register_driver as symbolic
Removed calls to 'flush_workqueue' (function is undefined)
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strchr
  strcmp
  strcpy
  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: 4.01811814308
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 1227 1404 9839 73665
INFO: Starting verification
KLEE: WARNING ONCE: function "falcon_probe_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_init_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_irq_ack_a1" has inline asm
KLEE: WARNING ONCE: function "falcon_monitor" has inline asm
KLEE: WARNING ONCE: function "falcon_handle_global_event" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fini_dmaq" has inline asm
KLEE: WARNING ONCE: function "falcon_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "falcon_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "falcon_reconfigure_xmac" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_enable_master" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_test_generate" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_disable_master" has inline asm
KLEE: WARNING ONCE: function "efx_farch_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "falcon_legacy_interrupt_a1" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_write" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_write" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_defer_refill" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_process" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_read_ack" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_test_generate" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_probe" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_restore" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_insert" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_get_safe" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_count_rx_used" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_get_rx_ids" has inline asm
KLEE: WARNING ONCE: function "falcon_mtd_erase" has inline asm
KLEE: WARNING ONCE: function "falcon_mtd_write" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_slow_wait" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_cmd" has inline asm
KLEE: WARNING ONCE: function "falcon_b0_test_chip" has inline asm
KLEE: WARNING ONCE: function "efx_farch_legacy_interrupt" has inline asm
KLEE: WARNING ONCE: function "falcon_b0_rx_push_rss_config" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_update_rx_scatter" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_rfs_expire_one" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_clear_entry" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_push_tx_limits" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_push_rx_config" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_build" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_push_indir_table" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fatal_interrupt" has inline asm
KLEE: WARNING ONCE: function "napi_schedule" has inline asm
KLEE: WARNING ONCE: function "efx_schedule_reset" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_complete_sync" has inline asm
KLEE: WARNING ONCE: function "efx_farch_test_registers" has inline asm
KLEE: WARNING ONCE: function "efx_enable_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_start_all" has inline asm
KLEE: WARNING ONCE: function "efx_init_rx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_fast_push_rx_descriptors" has inline asm
KLEE: WARNING ONCE: function "efx_start_eventq" has inline asm
KLEE: WARNING ONCE: function "_efx_mcdi_rpc_finish" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_poll_once" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_send_request" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_acquire_sync" has inline asm
KLEE: WARNING ONCE: function "efx_soft_enable_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_reado___0" has inline asm
KLEE: WARNING ONCE: function "efx_stop_all" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_flush_async" has inline asm
KLEE: WARNING ONCE: function "efx_fini_tx_queue" has inline asm
KLEE: WARNING ONCE: function "falcon_drain_tx_fifo" has inline asm
KLEE: WARNING ONCE: function "falcon_reset_macs" has inline asm
KLEE: WARNING ONCE: function "falcon_setup_xaui" has inline asm
KLEE: WARNING ONCE: function "siena_probe_nic" has inline asm
KLEE: WARNING ONCE: function "siena_init_nic" has inline asm
KLEE: WARNING ONCE: function "siena_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "siena_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_request" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_poll_response" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_read_response" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_poll_reboot" has inline asm
KLEE: WARNING ONCE: function "siena_rx_push_rss_config" has inline asm
KLEE: WARNING ONCE: function "siena_ptp_write_host_time" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_init" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_fini" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_reset" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_reset_vf" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_memcpy" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_bufs" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_peer_work" has inline asm
KLEE: WARNING ONCE: function "__efx_siena_sriov_push_vf_status" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_synchronize" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_sync_rx_mode" has inline asm
KLEE: WARNING ONCE: function "efx_farch_init_common" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fpga_ver" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_mon_probe" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_update_stats_vf" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_request" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_poll_response" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_poll_reboot" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_legacy_interrupt" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_tx_init" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_tx_write" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_rx_write" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ev_process" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ev_read_ack" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_filter_insert" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_set_mac_address" has inline asm
KLEE: WARNING ONCE: function "efx_device_detach_sync___2" has inline asm
KLEE: WARNING ONCE: function "efx_reset" has inline asm
KLEE: WARNING ONCE: function "efx_device_detach_sync" has inline asm
KLEE: WARNING ONCE: function "_efx_mcdi_rpc_async" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_filter_remove_internal" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_process_event" has inline asm
KLEE: WARNING ONCE: function "efx_xmit_done" has inline asm
KLEE: WARNING ONCE: function "efx_loopback_rx_packet" has inline asm
KLEE: WARNING ONCE: function "efx_rx_deliver" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_complete_async" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_handle_drain_event" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_alloc_rss_context" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_link_piobufs" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_probe" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_update_stats_pf" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ptp_write_host_time" has inline asm
KLEE: WARNING ONCE: function "efx_selftest" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock_bh___1" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock_bh___1" has inline asm
KLEE: WARNING ONCE: function "efx_enqueue_skb" has inline asm
KLEE: WARNING ONCE: function "netdev_tx_sent_queue" has inline asm
KLEE: WARNING ONCE: function "efx_tx_maybe_stop_queue" has inline asm
KLEE: WARNING ONCE: function "efx_memcpy_toio_aligned" has inline asm
KLEE: WARNING ONCE: function "efx_probe_channel" has inline asm
KLEE: WARNING ONCE: function "efx_probe_tx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_probe_rx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_get_regs" has inline asm
KLEE: WARNING ONCE: function "efx_reado" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_test_alive" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_check_mmds" has inline asm
KLEE: WARNING ONCE: function "falcon_reset_xaui" has inline asm
KLEE: WARNING ONCE: function "efx_pci_probe" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove_main" has inline asm
KLEE: WARNING ONCE: function "efx_reset_work" has inline asm
KLEE: WARNING ONCE: function "efx_monitor" has inline asm
KLEE: WARNING ONCE: function "falcon_setsda" has inline asm
KLEE: WARNING ONCE: function "falcon_setscl" has inline asm
KLEE: WARNING ONCE: function "efx_reado___1" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_rx" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_evq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_rxq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_txq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_fini_all_queues" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_read" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_remove" has inline asm
KLEE: WARNING ONCE: function "efx_farch_handle_drain_event" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_tx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_rx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_fini_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_init_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_alloc_special_buffer" has inline asm
KLEE: WARNING ONCE: function "falcon_xmac_link_ok" has inline asm
KLEE: WARNING ONCE: function "falcon_ack_status_intr" has inline asm
KLEE: WARNING ONCE: function "falcon_deconfigure_mac_wrapper" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_complete" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_request" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_flush_rxqs" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_fini" has inline asm
KLEE: WARNING ONCE: function "falcon_mdio_read" has inline asm
KLEE: WARNING ONCE: function "falcon_mdio_write" has inline asm
KLEE: WARNING ONCE: function "falcon_gmii_wait" has inline asm
KLEE: WARNING ONCE: function "__falcon_reset_hw" has inline asm
KLEE: WARNING ONCE: function "efx_farch_generate_event" has inline asm
KLEE: WARNING ONCE: function "efx_time_sync_event" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_30" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_27" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_28" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_24" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_23" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_29" 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-LeGs6P/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "falcon_probe_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_init_nic" has inline asm
KLEE: WARNING ONCE: function "falcon_irq_ack_a1" has inline asm
KLEE: WARNING ONCE: function "falcon_monitor" has inline asm
KLEE: WARNING ONCE: function "falcon_handle_global_event" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fini_dmaq" has inline asm
KLEE: WARNING ONCE: function "falcon_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "falcon_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "falcon_reconfigure_xmac" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_enable_master" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_test_generate" has inline asm
KLEE: WARNING ONCE: function "efx_farch_irq_disable_master" has inline asm
KLEE: WARNING ONCE: function "efx_farch_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "falcon_legacy_interrupt_a1" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_write" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_write" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_defer_refill" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_init" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_process" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_read_ack" has inline asm
KLEE: WARNING ONCE: function "efx_farch_ev_test_generate" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_probe" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_restore" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_insert" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_get_safe" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_count_rx_used" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_get_rx_ids" has inline asm
KLEE: WARNING ONCE: function "falcon_mtd_erase" has inline asm
KLEE: WARNING ONCE: function "falcon_mtd_write" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_slow_wait" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_cmd" has inline asm
KLEE: WARNING ONCE: function "falcon_b0_test_chip" has inline asm
KLEE: WARNING ONCE: function "efx_farch_legacy_interrupt" has inline asm
KLEE: WARNING ONCE: function "falcon_b0_rx_push_rss_config" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_update_rx_scatter" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_rfs_expire_one" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_table_clear_entry" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_push_tx_limits" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_push_rx_config" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_build" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_push_indir_table" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fatal_interrupt" has inline asm
KLEE: WARNING ONCE: function "napi_schedule" has inline asm
KLEE: WARNING ONCE: function "efx_schedule_reset" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_complete_sync" has inline asm
KLEE: WARNING ONCE: function "efx_farch_test_registers" has inline asm
KLEE: WARNING ONCE: function "efx_enable_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_start_all" has inline asm
KLEE: WARNING ONCE: function "efx_init_rx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_fast_push_rx_descriptors" has inline asm
KLEE: WARNING ONCE: function "efx_start_eventq" has inline asm
KLEE: WARNING ONCE: function "_efx_mcdi_rpc_finish" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_poll_once" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_send_request" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_acquire_sync" has inline asm
KLEE: WARNING ONCE: function "efx_soft_enable_interrupts" has inline asm
KLEE: WARNING ONCE: function "efx_reado___0" has inline asm
KLEE: WARNING ONCE: function "efx_stop_all" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_flush_async" has inline asm
KLEE: WARNING ONCE: function "efx_fini_tx_queue" has inline asm
KLEE: WARNING ONCE: function "falcon_drain_tx_fifo" has inline asm
KLEE: WARNING ONCE: function "falcon_reset_macs" has inline asm
KLEE: WARNING ONCE: function "falcon_setup_xaui" has inline asm
KLEE: WARNING ONCE: function "siena_probe_nic" has inline asm
KLEE: WARNING ONCE: function "siena_init_nic" has inline asm
KLEE: WARNING ONCE: function "siena_update_nic_stats" has inline asm
KLEE: WARNING ONCE: function "siena_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_request" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_poll_response" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_read_response" has inline asm
KLEE: WARNING ONCE: function "siena_mcdi_poll_reboot" has inline asm
KLEE: WARNING ONCE: function "siena_rx_push_rss_config" has inline asm
KLEE: WARNING ONCE: function "siena_ptp_write_host_time" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_init" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_fini" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_reset" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_reset_vf" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_memcpy" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_bufs" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_peer_work" has inline asm
KLEE: WARNING ONCE: function "__efx_siena_sriov_push_vf_status" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_synchronize" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_sync_rx_mode" has inline asm
KLEE: WARNING ONCE: function "efx_farch_init_common" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_fpga_ver" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_mon_probe" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_update_stats_vf" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_push_irq_moderation" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_request" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_poll_response" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_mcdi_poll_reboot" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_msi_interrupt" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_legacy_interrupt" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_tx_init" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_tx_write" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_rx_write" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ev_process" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ev_read_ack" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_filter_insert" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_set_mac_address" has inline asm
KLEE: WARNING ONCE: function "efx_device_detach_sync___2" has inline asm
KLEE: WARNING ONCE: function "efx_reset" has inline asm
KLEE: WARNING ONCE: function "efx_device_detach_sync" has inline asm
KLEE: WARNING ONCE: function "_efx_mcdi_rpc_async" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_filter_remove_internal" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_process_event" has inline asm
KLEE: WARNING ONCE: function "efx_xmit_done" has inline asm
KLEE: WARNING ONCE: function "efx_loopback_rx_packet" has inline asm
KLEE: WARNING ONCE: function "efx_rx_deliver" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_complete_async" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_handle_drain_event" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_alloc_rss_context" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_link_piobufs" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_probe" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_update_stats_pf" has inline asm
KLEE: WARNING ONCE: function "efx_ef10_ptp_write_host_time" has inline asm
KLEE: WARNING ONCE: function "efx_selftest" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock_bh___1" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock_bh___1" has inline asm
KLEE: WARNING ONCE: function "efx_enqueue_skb" has inline asm
KLEE: WARNING ONCE: function "netdev_tx_sent_queue" has inline asm
KLEE: WARNING ONCE: function "efx_tx_maybe_stop_queue" has inline asm
KLEE: WARNING ONCE: function "efx_memcpy_toio_aligned" has inline asm
KLEE: WARNING ONCE: function "efx_probe_channel" has inline asm
KLEE: WARNING ONCE: function "efx_probe_tx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_probe_rx_queue" has inline asm
KLEE: WARNING ONCE: function "efx_nic_get_regs" has inline asm
KLEE: WARNING ONCE: function "efx_reado" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_test_alive" has inline asm
KLEE: WARNING ONCE: function "efx_mdio_check_mmds" has inline asm
KLEE: WARNING ONCE: function "falcon_reset_xaui" has inline asm
KLEE: WARNING ONCE: function "efx_pci_probe" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove" has inline asm
KLEE: WARNING ONCE: function "efx_pci_remove_main" has inline asm
KLEE: WARNING ONCE: function "efx_reset_work" has inline asm
KLEE: WARNING ONCE: function "efx_monitor" has inline asm
KLEE: WARNING ONCE: function "falcon_setsda" has inline asm
KLEE: WARNING ONCE: function "falcon_setscl" has inline asm
KLEE: WARNING ONCE: function "efx_reado___1" has inline asm
KLEE: WARNING ONCE: function "efx_ptp_rx" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_evq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_rxq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_init_txq" has inline asm
KLEE: WARNING ONCE: function "efx_vfdi_fini_all_queues" has inline asm
KLEE: WARNING ONCE: function "falcon_spi_read" has inline asm
KLEE: WARNING ONCE: function "efx_farch_filter_remove" has inline asm
KLEE: WARNING ONCE: function "efx_farch_handle_drain_event" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_tx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_siena_sriov_rx_flush_done" has inline asm
KLEE: WARNING ONCE: function "efx_fini_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_init_special_buffer" has inline asm
KLEE: WARNING ONCE: function "efx_alloc_special_buffer" has inline asm
KLEE: WARNING ONCE: function "falcon_xmac_link_ok" has inline asm
KLEE: WARNING ONCE: function "falcon_ack_status_intr" has inline asm
KLEE: WARNING ONCE: function "falcon_deconfigure_mac_wrapper" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_complete" has inline asm
KLEE: WARNING ONCE: function "falcon_stats_request" has inline asm
KLEE: WARNING ONCE: function "efx_mcdi_flush_rxqs" has inline asm
KLEE: WARNING ONCE: function "efx_farch_rx_fini" has inline asm
KLEE: WARNING ONCE: function "efx_farch_tx_fini" has inline asm
KLEE: WARNING ONCE: function "falcon_mdio_read" has inline asm
KLEE: WARNING ONCE: function "falcon_mdio_write" has inline asm
KLEE: WARNING ONCE: function "falcon_gmii_wait" has inline asm
KLEE: WARNING ONCE: function "__falcon_reset_hw" has inline asm
KLEE: WARNING ONCE: function "efx_farch_generate_event" has inline asm
KLEE: WARNING ONCE: function "efx_time_sync_event" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_30" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_27" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_28" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_24" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_23" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_29" 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: 8.97385215759
