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_fr.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.: 52 98 928 6334
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.316656827927
Removed calls to 'add_timer' (function is undefined)
Removed calls to 'unregister_netdevice_queue' (function is undefined)
Removed calls to 'get_random_bytes' (function is undefined)
Removed calls to 'free_netdev' (function is undefined)
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Defining function skb_pull as symbolic
Defining function eth_type_trans as symbolic
Defining function netdev_info as symbolic
Defining function skb_clone as symbolic
Defining function netdev_warn as symbolic
Removed calls to 'netif_carrier_on' (function is undefined)
Removed calls to 'netif_carrier_off' (function is undefined)
Defining function skb_put as symbolic
Defining function dev_queue_xmit as symbolic
Defining function skb_push as symbolic
Defining function skb_realloc_headroom as symbolic
Removed calls to 'might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function capable as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function attach_hdlc_protocol as symbolic
Defining function alloc_netdev_mqs as symbolic
Defining function register_netdevice as symbolic
Defining function _copy_from_user as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'linkwatch_fire_event' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function dev_close as symbolic
Defining function hdlc_change_mtu as symbolic
Defining function pskb_expand_head as symbolic
Removed calls to 'unregister_hdlc_protocol' (function is undefined)
Removed calls to 'register_hdlc_protocol' (function is undefined)
Defining function ldv_ndo_init_3 as symbolic
Defining function ldv_ndo_uninit_3 as symbolic
Defining function ldv_disconnect_2 as symbolic
Defining function ldv_open_2 as symbolic
Defining function ldv_setup_2 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_ulong_named
INFO: After-slicing optimizations and preparation time: 0.307927131653
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 112 92 545 3317
INFO: Starting verification
KLEE: WARNING ONCE: function "fr_set_link_state" has inline asm
KLEE: WARNING: undefined reference to function: ether_setup
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_3726abc2-af37-49b7-b14c-a79bcd02c994/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:7465: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:6796: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:6926: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:7263: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5960: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5889: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5603: 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 13142 states (over memory cap)
KLEE: WARNING: killing 13873 states (over memory cap)
KLEE: WARNING: killing 10061 states (over memory cap)
KLEE: WARNING: killing 13666 states (over memory cap)
KLEE: WARNING: killing 10379 states (over memory cap)
KLEE: WARNING: killing 9963 states (over memory cap)
KLEE: WARNING: killing 14322 states (over memory cap)
KLEE: WARNING: killing 10778 states (over memory cap)
KLEE: WARNING: killing 10946 states (over memory cap)
KLEE: WARNING: killing 11216 states (over memory cap)
KLEE: WARNING: killing 11095 states (over memory cap)
KLEE: WARNING: killing 10972 states (over memory cap)
KLEE: WARNING: killing 10953 states (over memory cap)
KLEE: WARNING: killing 11125 states (over memory cap)
KLEE: WARNING: killing 11775 states (over memory cap)
KLEE: WARNING: killing 11461 states (over memory cap)
KLEE: WARNING: killing 11827 states (over memory cap)
KLEE: WARNING: killing 11425 states (over memory cap)
KLEE: WARNING: killing 11496 states (over memory cap)
KLEE: WARNING: killing 11665 states (over memory cap)
KLEE: WARNING: killing 11930 states (over memory cap)
KLEE: WARNING: killing 12101 states (over memory cap)
KLEE: WARNING: killing 11982 states (over memory cap)
KLEE: WARNING: killing 12340 states (over memory cap)
KLEE: WARNING: killing 12317 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5603: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12483 states (over memory cap)
KLEE: WARNING: killing 12744 states (over memory cap)
KLEE: WARNING: killing 12622 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5961: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12126 states (over memory cap)
KLEE: WARNING: killing 12948 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5603: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12708 states (over memory cap)
KLEE: WARNING: killing 12869 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-6KcV2a/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wan--hdlc_fr.ko-entry_point_false-unreach-call.cil.out.c:5898: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12847 states (over memory cap)
KLEE: WARNING: killing 13191 states (over memory cap)
KLEE: WARNING: killing 12705 states (over memory cap)
KLEE: WARNING: killing 13229 states (over memory cap)
KLEE: WARNING: killing 13025 states (over memory cap)
KLEE: WARNING: killing 12901 states (over memory cap)
KLEE: WARNING: killing 13157 states (over memory cap)
KLEE: WARNING: killing 13316 states (over memory cap)
KLEE: WARNING: killing 13383 states (over memory cap)
KLEE: WARNING: killing 13171 states (over memory cap)
KLEE: WARNING: killing 13146 states (over memory cap)
KLEE: WARNING: killing 12929 states (over memory cap)
KLEE: WARNING: killing 13902 states (over memory cap)
KLEE: WARNING: killing 13422 states (over memory cap)
KLEE: WARNING: killing 13395 states (over memory cap)
KLEE: WARNING: killing 13364 states (over memory cap)
KLEE: WARNING: killing 13705 states (over memory cap)
KLEE: WARNING: killing 13498 states (over memory cap)
KLEE: WARNING: killing 13470 states (over memory cap)
KLEE: WARNING: killing 13538 states (over memory cap)
KLEE: WARNING: killing 13607 states (over memory cap)
KLEE: WARNING: killing 13397 states (over memory cap)
KLEE: WARNING: killing 13546 states (over memory cap)
KLEE: WARNING: killing 13790 states (over memory cap)
KLEE: WARNING: killing 13583 states (over memory cap)
KLEE: WARNING: killing 13200 states (over memory cap)
KLEE: WARNING: killing 13621 states (over memory cap)
KLEE: WARNING: killing 13334 states (over memory cap)
KLEE: WARNING: killing 13747 states (over memory cap)
KLEE: WARNING: killing 13903 states (over memory cap)
KLEE: WARNING: killing 14138 states (over memory cap)
KLEE: WARNING: killing 13588 states (over memory cap)
KLEE: WARNING: killing 14187 states (over memory cap)
KLEE: WARNING: killing 13722 states (over memory cap)
KLEE: WARNING: killing 13611 states (over memory cap)
KLEE: WARNING: killing 13405 states (over memory cap)
KLEE: WARNING: killing 13905 states (over memory cap)
KLEE: WARNING: killing 14051 states (over memory cap)
KLEE: WARNING: killing 13245 states (over memory cap)
KLEE: WARNING: killing 13657 states (over memory cap)
KLEE: WARNING: killing 13802 states (over memory cap)
KLEE: WARNING: killing 13780 states (over memory cap)
KLEE: WARNING: killing 13838 states (over memory cap)
KLEE: WARNING: killing 14331 states (over memory cap)
KLEE: WARNING: killing 13882 states (over memory cap)
KLEE: WARNING: killing 13777 states (over memory cap)
KLEE: WARNING: killing 14093 states (over memory cap)
KLEE: WARNING: killing 13642 states (over memory cap)
KLEE: WARNING: killing 14476 states (over memory cap)
KLEE: WARNING: killing 13942 states (over memory cap)
KLEE: WARNING: killing 13231 states (over memory cap)
KLEE: WARNING: killing 13548 states (over memory cap)
KLEE: WARNING: killing 13692 states (over memory cap)
KLEE: WARNING: killing 14178 states (over memory cap)
KLEE: WARNING: killing 13305 states (over memory cap)
KLEE: WARNING: killing 13628 states (over memory cap)
KLEE: WARNING: killing 14199 states (over memory cap)
KLEE: WARNING: killing 13498 states (over memory cap)
KLEE: WARNING: killing 13809 states (over memory cap)
KLEE: WARNING: killing 13954 states (over memory cap)
KLEE: WARNING: killing 13685 states (over memory cap)
KLEE: WARNING: killing 14088 states (over memory cap)
KLEE: WARNING: killing 13894 states (over memory cap)
KLEE: WARNING: killing 13952 states (over memory cap)
KLEE: WARNING: killing 13428 states (over memory cap)
KLEE: WARNING: killing 13987 states (over memory cap)
KLEE: WARNING: killing 14551 states (over memory cap)
KLEE: WARNING: killing 14276 states (over memory cap)
KLEE: WARNING: killing 13926 states (over memory cap)
KLEE: WARNING: killing 14074 states (over memory cap)
KLEE: WARNING: killing 13799 states (over memory cap)
KLEE: WARNING: killing 14274 states (over memory cap)
KLEE: WARNING: killing 14084 states (over memory cap)
KLEE: WARNING: killing 13647 states (over memory cap)
KLEE: WARNING: killing 14042 states (over memory cap)
KLEE: WARNING: killing 13936 states (over memory cap)
KLEE: WARNING: killing 13670 states (over memory cap)
KLEE: WARNING: killing 14059 states (over memory cap)
KLEE: WARNING: killing 8124 states (over memory cap)
