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--wan--lapbether.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.: 43 99 599 2975
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.299751996994
Removed calls to 'warn_slowpath_null' (function is undefined)
Defining function lapb_connect_request as symbolic
Defining function printk as symbolic
Defining function lapb_disconnect_request as symbolic
Defining function skb_pull as symbolic
Defining function lapb_data_request as symbolic
Defining function lapb_unregister as symbolic
Defining function lapb_register as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'skb_trim' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function lapb_data_received as symbolic
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function rcu_lockdep_current_cpu_online as symbolic
Defining function lock_is_held as symbolic
Defining function __pskb_pull_tail as symbolic
Defining function skb_clone as symbolic
Removed calls to 'dump_stack' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Defining function dev_close as symbolic
Defining function rtnl_is_locked as symbolic
Defining function alloc_netdev_mqs as symbolic
Defining function register_netdevice as symbolic
Defining function skb_push as symbolic
Defining function dev_queue_xmit as symbolic
Defining function pskb_expand_head as symbolic
Defining function skb_put as symbolic
Removed calls to 'dev_remove_pack' (function is undefined)
Removed calls to 'rtnl_lock' (function is undefined)
Removed calls to 'rtnl_unlock' (function is undefined)
Removed calls to 'dev_add_pack' (function is undefined)
Defining function ldv_probe_4 as symbolic
Defining function ldv_ndo_init_3 as symbolic
Defining function ldv_ndo_uninit_3 as symbolic
Defining function register_netdevice_notifier as symbolic
Defining function unregister_netdevice_notifier as symbolic
Linked our definitions to these undefined functions:
  strncmp
  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.286262989044
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 90 87 288 1484
INFO: Starting verification
KLEE: WARNING ONCE: function "lapbeth_open" has inline asm
KLEE: WARNING ONCE: function "lapbeth_close" has inline asm
KLEE: WARNING ONCE: function "lapbeth_rcv" has inline asm
KLEE: WARNING ONCE: function "lapbeth_device_event" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: WARNING: undefined reference to function: free_netdev
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_2611b430-6c5c-4c87-bf8b-32c3f4d8a2ec/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:6853: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7000: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7203: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7071: 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 14988 states (over memory cap)
KLEE: WARNING: killing 12830 states (over memory cap)
KLEE: WARNING: killing 13591 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:5897: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 13952 states (over memory cap)
KLEE: WARNING: killing 14309 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13730 states (over memory cap)
KLEE: WARNING: killing 14677 states (over memory cap)
KLEE: WARNING: killing 14147 states (over memory cap)
KLEE: WARNING: killing 14301 states (over memory cap)
KLEE: WARNING: killing 14760 states (over memory cap)
KLEE: WARNING: killing 14530 states (over memory cap)
KLEE: WARNING: killing 14786 states (over memory cap)
KLEE: WARNING: killing 15137 states (over memory cap)
KLEE: WARNING: killing 15883 states (over memory cap)
KLEE: WARNING: killing 16342 states (over memory cap)
KLEE: WARNING: killing 16397 states (over memory cap)
KLEE: WARNING: killing 16546 states (over memory cap)
KLEE: WARNING: killing 16805 states (over memory cap)
KLEE: WARNING: killing 16379 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 16588 states (over memory cap)
KLEE: WARNING: killing 16361 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7071: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16798 states (over memory cap)
KLEE: WARNING: killing 16574 states (over memory cap)
KLEE: WARNING: killing 16632 states (over memory cap)
KLEE: WARNING: killing 16012 states (over memory cap)
KLEE: WARNING: killing 16446 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7087: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING: killing 16651 states (over memory cap)
KLEE: WARNING: killing 16705 states (over memory cap)
KLEE: WARNING: killing 16478 states (over memory cap)
KLEE: WARNING: killing 16623 states (over memory cap)
KLEE: WARNING: killing 17053 states (over memory cap)
KLEE: WARNING: killing 17206 states (over memory cap)
KLEE: WARNING: killing 17635 states (over memory cap)
KLEE: WARNING: killing 17034 states (over memory cap)
KLEE: WARNING: killing 16908 states (over memory cap)
KLEE: WARNING: killing 16875 states (over memory cap)
KLEE: WARNING: killing 16920 states (over memory cap)
KLEE: WARNING: killing 16691 states (over memory cap)
KLEE: WARNING: killing 9362 states (over memory cap)
KLEE: WARNING: killing 16830 states (over memory cap)
KLEE: WARNING: killing 16882 states (over memory cap)
KLEE: WARNING: killing 9306 states (over memory cap)
KLEE: WARNING: killing 16828 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7008: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17152 states (over memory cap)
KLEE: WARNING: killing 16838 states (over memory cap)
KLEE: WARNING: killing 9053 states (over memory cap)
KLEE: WARNING: killing 16513 states (over memory cap)
KLEE: WARNING: killing 9020 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:6926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 17095 states (over memory cap)
KLEE: WARNING: killing 9173 states (over memory cap)
KLEE: WARNING: killing 16224 states (over memory cap)
KLEE: WARNING: killing 9228 states (over memory cap)
KLEE: WARNING: killing 16709 states (over memory cap)
KLEE: WARNING: killing 16938 states (over memory cap)
KLEE: WARNING: killing 9001 states (over memory cap)
KLEE: WARNING: killing 16072 states (over memory cap)
KLEE: WARNING: killing 9234 states (over memory cap)
KLEE: WARNING: killing 15845 states (over memory cap)
KLEE: WARNING: killing 9201 states (over memory cap)
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING: killing 9258 states (over memory cap)
KLEE: WARNING: killing 8811 states (over memory cap)
KLEE: WARNING: killing 9154 states (over memory cap)
KLEE: WARNING: killing 16597 states (over memory cap)
KLEE: WARNING: killing 8780 states (over memory cap)
KLEE: WARNING: killing 16638 states (over memory cap)
KLEE: WARNING: killing 9099 states (over memory cap)
KLEE: WARNING: killing 16056 states (over memory cap)
KLEE: WARNING: killing 9327 states (over memory cap)
KLEE: WARNING: killing 16441 states (over memory cap)
KLEE: WARNING: killing 9127 states (over memory cap)
KLEE: WARNING: killing 16651 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-uX_AFn/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--lapbether.ko-entry_point_true-unreach-call.cil.out.c:7009: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 9011 states (over memory cap)
KLEE: WARNING: killing 8659 states (over memory cap)
KLEE: WARNING: killing 8908 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 9489 states (over memory cap)
KLEE: WARNING: killing 16187 states (over memory cap)
KLEE: WARNING: killing 9205 states (over memory cap)
KLEE: WARNING: killing 15878 states (over memory cap)
KLEE: WARNING: killing 8918 states (over memory cap)
KLEE: WARNING: killing 16526 states (over memory cap)
KLEE: WARNING: killing 9493 states (over memory cap)
KLEE: WARNING: killing 8544 states (over memory cap)
KLEE: WARNING: killing 16466 states (over memory cap)
KLEE: WARNING: killing 9456 states (over memory cap)
KLEE: WARNING: killing 8600 states (over memory cap)
KLEE: WARNING: killing 16233 states (over memory cap)
KLEE: WARNING: killing 9255 states (over memory cap)
KLEE: WARNING: killing 8743 states (over memory cap)
KLEE: WARNING: killing 9154 states (over memory cap)
KLEE: WARNING: killing 8558 states (over memory cap)
KLEE: WARNING: killing 8631 states (over memory cap)
KLEE: WARNING: killing 15888 states (over memory cap)
KLEE: WARNING: killing 9026 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 9339 states (over memory cap)
KLEE: WARNING: killing 8831 states (over memory cap)
KLEE: WARNING: killing 15782 states (over memory cap)
KLEE: WARNING: killing 9388 states (over memory cap)
KLEE: WARNING: killing 8461 states (over memory cap)
KLEE: WARNING: killing 8789 states (over memory cap)
KLEE: WARNING: killing 8447 states (over memory cap)
KLEE: WARNING: killing 8522 states (over memory cap)
KLEE: WARNING: killing 8516 states (over memory cap)
KLEE: WARNING: killing 8754 states (over memory cap)
KLEE: WARNING: killing 8415 states (over memory cap)
KLEE: WARNING: killing 8823 states (over memory cap)
KLEE: WARNING: killing 8734 states (over memory cap)
KLEE: WARNING: killing 8393 states (over memory cap)
