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_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--can--sja1000--sja1000.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.: 55 83 528 3397
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.216495990753
Removed calls to 'can_free_echo_skb' (function is undefined)
Removed calls to 'can_led_event' (function is undefined)
Removed calls to 'can_bus_off' (function is undefined)
Defining function netdev_warn as symbolic
Defining function can_get_echo_skb as symbolic
Removed calls to '__netif_schedule' (function is undefined)
Defining function __dynamic_netdev_dbg as symbolic
Defining function alloc_can_err_skb as symbolic
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function alloc_can_skb as symbolic
Removed calls to '__raw_spin_lock_init' (function is undefined)
Defining function alloc_candev as symbolic
Removed calls to '__const_udelay' (function is undefined)
Defining function netdev_err as symbolic
Defining function netdev_info as symbolic
Removed calls to 'free_candev' (function is undefined)
Removed calls to 'devm_can_led_init' (function is undefined)
Defining function register_candev as symbolic
Removed calls to 'unregister_candev' (function is undefined)
Removed calls to 'close_candev' (function is undefined)
Removed calls to 'free_irq' (function is undefined)
Removed calls to 'can_put_echo_skb' (function is undefined)
Defining function can_change_mtu as symbolic
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function printk as symbolic
Defining function open_candev as symbolic
Defining function request_threaded_irq as symbolic
Defining function ldv_ndo_init_2 as symbolic
Defining function ldv_ndo_uninit_2 as symbolic
Linked our definitions to these undefined functions:
  __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.280759096146
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 96 78 298 1914
INFO: Starting verification
KLEE: WARNING ONCE: function "netif_wake_queue" has inline asm
KLEE: WARNING ONCE: function "sja1000_open" has inline asm
KLEE: WARNING ONCE: function "netif_stop_queue" 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_4470e5a9-751b-4d5e-ba75-3e4ef3e2faa6/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-D8mrbG/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--can--sja1000--sja1000.ko-entry_point_true-unreach-call.cil.out.c:5635: 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 15487 states (over memory cap)
KLEE: WARNING: killing 16502 states (over memory cap)
KLEE: WARNING: killing 16536 states (over memory cap)
KLEE: WARNING: killing 16581 states (over memory cap)
KLEE: WARNING: killing 16628 states (over memory cap)
KLEE: WARNING: killing 17088 states (over memory cap)
KLEE: WARNING: killing 17410 states (over memory cap)
KLEE: WARNING: killing 17602 states (over memory cap)
KLEE: WARNING: killing 17384 states (over memory cap)
KLEE: WARNING: killing 17450 states (over memory cap)
KLEE: WARNING: killing 17503 states (over memory cap)
KLEE: WARNING: killing 17425 states (over memory cap)
KLEE: WARNING: killing 17622 states (over memory cap)
KLEE: WARNING: killing 17549 states (over memory cap)
KLEE: WARNING: killing 17881 states (over memory cap)
KLEE: WARNING: killing 17677 states (over memory cap)
KLEE: WARNING: killing 17606 states (over memory cap)
KLEE: WARNING: killing 17411 states (over memory cap)
KLEE: WARNING: killing 17873 states (over memory cap)
KLEE: WARNING: killing 17925 states (over memory cap)
KLEE: WARNING: killing 17469 states (over memory cap)
KLEE: WARNING: killing 18054 states (over memory cap)
KLEE: WARNING: killing 17729 states (over memory cap)
KLEE: WARNING: killing 18043 states (over memory cap)
KLEE: WARNING: killing 17593 states (over memory cap)
KLEE: WARNING: killing 17524 states (over memory cap)
KLEE: WARNING: killing 17716 states (over memory cap)
KLEE: WARNING: killing 12627 states (over memory cap)
KLEE: WARNING: killing 17232 states (over memory cap)
KLEE: WARNING: killing 12556 states (over memory cap)
KLEE: WARNING: killing 17379 states (over memory cap)
KLEE: WARNING: killing 12475 states (over memory cap)
KLEE: WARNING: killing 17536 states (over memory cap)
KLEE: WARNING: killing 12782 states (over memory cap)
KLEE: WARNING: killing 12382 states (over memory cap)
KLEE: WARNING: killing 17284 states (over memory cap)
KLEE: WARNING: killing 12685 states (over memory cap)
KLEE: WARNING: killing 17180 states (over memory cap)
KLEE: WARNING: killing 12489 states (over memory cap)
KLEE: WARNING: killing 17205 states (over memory cap)
KLEE: WARNING: killing 12539 states (over memory cap)
KLEE: WARNING: killing 12141 states (over memory cap)
KLEE: WARNING: killing 17070 states (over memory cap)
KLEE: WARNING: killing 12441 states (over memory cap)
KLEE: WARNING: killing 17336 states (over memory cap)
KLEE: WARNING: killing 12251 states (over memory cap)
KLEE: WARNING: killing 16999 states (over memory cap)
KLEE: WARNING: killing 12653 states (over memory cap)
KLEE: WARNING: killing 17144 states (over memory cap)
KLEE: WARNING: killing 12467 states (over memory cap)
KLEE: WARNING: killing 11847 states (over memory cap)
KLEE: WARNING: killing 12173 states (over memory cap)
KLEE: WARNING: killing 12030 states (over memory cap)
KLEE: WARNING: killing 12120 states (over memory cap)
KLEE: WARNING: killing 11861 states (over memory cap)
KLEE: WARNING: killing 11949 states (over memory cap)
KLEE: WARNING: killing 11692 states (over memory cap)
KLEE: WARNING: killing 11901 states (over memory cap)
KLEE: WARNING: killing 11870 states (over memory cap)
KLEE: WARNING: killing 11960 states (over memory cap)
KLEE: WARNING: killing 11704 states (over memory cap)
KLEE: WARNING: killing 12028 states (over memory cap)
KLEE: WARNING: killing 11887 states (over memory cap)
KLEE: WARNING: killing 11744 states (over memory cap)
KLEE: WARNING: killing 12063 states (over memory cap)
KLEE: WARNING: killing 11814 states (over memory cap)
KLEE: WARNING: killing 12012 states (over memory cap)
KLEE: WARNING: killing 12340 states (over memory cap)
KLEE: WARNING: killing 12430 states (over memory cap)
KLEE: WARNING: killing 11951 states (over memory cap)
KLEE: WARNING: killing 11924 states (over memory cap)
KLEE: WARNING: killing 12246 states (over memory cap)
KLEE: WARNING: killing 11995 states (over memory cap)
KLEE: WARNING: killing 12196 states (over memory cap)
KLEE: WARNING: killing 11720 states (over memory cap)
KLEE: WARNING: killing 11804 states (over memory cap)
KLEE: WARNING: killing 12230 states (over memory cap)
KLEE: WARNING: killing 11871 states (over memory cap)
KLEE: WARNING: killing 11845 states (over memory cap)
KLEE: WARNING: killing 11821 states (over memory cap)
KLEE: WARNING: killing 12130 states (over memory cap)
KLEE: WARNING: killing 11663 states (over memory cap)
KLEE: WARNING: killing 12312 states (over memory cap)
KLEE: WARNING: killing 12070 states (over memory cap)
KLEE: WARNING: killing 11817 states (over memory cap)
KLEE: WARNING: killing 11906 states (over memory cap)
KLEE: WARNING: killing 11880 states (over memory cap)
KLEE: WARNING: killing 11962 states (over memory cap)
KLEE: WARNING: killing 11605 states (over memory cap)
KLEE: WARNING: killing 12244 states (over memory cap)
KLEE: WARNING: killing 12225 states (over memory cap)
KLEE: WARNING: killing 12201 states (over memory cap)
KLEE: WARNING: killing 12067 states (over memory cap)
KLEE: WARNING: killing 11829 states (over memory cap)
KLEE: WARNING: killing 12025 states (over memory cap)
KLEE: WARNING: killing 11994 states (over memory cap)
KLEE: WARNING: killing 11973 states (over memory cap)
KLEE: WARNING: killing 11955 states (over memory cap)
KLEE: WARNING: killing 12034 states (over memory cap)
KLEE: WARNING: killing 12019 states (over memory cap)
KLEE: WARNING: killing 12100 states (over memory cap)
