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--wan--hdlc_ppp.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.: 30 74 538 3034
Removed infinite loop in ppp_cp_event
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.244999170303
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '_raw_spin_unlock_irqrestore' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function _raw_spin_lock_irqsave as symbolic
Defining function skb_pull as symbolic
Removed calls to 'skb_queue_tail' (function is undefined)
Removed calls to 'linkwatch_fire_event' (function is undefined)
Defining function dev_queue_xmit as symbolic
Defining function netdev_info as symbolic
Defining function del_timer as symbolic
Defining function mod_timer as symbolic
Defining function netdev_warn as symbolic
Defining function skb_put as symbolic
Defining function skb_push as symbolic
Defining function capable as symbolic
Defining function attach_hdlc_protocol as symbolic
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'unregister_hdlc_protocol' (function is undefined)
Removed calls to 'register_hdlc_protocol' (function is undefined)
Defining function ldv_disconnect_3 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_open_3 as symbolic
Defining function ldv_setup_3 as symbolic
Linked our definitions to these undefined functions:
  memcmp
  __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_uint_named
  __VERIFIER_nondet_ulong_named
  __VERIFIER_nondet_ushort_named
INFO: After-slicing optimizations and preparation time: 0.249851942062
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 79 78 342 1780
INFO: Starting verification
KLEE: WARNING ONCE: function "ppp_cp_event" has inline asm
KLEE: WARNING ONCE: function "netif_dormant_on" has inline asm
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:6241: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_2f05bdbd-8314-4b77-8fc5-88ec61b84d76/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5490: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5877: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5491: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5459: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:6118: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5414: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-TURmRh/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_ppp.ko-entry_point_false-unreach-call.cil.out.c:5414: 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 14196 states (over memory cap)
KLEE: WARNING: killing 12675 states (over memory cap)
KLEE: WARNING: killing 12825 states (over memory cap)
KLEE: WARNING: killing 12868 states (over memory cap)
KLEE: WARNING: killing 12507 states (over memory cap)
KLEE: WARNING: killing 12760 states (over memory cap)
KLEE: WARNING: killing 12810 states (over memory cap)
KLEE: WARNING: killing 12961 states (over memory cap)
KLEE: WARNING: killing 13821 states (over memory cap)
KLEE: WARNING: killing 14073 states (over memory cap)
KLEE: WARNING: killing 14026 states (over memory cap)
KLEE: WARNING: killing 14379 states (over memory cap)
KLEE: WARNING: killing 14434 states (over memory cap)
KLEE: WARNING: killing 14591 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 9893 states (over memory cap)
KLEE: WARNING: killing 14091 states (over memory cap)
KLEE: WARNING: killing 10432 states (over memory cap)
KLEE: WARNING: killing 14014 states (over memory cap)
KLEE: WARNING: killing 10280 states (over memory cap)
KLEE: WARNING: killing 10157 states (over memory cap)
KLEE: WARNING: killing 9940 states (over memory cap)
KLEE: WARNING: killing 14367 states (over memory cap)
KLEE: WARNING: killing 10279 states (over memory cap)
KLEE: WARNING: killing 10160 states (over memory cap)
KLEE: WARNING: killing 10045 states (over memory cap)
KLEE: WARNING: killing 9829 states (over memory cap)
KLEE: WARNING: killing 10289 states (over memory cap)
KLEE: WARNING: killing 10081 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 10041 states (over memory cap)
KLEE: WARNING: killing 10498 states (over memory cap)
KLEE: WARNING: killing 10283 states (over memory cap)
KLEE: WARNING: killing 9982 states (over memory cap)
KLEE: WARNING: killing 10057 states (over memory cap)
KLEE: WARNING: killing 10127 states (over memory cap)
KLEE: WARNING: killing 9920 states (over memory cap)
KLEE: WARNING: killing 10091 states (over memory cap)
KLEE: WARNING: killing 10540 states (over memory cap)
KLEE: WARNING: killing 10619 states (over memory cap)
KLEE: WARNING: killing 10314 states (over memory cap)
KLEE: WARNING: killing 10011 states (over memory cap)
KLEE: WARNING: killing 10459 states (over memory cap)
KLEE: WARNING: killing 10064 states (over memory cap)
KLEE: WARNING: killing 10418 states (over memory cap)
KLEE: WARNING: killing 10032 states (over memory cap)
KLEE: WARNING: killing 10293 states (over memory cap)
KLEE: WARNING: killing 10454 states (over memory cap)
KLEE: WARNING: killing 10716 states (over memory cap)
KLEE: WARNING: killing 10515 states (over memory cap)
KLEE: WARNING: killing 10038 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10643 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 10697 states (over memory cap)
KLEE: WARNING: killing 10407 states (over memory cap)
KLEE: WARNING: killing 10658 states (over memory cap)
KLEE: WARNING: killing 10461 states (over memory cap)
KLEE: WARNING: killing 10716 states (over memory cap)
KLEE: WARNING: killing 10057 states (over memory cap)
KLEE: WARNING: killing 10674 states (over memory cap)
KLEE: WARNING: killing 10567 states (over memory cap)
KLEE: WARNING: killing 11003 states (over memory cap)
KLEE: WARNING: killing 10628 states (over memory cap)
KLEE: WARNING: killing 10523 states (over memory cap)
KLEE: WARNING: killing 10770 states (over memory cap)
KLEE: WARNING: killing 10306 states (over memory cap)
KLEE: WARNING: killing 10649 states (over memory cap)
KLEE: WARNING: killing 10091 states (over memory cap)
KLEE: WARNING: killing 10251 states (over memory cap)
KLEE: WARNING: killing 10502 states (over memory cap)
KLEE: WARNING: killing 10309 states (over memory cap)
KLEE: WARNING: killing 10738 states (over memory cap)
KLEE: WARNING: killing 10188 states (over memory cap)
KLEE: WARNING: killing 10704 states (over memory cap)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 10670 states (over memory cap)
KLEE: WARNING: killing 10657 states (over memory cap)
KLEE: WARNING: killing 10464 states (over memory cap)
KLEE: WARNING: killing 10444 states (over memory cap)
KLEE: WARNING: killing 10342 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10394 states (over memory cap)
KLEE: WARNING: killing 10737 states (over memory cap)
KLEE: WARNING: killing 10192 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 10504 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 10568 states (over memory cap)
KLEE: WARNING: killing 10898 states (over memory cap)
KLEE: WARNING: killing 10360 states (over memory cap)
KLEE: WARNING: killing 10173 states (over memory cap)
KLEE: WARNING: killing 10676 states (over memory cap)
KLEE: WARNING: killing 10404 states (over memory cap)
KLEE: WARNING: killing 10302 states (over memory cap)
KLEE: WARNING: killing 10632 states (over memory cap)
KLEE: WARNING: killing 10613 states (over memory cap)
KLEE: WARNING: killing 10600 states (over memory cap)
KLEE: WARNING: killing 10756 states (over memory cap)
KLEE: WARNING: killing 10824 states (over memory cap)
KLEE: WARNING: killing 10381 states (over memory cap)
KLEE: WARNING: killing 10452 states (over memory cap)
KLEE: WARNING: killing 10348 states (over memory cap)
KLEE: WARNING: killing 10677 states (over memory cap)
KLEE: WARNING: killing 10578 states (over memory cap)
KLEE: WARNING: killing 11329 states (over memory cap)
KLEE: WARNING: killing 10637 states (over memory cap)
KLEE: WARNING: killing 11046 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10758 states (over memory cap)
KLEE: WARNING: killing 10831 states (over memory cap)
KLEE: WARNING: killing 10557 states (over memory cap)
