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_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--net--can--usb--kvaser_usb.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.: 60 114 782 5697
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.300240039825
Defining function can_change_mtu as symbolic
Defining function netdev_err as symbolic
Defining function netdev_warn as symbolic
Defining function usb_submit_urb as symbolic
Defining function printk as symbolic
Defining function usb_alloc_urb as symbolic
Defining function open_candev as symbolic
Defining function dev_warn as symbolic
Defining function dev_err as symbolic
Defining function usb_alloc_coherent as symbolic
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to 'unregister_netdev' (function is undefined)
Removed calls to 'usb_kill_anchored_urbs' (function is undefined)
Removed calls to 'usb_free_coherent' (function is undefined)
Removed calls to 'free_candev' (function is undefined)
Defining function devm_kmalloc as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'close_candev' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'kfree_skb' (function is undefined)
Removed calls to 'consume_skb' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 as symbolic
Defining function usb_register_driver 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 __netdev_alloc_skb as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  __kmalloc
  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.262943029404
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 89 70 230 1208
INFO: Starting verification
KLEE: WARNING ONCE: function "main" 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_10db2ae0-31da-4886-acf3-c126732d116c/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Z1Hodp/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--net--can--usb--kvaser_usb.ko-entry_point_true-unreach-call.cil.out.c:7983: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Z1Hodp/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--net--can--usb--kvaser_usb.ko-entry_point_true-unreach-call.cil.out.c:7346: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-Z1Hodp/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--net--can--usb--kvaser_usb.ko-entry_point_true-unreach-call.cil.out.c:7955: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 9841 states (over memory cap)
KLEE: WARNING: killing 12648 states (over memory cap)
KLEE: WARNING: killing 12863 states (over memory cap)
KLEE: WARNING: killing 12986 states (over memory cap)
KLEE: WARNING: killing 13211 states (over memory cap)
KLEE: WARNING: killing 9421 states (over memory cap)
KLEE: WARNING: killing 13496 states (over memory cap)
KLEE: WARNING: killing 9820 states (over memory cap)
KLEE: WARNING: killing 9800 states (over memory cap)
KLEE: WARNING: killing 9589 states (over memory cap)
KLEE: WARNING: killing 9660 states (over memory cap)
KLEE: WARNING: killing 9913 states (over memory cap)
KLEE: WARNING: killing 9796 states (over memory cap)
KLEE: WARNING: killing 9866 states (over memory cap)
KLEE: WARNING: killing 9844 states (over memory cap)
KLEE: WARNING: killing 9915 states (over memory cap)
KLEE: WARNING: killing 9888 states (over memory cap)
KLEE: WARNING: killing 10320 states (over memory cap)
KLEE: WARNING: killing 10117 states (over memory cap)
KLEE: WARNING: killing 10183 states (over memory cap)
KLEE: WARNING: killing 9976 states (over memory cap)
KLEE: WARNING: killing 10320 states (over memory cap)
KLEE: WARNING: killing 10115 states (over memory cap)
KLEE: WARNING: killing 10271 states (over memory cap)
KLEE: WARNING: killing 10248 states (over memory cap)
KLEE: WARNING: killing 10402 states (over memory cap)
KLEE: WARNING: killing 10287 states (over memory cap)
KLEE: WARNING: killing 10264 states (over memory cap)
KLEE: WARNING: killing 10332 states (over memory cap)
KLEE: WARNING: killing 10396 states (over memory cap)
KLEE: WARNING: killing 10550 states (over memory cap)
KLEE: WARNING: killing 10617 states (over memory cap)
KLEE: WARNING: killing 10947 states (over memory cap)
KLEE: WARNING: killing 10573 states (over memory cap)
KLEE: WARNING: killing 10284 states (over memory cap)
KLEE: WARNING: killing 10439 states (over memory cap)
KLEE: WARNING: killing 10239 states (over memory cap)
KLEE: WARNING: killing 10654 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10873 states (over memory cap)
KLEE: WARNING: killing 10764 states (over memory cap)
KLEE: WARNING: killing 11001 states (over memory cap)
KLEE: WARNING: killing 10457 states (over memory cap)
KLEE: WARNING: killing 10688 states (over memory cap)
KLEE: WARNING: killing 10668 states (over memory cap)
KLEE: WARNING: killing 10980 states (over memory cap)
KLEE: WARNING: killing 10961 states (over memory cap)
KLEE: WARNING: killing 10935 states (over memory cap)
KLEE: WARNING: killing 10572 states (over memory cap)
KLEE: WARNING: killing 10891 states (over memory cap)
KLEE: WARNING: killing 10948 states (over memory cap)
KLEE: WARNING: killing 10755 states (over memory cap)
KLEE: WARNING: killing 10651 states (over memory cap)
KLEE: WARNING: killing 10882 states (over memory cap)
KLEE: WARNING: killing 10859 states (over memory cap)
KLEE: WARNING: killing 11003 states (over memory cap)
KLEE: WARNING: killing 10903 states (over memory cap)
KLEE: WARNING: killing 10966 states (over memory cap)
KLEE: WARNING: killing 11360 states (over memory cap)
KLEE: WARNING: killing 10758 states (over memory cap)
KLEE: WARNING: killing 10815 states (over memory cap)
KLEE: WARNING: killing 10710 states (over memory cap)
KLEE: WARNING: killing 10518 states (over memory cap)
KLEE: WARNING: killing 10829 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 11204 states (over memory cap)
KLEE: WARNING: killing 11186 states (over memory cap)
KLEE: WARNING: killing 10999 states (over memory cap)
KLEE: WARNING: killing 10979 states (over memory cap)
KLEE: WARNING: killing 11122 states (over memory cap)
KLEE: WARNING: killing 11023 states (over memory cap)
KLEE: WARNING: killing 10914 states (over memory cap)
KLEE: WARNING: killing 10897 states (over memory cap)
KLEE: WARNING: killing 11123 states (over memory cap)
KLEE: WARNING: killing 10934 states (over memory cap)
KLEE: WARNING: killing 10921 states (over memory cap)
KLEE: WARNING: killing 10979 states (over memory cap)
KLEE: WARNING: killing 10880 states (over memory cap)
KLEE: WARNING: killing 10696 states (over memory cap)
KLEE: WARNING: killing 10429 states (over memory cap)
KLEE: WARNING: killing 11053 states (over memory cap)
KLEE: WARNING: killing 10877 states (over memory cap)
KLEE: WARNING: killing 10856 states (over memory cap)
KLEE: WARNING: killing 11077 states (over memory cap)
KLEE: WARNING: killing 11056 states (over memory cap)
KLEE: WARNING: killing 11036 states (over memory cap)
KLEE: WARNING: killing 11257 states (over memory cap)
KLEE: WARNING: killing 11162 states (over memory cap)
KLEE: WARNING: killing 10907 states (over memory cap)
KLEE: WARNING: killing 10962 states (over memory cap)
KLEE: WARNING: killing 11104 states (over memory cap)
KLEE: WARNING: killing 10924 states (over memory cap)
KLEE: WARNING: killing 10671 states (over memory cap)
KLEE: WARNING: killing 11043 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 10685 states (over memory cap)
KLEE: WARNING: killing 11062 states (over memory cap)
KLEE: WARNING: killing 10885 states (over memory cap)
KLEE: WARNING: killing 11106 states (over memory cap)
KLEE: WARNING: killing 10933 states (over memory cap)
KLEE: WARNING: killing 10914 states (over memory cap)
KLEE: WARNING: killing 10741 states (over memory cap)
KLEE: WARNING: killing 11038 states (over memory cap)
KLEE: WARNING: killing 11091 states (over memory cap)
KLEE: WARNING: killing 11002 states (over memory cap)
KLEE: WARNING: killing 10830 states (over memory cap)
KLEE: WARNING: killing 10887 states (over memory cap)
KLEE: WARNING: killing 11099 states (over memory cap)
KLEE: WARNING: killing 11001 states (over memory cap)
KLEE: WARNING: killing 10987 states (over memory cap)
KLEE: WARNING: killing 10892 states (over memory cap)
