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/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--cdc_ncm.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.: 174 138 1392 9135
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.447963953018
Removed calls to 'hrtimer_init' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'usb_driver_release_interface' (function is undefined)
Removed calls to '__tasklet_schedule' (function is undefined)
Removed calls to '_raw_spin_lock_bh' (function is undefined)
Removed calls to '_raw_spin_unlock_bh' (function is undefined)
Defining function usb_ifnum_to_if as symbolic
Defining function usb_driver_claim_interface as symbolic
Defining function usb_set_interface as symbolic
Defining function usbnet_get_ethernet_addr as symbolic
Defining function _dev_info as symbolic
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'usbnet_unlink_rx_urbs' (function is undefined)
Removed calls to 'usbnet_update_max_qlen' (function is undefined)
Defining function usbnet_read_cmd as symbolic
Defining function usbnet_write_cmd as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__local_bh_disable_ip' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function usbnet_start_xmit as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Removed calls to '__local_bh_enable_ip' (function is undefined)
Defining function dev_warn as symbolic
Defining function dev_err as symbolic
Defining function hrtimer_start as symbolic
Removed calls to 'tasklet_kill' (function is undefined)
Defining function hrtimer_cancel as symbolic
Defining function usb_altnum_to_altsetting as symbolic
Defining function skb_put as symbolic
Removed calls to 'usbnet_skb_return' (function is undefined)
Defining function __netdev_alloc_skb as symbolic
Defining function usbnet_get_settings as symbolic
Defining function usbnet_set_settings as symbolic
Defining function usbnet_get_msglevel as symbolic
Defining function usbnet_nway_reset as symbolic
Defining function usbnet_get_link as symbolic
Defining function ethtool_op_get_ts_info as symbolic
Defining function kstrtoull as symbolic
Defining function sprintf as symbolic
Defining function usbnet_probe as symbolic
Defining function usbnet_suspend as symbolic
Defining function usbnet_resume as symbolic
Removed calls to 'usbnet_link_change' (function is undefined)
Defining function usbnet_manage_power as symbolic
Defining function netdev_info as symbolic
Removed calls to 'usbnet_disconnect' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'usbnet_get_drvinfo' (function is undefined)
Removed calls to 'usbnet_set_msglevel' (function is undefined)
Defining function usb_register_driver 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_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_u32_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.42233300209
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 247 126 694 4955
INFO: Starting verification
KLEE: WARNING ONCE: function "cdc_ncm_tx_timer_cb" has inline asm
KLEE: WARNING ONCE: function "netif_tx_lock_bh" has inline asm
KLEE: WARNING ONCE: function "netif_tx_unlock_bh" has inline asm
KLEE: WARNING ONCE: function "cdc_ncm_status" 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 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 4931 states (over memory cap)
KLEE: WARNING: killing 4558 states (over memory cap)
KLEE: WARNING: killing 4339 states (over memory cap)
KLEE: WARNING: killing 4130 states (over memory cap)
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_54db95db-65d5-42a7-8897-a2b4f6d98572/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 4719 states (over memory cap)
KLEE: WARNING: killing 6826 states (over memory cap)
KLEE: WARNING: killing 8669 states (over memory cap)
KLEE: WARNING: killing 8915 states (over memory cap)
KLEE: WARNING: killing 8658 states (over memory cap)
KLEE: WARNING: killing 8270 states (over memory cap)
KLEE: WARNING: killing 6994 states (over memory cap)
KLEE: WARNING: killing 7344 states (over memory cap)
KLEE: WARNING: killing 7400 states (over memory cap)
KLEE: WARNING: killing 7161 states (over memory cap)
KLEE: WARNING: killing 7600 states (over memory cap)
KLEE: WARNING: killing 7822 states (over memory cap)
KLEE: WARNING: killing 7416 states (over memory cap)
KLEE: WARNING: killing 8234 states (over memory cap)
KLEE: WARNING: killing 7911 states (over memory cap)
KLEE: WARNING: killing 8608 states (over memory cap)
KLEE: WARNING: killing 8456 states (over memory cap)
KLEE: WARNING: killing 8856 states (over memory cap)
KLEE: WARNING: killing 8659 states (over memory cap)
KLEE: WARNING: killing 8716 states (over memory cap)
KLEE: WARNING: killing 7656 states (over memory cap)
KLEE: WARNING: killing 7618 states (over memory cap)
KLEE: WARNING: killing 8318 states (over memory cap)
KLEE: WARNING: killing 8457 states (over memory cap)
KLEE: WARNING: killing 8034 states (over memory cap)
KLEE: WARNING: killing 8086 states (over memory cap)
KLEE: WARNING: killing 8222 states (over memory cap)
KLEE: WARNING: killing 7623 states (over memory cap)
KLEE: WARNING: killing 8535 states (over memory cap)
KLEE: WARNING: killing 8023 states (over memory cap)
KLEE: WARNING: killing 7551 states (over memory cap)
KLEE: WARNING: killing 7985 states (over memory cap)
KLEE: WARNING: killing 8074 states (over memory cap)
KLEE: WARNING: killing 7906 states (over memory cap)
KLEE: WARNING: killing 8210 states (over memory cap)
KLEE: WARNING: killing 9040 states (over memory cap)
KLEE: WARNING: killing 8219 states (over memory cap)
KLEE: WARNING: killing 7784 states (over memory cap)
KLEE: WARNING: killing 7786 states (over memory cap)
KLEE: WARNING: killing 7829 states (over memory cap)
KLEE: WARNING: killing 8093 states (over memory cap)
KLEE: WARNING: killing 8613 states (over memory cap)
KLEE: WARNING: killing 8266 states (over memory cap)
KLEE: WARNING: killing 8182 states (over memory cap)
KLEE: WARNING: killing 8225 states (over memory cap)
KLEE: WARNING: killing 8530 states (over memory cap)
KLEE: WARNING: killing 8796 states (over memory cap)
KLEE: WARNING: killing 8663 states (over memory cap)
KLEE: WARNING: killing 7710 states (over memory cap)
KLEE: WARNING: killing 8140 states (over memory cap)
KLEE: WARNING: killing 8835 states (over memory cap)
KLEE: WARNING: killing 8054 states (over memory cap)
KLEE: WARNING: killing 7923 states (over memory cap)
KLEE: WARNING: killing 7878 states (over memory cap)
KLEE: WARNING: killing 7875 states (over memory cap)
KLEE: WARNING: killing 8133 states (over memory cap)
KLEE: WARNING: killing 8305 states (over memory cap)
KLEE: WARNING: killing 7437 states (over memory cap)
KLEE: WARNING: killing 8085 states (over memory cap)
KLEE: WARNING: killing 7648 states (over memory cap)
KLEE: WARNING: killing 8164 states (over memory cap)
KLEE: WARNING: killing 8078 states (over memory cap)
KLEE: WARNING: killing 8550 states (over memory cap)
KLEE: WARNING: killing 8245 states (over memory cap)
KLEE: WARNING: killing 8115 states (over memory cap)
KLEE: WARNING: killing 8503 states (over memory cap)
KLEE: WARNING: killing 8197 states (over memory cap)
KLEE: WARNING: killing 7936 states (over memory cap)
KLEE: WARNING: killing 8625 states (over memory cap)
