bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--ethernet--stmicro--stmmac--stmmac.ko-entry_point_false-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.: 408 632 4534 33983
Removed infinite loop in dma_map_single_attrs___0
Removed infinite loop in dma_unmap_single_attrs
Removed infinite loop in dma_map_single_attrs
Removed infinite loop in napi_enable
Removed infinite loop in dma_map_page
Removed infinite loop in arch_local_save_flags
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 1.17609095573
Removed calls to 'debug_dma_map_page' (function is undefined)
Defining function __phys_addr as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function printk as symbolic
Removed calls to 'netif_carrier_off' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'clk_disable' (function is undefined)
Removed calls to 'clk_unprepare' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to 'mdiobus_unregister' (function is undefined)
Removed calls to 'mdiobus_free' (function is undefined)
Defining function reset_control_assert as symbolic
Defining function platform_get_resource as symbolic
Defining function devm_ioremap_resource as symbolic
Removed calls to 'ether_setup' (function is undefined)
Defining function platform_get_irq_byname as symbolic
Defining function netdev_err as symbolic
Defining function alloc_etherdev_mqs as symbolic
Defining function devm_clk_get as symbolic
Defining function dev_warn as symbolic
Defining function devm_reset_control_get as symbolic
Defining function _dev_info as symbolic
Defining function reset_control_deassert as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function snprintf as symbolic
Defining function mdiobus_register as symbolic
Defining function sprintf as symbolic
Defining function mdiobus_alloc_size as symbolic
Defining function clk_get_rate as symbolic
Defining function register_netdev as symbolic
Removed calls to 'debug_dma_unmap_page' (function is undefined)
Defining function __netdev_alloc_skb as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Defining function mod_timer as symbolic
Defining function clk_prepare as symbolic
Defining function clk_enable as symbolic
Defining function devm_kmalloc as symbolic
Removed calls to 'pci_set_master' (function is undefined)
Removed calls to 'pci_clear_master' (function is undefined)
Removed calls to 'pci_release_regions' (function is undefined)
Removed calls to 'pci_disable_device' (function is undefined)
Removed calls to 'pci_iounmap' (function is undefined)
Removed calls to 'pci_restore_state' (function is undefined)
Defining function pci_set_power_state as symbolic
Removed calls to 'netif_device_attach' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to 'phy_start' (function is undefined)
Defining function pinctrl_pm_select_default_state as symbolic
Removed calls to 'debug_dma_mapping_error' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'debugfs_remove' (function is undefined)
Removed calls to 'add_timer' (function is undefined)
Defining function usecs_to_jiffies as symbolic
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to 'skb_tstamp_tx' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function phy_init_eee as symbolic
Defining function del_timer_sync as symbolic
Defining function debugfs_create_dir as symbolic
Defining function debugfs_create_file as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function ptp_clock_register as symbolic
Removed calls to 'phy_stop' (function is undefined)
Removed calls to 'netif_device_detach' (function is undefined)
Defining function pci_save_state as symbolic
Defining function pci_choose_state as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Defining function pinctrl_pm_select_sleep_state as symbolic
Defining function pci_enable_device as symbolic
Defining function pci_request_regions as symbolic
Defining function pci_iomap as symbolic
Defining function dev_err as symbolic
Defining function regmap_read as symbolic
Defining function regmap_write as symbolic
Defining function syscon_regmap_lookup_by_phandle as symbolic
Defining function eth_mac_addr as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to 'getnstimeofday' (function is undefined)
Removed calls to 'netdev_update_features' (function is undefined)
Removed calls to 'disable_irq' (function is undefined)
Removed calls to 'enable_irq' (function is undefined)
Removed calls to 'pm_wakeup_event' (function is undefined)
Removed calls to '__napi_schedule' (function is undefined)
Defining function phy_mii_ioctl as symbolic
Defining function netdev_alert as symbolic
Defining function _copy_to_user as symbolic
Defining function _copy_from_user as symbolic
Removed calls to 'free_irq' (function is undefined)
Defining function ptp_clock_unregister as symbolic
Removed calls to 'debug_dma_free_coherent' (function is undefined)
Defining function request_threaded_irq as symbolic
Removed calls to 'debug_dma_alloc_coherent' (function is undefined)
Removed calls to 'phy_print_status' (function is undefined)
Defining function phy_connect as symbolic
Defining function seq_lseek as symbolic
Defining function seq_read as symbolic
Defining function single_release as symbolic
Defining function single_open as symbolic
Defining function seq_printf as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Defining function ethtool_op_get_link as symbolic
Defining function phy_ethtool_set_eee as symbolic
Defining function phy_ethtool_get_eee as symbolic
Defining function ptp_clock_index as symbolic
Defining function ethtool_op_get_ts_info as symbolic
Defining function phy_get_eee_err as symbolic
Defining function phy_start_aneg as symbolic
Defining function device_set_wakeup_enable as symbolic
Defining function irq_set_irq_wake as symbolic
Defining function strlcpy as symbolic
Defining function phy_ethtool_sset as symbolic
Defining function phy_ethtool_gset as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'phy_disconnect' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'skb_clone_tx_timestamp' (function is undefined)
Removed calls to 'platform_driver_unregister' (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_uninit_21 as symbolic
Defining function ldv_ndo_init_21 as symbolic
Defining function ldv_release_14 as symbolic
Defining function ldv_setup_14 as symbolic
Defining function ldv_suspend_late_9 as symbolic
Defining function ldv_restore_early_9 as symbolic
Defining function ldv_resume_early_9 as symbolic
Defining function ldv_thaw_early_9 as symbolic
Defining function ldv_resume_noirq_9 as symbolic
Defining function ldv_freeze_noirq_9 as symbolic
Defining function ldv_prepare_9 as symbolic
Defining function ldv_freeze_late_9 as symbolic
Defining function ldv_thaw_noirq_9 as symbolic
Defining function ldv_poweroff_noirq_9 as symbolic
Defining function ldv_poweroff_late_9 as symbolic
Defining function ldv_restore_noirq_9 as symbolic
Defining function ldv_suspend_noirq_9 as symbolic
Defining function ldv_complete_9 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_init_6 as symbolic
Defining function ldv_release_16 as symbolic
Defining function ldv_setup_16 as symbolic
Defining function __pci_register_driver as symbolic
Defining function __platform_driver_register as symbolic
Defining function ldv_release_18 as symbolic
Defining function ldv_setup_18 as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_clone as symbolic
Defining function skb_copy as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_u32_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 1.06906890869
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 540 547 2698 18054
INFO: Starting verification
KLEE: WARNING ONCE: function "stmmac_jumbo_frm" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_dma_init" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_dump_dma_regs" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_dma_operation_mode" has inline asm
KLEE: WARNING ONCE: function "dwmac_enable_dma_transmission" has inline asm
KLEE: WARNING ONCE: function "dwmac_enable_dma_irq" has inline asm
KLEE: WARNING ONCE: function "dwmac_disable_dma_irq" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_start_tx" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_stop_tx" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_start_rx" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_stop_rx" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_interrupt" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_get_hw_feature" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_rx_watchdog" has inline asm
KLEE: WARNING ONCE: function "dwmac100_dma_init" has inline asm
KLEE: WARNING ONCE: function "dwmac100_dma_operation_mode" has inline asm
KLEE: WARNING ONCE: function "dwmac100_dma_diagnostic_fr" has inline asm
KLEE: WARNING ONCE: function "enh_desc_get_tx_status" has inline asm
KLEE: WARNING ONCE: function "stmmac_config_hw_tstamping" has inline asm
KLEE: WARNING ONCE: function "stmmac_config_sub_second_increment" has inline asm
KLEE: WARNING ONCE: function "stmmac_init_systime" has inline asm
KLEE: WARNING ONCE: function "stmmac_config_addend" has inline asm
KLEE: WARNING ONCE: function "stmmac_adjust_systime" has inline asm
KLEE: WARNING ONCE: function "stmmac_get_systime" has inline asm
KLEE: WARNING ONCE: function "stmmac_dvr_remove" has inline asm
KLEE: WARNING ONCE: function "stmmac_dvr_probe" has inline asm
KLEE: WARNING ONCE: function "stmmac_resume" has inline asm
KLEE: WARNING ONCE: function "stmmac_mdio_reset" has inline asm
KLEE: WARNING ONCE: function "stmmac_hw_setup" has inline asm
KLEE: WARNING ONCE: function "napi_enable" has inline asm
KLEE: WARNING ONCE: function "dma_map_single_attrs" has inline asm
KLEE: WARNING ONCE: function "stmmac_tx_timer" has inline asm
KLEE: WARNING ONCE: function "dma_unmap_single_attrs" has inline asm
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "stmmac_suspend" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" has inline asm
KLEE: WARNING ONCE: function "napi_disable" has inline asm
KLEE: WARNING ONCE: function "stmmac_ethtool_gregs" has inline asm
KLEE: WARNING ONCE: function "dwmac_mmc_read" has inline asm
KLEE: WARNING ONCE: function "dwmac_dma_flush_tx_fifo" has inline asm
KLEE: WARNING ONCE: function "stmmac_set_mac" has inline asm
KLEE: WARNING ONCE: function "stmmac_mdio_read" has inline asm
KLEE: WARNING ONCE: function "stmmac_mdio_write" has inline asm
KLEE: WARNING ONCE: function "dwmac1000_setup" has inline asm
KLEE: WARNING ONCE: function "dwmac_mmc_intr_all_mask" has inline asm
KLEE: WARNING ONCE: function "dwmac_mmc_ctrl" has inline asm
KLEE: WARNING ONCE: function "stmmac_interrupt" has inline asm
KLEE: WARNING ONCE: function "stmmac_get_mac_addr" has inline asm
KLEE: WARNING ONCE: function "stmmac_set_mac_addr" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_11" has inline asm
KLEE: WARNING ONCE: function "stmmac_adjust_link" has inline asm
KLEE: WARNING ONCE: function "dma_free_attrs" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_17" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_16" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_14" has inline asm
KLEE: WARNING ONCE: function "ldv_main_exported_15" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_b7efbf31-1442-4684-b693-061636594a8f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOGRcr/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--ethernet--stmicro--stmmac--stmmac.ko-entry_point_false-unreach-call.cil.out.c:12085: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-BOGRcr/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--ethernet--stmicro--stmmac--stmmac.ko-entry_point_false-unreach-call.cil.out.c:12238: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17805 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 22430 states (over memory cap)
KLEE: WARNING: killing 21992 states (over memory cap)
KLEE: WARNING: killing 21840 states (over memory cap)
KLEE: WARNING: killing 22260 states (over memory cap)
KLEE: WARNING: killing 22360 states (over memory cap)
KLEE: WARNING: killing 24015 states (over memory cap)
KLEE: WARNING: killing 25427 states (over memory cap)
KLEE: WARNING: killing 24264 states (over memory cap)
KLEE: WARNING: killing 24701 states (over memory cap)
KLEE: WARNING: killing 25743 states (over memory cap)
KLEE: WARNING: killing 25284 states (over memory cap)
KLEE: WARNING: killing 25583 states (over memory cap)
KLEE: WARNING: killing 23682 states (over memory cap)
KLEE: WARNING: killing 23560 states (over memory cap)
KLEE: WARNING: killing 23103 states (over memory cap)
KLEE: WARNING: killing 24137 states (over memory cap)
KLEE: WARNING: killing 24948 states (over memory cap)
KLEE: WARNING: killing 23067 states (over memory cap)
KLEE: WARNING: killing 23920 states (over memory cap)
KLEE: WARNING: killing 23293 states (over memory cap)
KLEE: WARNING: killing 25018 states (over memory cap)
KLEE: WARNING: killing 25312 states (over memory cap)
KLEE: WARNING: killing 23627 states (over memory cap)
KLEE: WARNING: killing 24614 states (over memory cap)
KLEE: WARNING: killing 25091 states (over memory cap)
KLEE: WARNING: killing 24523 states (over memory cap)
KLEE: WARNING: killing 23441 states (over memory cap)
KLEE: WARNING: killing 24380 states (over memory cap)
KLEE: WARNING: killing 24448 states (over memory cap)
KLEE: WARNING: killing 23140 states (over memory cap)
KLEE: WARNING: killing 25082 states (over memory cap)
KLEE: WARNING: killing 25281 states (over memory cap)
KLEE: WARNING: killing 24210 states (over memory cap)
KLEE: WARNING: killing 23690 states (over memory cap)
KLEE: WARNING: killing 24437 states (over memory cap)
KLEE: WARNING: killing 24418 states (over memory cap)
KLEE: WARNING: killing 24352 states (over memory cap)
KLEE: WARNING: killing 23275 states (over memory cap)
KLEE: WARNING: killing 24711 states (over memory cap)
KLEE: WARNING: killing 22910 states (over memory cap)
KLEE: WARNING: killing 25800 states (over memory cap)
KLEE: WARNING: killing 24282 states (over memory cap)
KLEE: WARNING: killing 24351 states (over memory cap)
KLEE: WARNING: killing 24278 states (over memory cap)
KLEE: WARNING: killing 24305 states (over memory cap)
KLEE: WARNING: killing 25412 states (over memory cap)
KLEE: WARNING: killing 24257 states (over memory cap)
KLEE: WARNING: killing 23739 states (over memory cap)
KLEE: WARNING: killing 24392 states (over memory cap)
KLEE: WARNING: killing 24058 states (over memory cap)
KLEE: WARNING: killing 24938 states (over memory cap)
KLEE: WARNING: killing 24015 states (over memory cap)
KLEE: WARNING: killing 24531 states (over memory cap)
KLEE: WARNING: killing 24198 states (over memory cap)
KLEE: WARNING: killing 24987 states (over memory cap)
KLEE: WARNING: killing 24653 states (over memory cap)
KLEE: WARNING: killing 25310 states (over memory cap)
KLEE: WARNING: killing 23186 states (over memory cap)
KLEE: WARNING: killing 23204 states (over memory cap)
KLEE: WARNING: killing 24564 states (over memory cap)
KLEE: WARNING: killing 24942 states (over memory cap)
KLEE: WARNING: killing 24567 states (over memory cap)
KLEE: WARNING: killing 23344 states (over memory cap)
KLEE: WARNING: killing 24204 states (over memory cap)
KLEE: WARNING: killing 23425 states (over memory cap)
KLEE: WARNING: killing 24910 states (over memory cap)
KLEE: WARNING: killing 23785 states (over memory cap)
KLEE: WARNING: killing 25305 states (over memory cap)
KLEE: WARNING: killing 24133 states (over memory cap)
KLEE: WARNING: killing 25169 states (over memory cap)
KLEE: WARNING: killing 24125 states (over memory cap)
KLEE: WARNING: killing 25116 states (over memory cap)
KLEE: WARNING: killing 23863 states (over memory cap)
KLEE: WARNING: killing 24058 states (over memory cap)
KLEE: WARNING: killing 24339 states (over memory cap)
KLEE: WARNING: killing 25151 states (over memory cap)
KLEE: WARNING: killing 23987 states (over memory cap)
KLEE: WARNING: killing 24317 states (over memory cap)
KLEE: WARNING: killing 25206 states (over memory cap)
KLEE: WARNING: killing 23518 states (over memory cap)
KLEE: WARNING: killing 23757 states (over memory cap)
KLEE: WARNING: killing 24213 states (over memory cap)
KLEE: WARNING: killing 24408 states (over memory cap)
KLEE: WARNING: killing 24037 states (over memory cap)
KLEE: WARNING: killing 24797 states (over memory cap)
KLEE: WARNING: killing 24557 states (over memory cap)
KLEE: WARNING: killing 23875 states (over memory cap)
KLEE: WARNING: killing 24998 states (over memory cap)
KLEE: WARNING: killing 24583 states (over memory cap)
KLEE: WARNING: killing 24824 states (over memory cap)
KLEE: WARNING: killing 24194 states (over memory cap)
KLEE: WARNING: killing 23822 states (over memory cap)
KLEE: WARNING: killing 24013 states (over memory cap)
KLEE: WARNING: killing 22875 states (over memory cap)
KLEE: WARNING: killing 24321 states (over memory cap)
KLEE: WARNING: killing 25633 states (over memory cap)
