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-kernel-locking-spinlock__drivers-net-usb-smsc95xx_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.: 198 295 1931 11218
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.436810016632
Removed calls to '__const_udelay' (function is undefined)
Defining function netdev_warn as symbolic
Defining function usbnet_read_cmd as symbolic
Defining function usbnet_read_cmd_nopm as symbolic
Defining function usbnet_write_cmd as symbolic
Defining function usbnet_write_cmd_nopm as symbolic
Defining function usbnet_get_link as symbolic
Defining function usbnet_get_msglevel as symbolic
Defining function usbnet_get_settings as symbolic
Defining function usbnet_change_mtu as symbolic
Defining function generic_mii_ioctl as symbolic
Defining function usbnet_open as symbolic
Defining function eth_mac_addr as symbolic
Removed calls to '__ldv_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function usbnet_write_cmd_async as symbolic
Defining function crc32_le as symbolic
Defining function bitrev32 as symbolic
Defining function usbnet_start_xmit as symbolic
Defining function usbnet_stop as symbolic
Defining function eth_validate_addr as symbolic
Defining function usbnet_nway_reset as symbolic
Defining function usbnet_set_settings as symbolic
Defining function device_set_wakeup_enable as symbolic
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Defining function printk as symbolic
Defining function usbnet_get_endpoints as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function mii_nway_restart as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mii_check_media as symbolic
Defining function mii_ethtool_gset as symbolic
Removed calls to 'usb_autopm_get_interface_no_resume' (function is undefined)
Removed calls to 'usb_autopm_put_interface' (function is undefined)
Defining function netdev_info as symbolic
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'usbnet_skb_return' (function is undefined)
Defining function skb_pull as symbolic
Defining function skb_clone as symbolic
Removed calls to 'usbnet_defer_kevent' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function skb_copy_expand as symbolic
Defining function csum_partial as symbolic
Defining function skb_push as symbolic
Defining function usbnet_resume 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 usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function crc16 as symbolic
Defining function bitrev16 as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'usbnet_get_drvinfo' (function is undefined)
Removed calls to 'usbnet_tx_timeout' (function is undefined)
Removed calls to 'usbnet_set_msglevel' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_assert' (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.445453882217
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 209 293 996 5945
INFO: Starting verification
KLEE: WARNING ONCE: function "smsc95xx_read_eeprom" has inline asm
KLEE: WARNING ONCE: function "__smsc95xx_read_reg" has inline asm
KLEE: WARNING ONCE: function "__smsc95xx_write_reg" has inline asm
KLEE: WARNING ONCE: function "smsc95xx_ethtool_set_eeprom" has inline asm
KLEE: WARNING ONCE: function "smsc95xx_tx_fixup" has inline asm
KLEE: WARNING ONCE: function "smsc95xx_resume" has inline asm
KLEE: WARNING: undefined reference to function: usbnet_disconnect
KLEE: WARNING: undefined reference to function: usbnet_get_drvinfo
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_e108ecba-15b1-486b-bf6b-8f16c7ba3aa2/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: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:8041: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:8932: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_e108ecba-15b1-486b-bf6b-8f16c7ba3aa2/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:11813: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:9225: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:8925: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_e108ecba-15b1-486b-bf6b-8f16c7ba3aa2/symbiotic/lib/kernel/kfree.c:5: free of global
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-PjwQvl/linux-3.14__complex_emg__linux-kernel-locking-spinlock__drivers-net-usb-smsc95xx_true-unreach-call.cil.c:9226: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
