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--wireless--at76c50x-usb.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.: 248 146 1328 8805
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.440697908401
Removed calls to '__dev_kfree_skb_any' (function is undefined)
Removed calls to 'ieee80211_queue_work' (function is undefined)
Removed calls to 'ieee80211_stop_queues' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'ieee80211_queue_delayed_work' (function is undefined)
Defining function printk as symbolic
Defining function dev_err as symbolic
Defining function usb_control_msg as symbolic
Defining function _dev_info as symbolic
Defining function schedule_timeout_interruptible as symbolic
Defining function cancel_delayed_work as symbolic
Defining function cancel_work_sync as symbolic
Removed calls to 'skb_trim' (function is undefined)
Defining function skb_push as symbolic
Defining function skb_put as symbolic
Removed calls to '__tasklet_schedule' (function is undefined)
Defining function usb_submit_urb as symbolic
Removed calls to 'ieee80211_tx_status_irqsafe' (function is undefined)
Removed calls to 'ieee80211_wake_queues' (function is undefined)
Defining function mod_timer as symbolic
Removed calls to 'led_trigger_event' (function is undefined)
Removed calls to 'usb_put_dev' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to '__init_work' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to 'init_timer_key' (function is undefined)
Removed calls to 'tasklet_init' (function is undefined)
Removed calls to 'tasklet_kill' (function is undefined)
Removed calls to 'ieee80211_unregister_hw' (function is undefined)
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'ieee80211_free_hw' (function is undefined)
Defining function del_timer_sync as symbolic
Defining function usb_get_dev as symbolic
Defining function dev_printk as symbolic
Defining function snprintf as symbolic
Defining function ieee80211_register_hw as symbolic
Defining function usb_alloc_urb as symbolic
Defining function ieee80211_alloc_hw as symbolic
Removed calls to 'ieee80211_scan_completed' (function is undefined)
Removed calls to 'ieee80211_rx_irqsafe' (function is undefined)
Defining function skb_pull as symbolic
Defining function cfg80211_find_ie as symbolic
Defining function ieee80211_channel_to_frequency as symbolic
Defining function usb_reset_device as symbolic
Defining function msecs_to_jiffies as symbolic
Defining function request_firmware as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'led_trigger_unregister_simple' (function is undefined)
Removed calls to 'led_trigger_register_simple' (function is undefined)
Defining function usb_register_driver 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_u32_named
  __VERIFIER_nondet_uint_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.412779092789
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 186 98 484 3751
INFO: Starting verification
KLEE: WARNING ONCE: function "at76_rx_callback" has inline asm
KLEE: WARNING: undefined reference to variable: boot_tvec_bases
KLEE: WARNING: undefined reference to function: delayed_work_timer_fn
KLEE: WARNING: Type for boot_tvec_bases is not sized
KLEE: WARNING: Unable to find size for global variable: boot_tvec_bases (use will result in out of bounds access)
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_52d933b4-e2e5-4daf-b0ba-34b9e5246b6a/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10218: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10792: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:9898: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10317: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10013: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10264: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10066: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:7374: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10397: 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 11426 states (over memory cap)
KLEE: WARNING: killing 11464 states (over memory cap)
KLEE: WARNING: killing 10723 states (over memory cap)
KLEE: WARNING: killing 11292 states (over memory cap)
KLEE: WARNING: killing 11428 states (over memory cap)
KLEE: WARNING: killing 11567 states (over memory cap)
KLEE: WARNING: killing 11617 states (over memory cap)
KLEE: WARNING: killing 11669 states (over memory cap)
KLEE: WARNING: killing 11896 states (over memory cap)
KLEE: WARNING: killing 12030 states (over memory cap)
KLEE: WARNING: killing 12519 states (over memory cap)
KLEE: WARNING: killing 12145 states (over memory cap)
KLEE: WARNING: killing 12368 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:9097: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:9899: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12001 states (over memory cap)
KLEE: WARNING: killing 12393 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10325: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10242: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11934 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10295: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12162 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10074: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 11877 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10326: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12267 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10404: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12660 states (over memory cap)
KLEE: WARNING: killing 12289 states (over memory cap)
KLEE: WARNING: killing 11759 states (over memory cap)
KLEE: WARNING: killing 12645 states (over memory cap)
KLEE: ERROR: (location information missing) memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12615 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10155: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12586 states (over memory cap)
KLEE: WARNING: killing 12805 states (over memory cap)
KLEE: WARNING: killing 12282 states (over memory cap)
KLEE: WARNING: killing 12333 states (over memory cap)
KLEE: WARNING: killing 12628 states (over memory cap)
KLEE: WARNING: killing 12683 states (over memory cap)
KLEE: WARNING: killing 13062 states (over memory cap)
KLEE: WARNING: killing 12623 states (over memory cap)
KLEE: WARNING: killing 12515 states (over memory cap)
KLEE: WARNING: killing 12731 states (over memory cap)
KLEE: WARNING: killing 12700 states (over memory cap)
KLEE: WARNING: killing 12508 states (over memory cap)
KLEE: WARNING: killing 12721 states (over memory cap)
KLEE: WARNING: killing 12773 states (over memory cap)
KLEE: WARNING: killing 12419 states (over memory cap)
KLEE: WARNING: killing 12152 states (over memory cap)
KLEE: WARNING: killing 12602 states (over memory cap)
KLEE: WARNING: killing 12654 states (over memory cap)
KLEE: WARNING: killing 12864 states (over memory cap)
KLEE: WARNING: killing 12839 states (over memory cap)
KLEE: WARNING: killing 13126 states (over memory cap)
KLEE: WARNING: killing 13022 states (over memory cap)
KLEE: WARNING: killing 12603 states (over memory cap)
KLEE: WARNING: killing 13048 states (over memory cap)
KLEE: WARNING: killing 12308 states (over memory cap)
KLEE: WARNING: killing 12906 states (over memory cap)
KLEE: WARNING: killing 12725 states (over memory cap)
KLEE: WARNING: killing 12778 states (over memory cap)
KLEE: WARNING: killing 12520 states (over memory cap)
KLEE: WARNING: killing 12495 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 12993 states (over memory cap)
KLEE: WARNING: killing 12496 states (over memory cap)
KLEE: WARNING: killing 12707 states (over memory cap)
KLEE: WARNING: killing 12911 states (over memory cap)
KLEE: WARNING: killing 12731 states (over memory cap)
KLEE: WARNING: killing 12779 states (over memory cap)
KLEE: WARNING: killing 12372 states (over memory cap)
KLEE: WARNING: killing 12732 states (over memory cap)
KLEE: WARNING: killing 12708 states (over memory cap)
KLEE: WARNING: killing 13070 states (over memory cap)
KLEE: WARNING: killing 12818 states (over memory cap)
KLEE: WARNING: killing 12642 states (over memory cap)
KLEE: WARNING: killing 12616 states (over memory cap)
KLEE: WARNING: killing 12743 states (over memory cap)
KLEE: WARNING: killing 12722 states (over memory cap)
KLEE: WARNING: killing 12702 states (over memory cap)
KLEE: WARNING: killing 12604 states (over memory cap)
KLEE: WARNING: killing 12801 states (over memory cap)
KLEE: WARNING: killing 12635 states (over memory cap)
KLEE: WARNING: killing 12690 states (over memory cap)
KLEE: WARNING: killing 12589 states (over memory cap)
KLEE: WARNING: killing 12416 states (over memory cap)
KLEE: WARNING: killing 13069 states (over memory cap)
KLEE: WARNING: killing 12447 states (over memory cap)
KLEE: WARNING: killing 12350 states (over memory cap)
KLEE: WARNING: killing 12699 states (over memory cap)
KLEE: WARNING: killing 12750 states (over memory cap)
KLEE: WARNING: killing 12660 states (over memory cap)
KLEE: WARNING: killing 12570 states (over memory cap)
KLEE: WARNING: killing 12772 states (over memory cap)
KLEE: WARNING: killing 13122 states (over memory cap)
KLEE: WARNING: killing 12588 states (over memory cap)
KLEE: WARNING: killing 12639 states (over memory cap)
KLEE: WARNING: killing 12690 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xkcfNz/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--at76c50x-usb.ko-entry_point_false-unreach-call.cil.out.c:10163: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 12526 states (over memory cap)
KLEE: WARNING: killing 12654 states (over memory cap)
KLEE: WARNING: killing 12624 states (over memory cap)
KLEE: WARNING: killing 12456 states (over memory cap)
KLEE: WARNING: killing 12804 states (over memory cap)
KLEE: WARNING: killing 12708 states (over memory cap)
KLEE: WARNING: killing 12399 states (over memory cap)
KLEE: WARNING: killing 12815 states (over memory cap)
