bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-usb-asix_true-unreach-call.cil.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.: 284 357 2168 13048
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.502560138702
Defining function usbnet_get_settings as symbolic
Removed calls to 'usbnet_unlink_rx_urbs' (function is undefined)
Removed calls to 'usbnet_update_max_qlen' (function is undefined)
Defining function netdev_err as symbolic
Defining function usbnet_write_cmd as symbolic
Defining function usbnet_read_cmd as symbolic
Defining function generic_mii_ioctl as symbolic
Defining function eth_mac_addr as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Defining function usbnet_write_cmd_async as symbolic
Defining function usbnet_nway_reset as symbolic
Defining function usbnet_set_settings as symbolic
Defining function mii_check_media as symbolic
Defining function mii_ethtool_gset as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to '__const_udelay' (function is undefined)
Defining function mii_nway_restart as symbolic
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'usbnet_skb_return' (function is undefined)
Defining function skb_put as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'usbnet_link_change' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'mdiobus_free' (function is undefined)
Removed calls to 'mdiobus_unregister' (function is undefined)
Removed calls to 'phy_start' (function is undefined)
Removed calls to 'phy_stop' (function is undefined)
Removed calls to 'phy_disconnect' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function skb_push as symbolic
Defining function netdev_info as symbolic
Defining function snprintf as symbolic
Removed calls to 'phy_print_status' (function is undefined)
Defining function phy_connect as symbolic
Defining function genphy_resume as symbolic
Defining function usbnet_get_endpoints as symbolic
Defining function mdiobus_register as symbolic
Defining function mdiobus_alloc_size as symbolic
Removed calls to 'usbnet_get_drvinfo' (function is undefined)
Defining function strlcpy as symbolic
Defining function usbnet_get_link as symbolic
Defining function usbnet_get_msglevel as symbolic
Defining function usbnet_open as symbolic
Defining function usbnet_start_xmit as symbolic
Defining function usbnet_stop as symbolic
Defining function eth_validate_addr as symbolic
Defining function phy_start_aneg as symbolic
Defining function phy_ethtool_sset as symbolic
Defining function usbnet_change_mtu as symbolic
Defining function phy_mii_ioctl as symbolic
Defining function usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function usbnet_resume as symbolic
Removed calls to 'get_random_bytes' (function is undefined)
Defining function mii_link_ok as symbolic
Defining function phy_ethtool_gset as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usbnet_tx_timeout' (function is undefined)
Removed calls to 'usbnet_set_msglevel' (function is undefined)
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  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.452241897583
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 269 364 960 6450
INFO: Starting verification
KLEE: WARNING: undefined reference to function: usbnet_disconnect
KLEE: WARNING: undefined reference to function: usbnet_set_msglevel
KLEE: WARNING: undefined reference to function: usbnet_tx_timeout
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_cfb3f045-544d-4431-9f0e-1823ae928292/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 24956 states (over memory cap)
KLEE: WARNING: killing 23392 states (over memory cap)
KLEE: WARNING: killing 23119 states (over memory cap)
KLEE: WARNING: killing 23935 states (over memory cap)
KLEE: WARNING: killing 22939 states (over memory cap)
KLEE: WARNING: killing 22137 states (over memory cap)
KLEE: WARNING: killing 22047 states (over memory cap)
KLEE: WARNING: killing 22147 states (over memory cap)
KLEE: WARNING: killing 22258 states (over memory cap)
KLEE: WARNING: killing 21997 states (over memory cap)
KLEE: WARNING: killing 22103 states (over memory cap)
KLEE: WARNING: killing 22394 states (over memory cap)
KLEE: WARNING: killing 23027 states (over memory cap)
KLEE: WARNING: killing 23296 states (over memory cap)
KLEE: WARNING: killing 23925 states (over memory cap)
KLEE: WARNING: killing 24724 states (over memory cap)
KLEE: WARNING: killing 24989 states (over memory cap)
KLEE: WARNING: killing 25102 states (over memory cap)
KLEE: WARNING: killing 25021 states (over memory cap)
KLEE: WARNING: killing 25108 states (over memory cap)
KLEE: WARNING: killing 25390 states (over memory cap)
KLEE: WARNING: killing 25496 states (over memory cap)
KLEE: WARNING: killing 25428 states (over memory cap)
KLEE: WARNING: killing 25192 states (over memory cap)
KLEE: WARNING: killing 25641 states (over memory cap)
KLEE: WARNING: killing 25243 states (over memory cap)
KLEE: WARNING: killing 25511 states (over memory cap)
KLEE: WARNING: killing 25295 states (over memory cap)
KLEE: WARNING: killing 25398 states (over memory cap)
KLEE: WARNING: killing 25167 states (over memory cap)
KLEE: WARNING: killing 24437 states (over memory cap)
KLEE: WARNING: killing 23699 states (over memory cap)
KLEE: WARNING: killing 23638 states (over memory cap)
KLEE: WARNING: killing 23415 states (over memory cap)
KLEE: WARNING: killing 24024 states (over memory cap)
KLEE: WARNING: killing 23799 states (over memory cap)
KLEE: WARNING: killing 23577 states (over memory cap)
KLEE: WARNING: killing 23354 states (over memory cap)
KLEE: WARNING: killing 23636 states (over memory cap)
KLEE: WARNING: killing 24071 states (over memory cap)
KLEE: WARNING: killing 23039 states (over memory cap)
KLEE: WARNING: killing 23637 states (over memory cap)
KLEE: WARNING: killing 23425 states (over memory cap)
KLEE: WARNING: killing 23366 states (over memory cap)
KLEE: WARNING: killing 23638 states (over memory cap)
KLEE: WARNING: killing 23916 states (over memory cap)
KLEE: WARNING: killing 24661 states (over memory cap)
KLEE: WARNING: killing 23632 states (over memory cap)
KLEE: WARNING: killing 23580 states (over memory cap)
KLEE: WARNING: killing 23688 states (over memory cap)
KLEE: WARNING: killing 24278 states (over memory cap)
KLEE: WARNING: killing 24389 states (over memory cap)
KLEE: WARNING: killing 24664 states (over memory cap)
KLEE: WARNING: killing 23818 states (over memory cap)
KLEE: WARNING: killing 24409 states (over memory cap)
KLEE: WARNING: killing 23888 states (over memory cap)
KLEE: WARNING: killing 24003 states (over memory cap)
KLEE: WARNING: killing 24409 states (over memory cap)
KLEE: WARNING: killing 23898 states (over memory cap)
KLEE: WARNING: killing 23530 states (over memory cap)
KLEE: WARNING: killing 24104 states (over memory cap)
KLEE: WARNING: killing 23418 states (over memory cap)
KLEE: WARNING: killing 23833 states (over memory cap)
KLEE: WARNING: killing 24585 states (over memory cap)
KLEE: WARNING: killing 23910 states (over memory cap)
KLEE: WARNING: killing 23848 states (over memory cap)
KLEE: WARNING: killing 23810 states (over memory cap)
KLEE: WARNING: killing 23602 states (over memory cap)
KLEE: WARNING: killing 23552 states (over memory cap)
KLEE: WARNING: killing 22873 states (over memory cap)
KLEE: WARNING: killing 23597 states (over memory cap)
KLEE: WARNING: killing 23559 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-7XBCX9/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-net-usb-asix_true-unreach-call.cil.c:11585: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24117 states (over memory cap)
KLEE: WARNING: killing 23908 states (over memory cap)
KLEE: WARNING: killing 23253 states (over memory cap)
KLEE: WARNING: killing 23518 states (over memory cap)
KLEE: WARNING: killing 24076 states (over memory cap)
KLEE: WARNING: killing 23420 states (over memory cap)
KLEE: WARNING: killing 23692 states (over memory cap)
KLEE: WARNING: killing 23342 states (over memory cap)
KLEE: WARNING: killing 23897 states (over memory cap)
