bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-usb-gspca-stv06xx-gspca_stv06xx_true-unreach-call.cil.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.: 189 276 1989 9970
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.403789997101
Defining function printk as symbolic
Defining function usb_control_msg as symbolic
Removed calls to 'msleep' (function is undefined)
Removed calls to 'input_event' (function is undefined)
Defining function usb_set_interface as symbolic
Removed calls to 'gspca_frame_add' (function is undefined)
Defining function usb_ifnum_to_if as symbolic
Defining function usb_altnum_to_altsetting as symbolic
Defining function gspca_resume as symbolic
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function ldv_pre_usb_register_driver as symbolic
Defining function v4l2_ctrl_handler_init_class as symbolic
Defining function v4l2_ctrl_new_std as symbolic
Removed calls to 'ldv_after_alloc' (function is undefined)
Defining function external_allocated_data as symbolic
Removed calls to 'v4l2_ctrl_auto_cluster' (function is undefined)
Defining function v4l2_ctrl_new_custom as symbolic
Removed calls to 'gspca_disconnect' (function is undefined)
Defining function gspca_suspend as symbolic
Defining function gspca_dev_probe as symbolic
Removed calls to 'ldv_assert' (function is undefined)
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Linked our definitions to these undefined functions:
  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.3912961483
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 227 270 877 5460
INFO: Starting verification
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_95968c50-8d11-49d6-b8f3-c61b47bfcbb1/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 22245 states (over memory cap)
KLEE: WARNING: killing 29880 states (over memory cap)
KLEE: WARNING: killing 30502 states (over memory cap)
KLEE: WARNING: killing 30193 states (over memory cap)
KLEE: WARNING: killing 28914 states (over memory cap)
KLEE: WARNING: killing 29187 states (over memory cap)
KLEE: WARNING: killing 29468 states (over memory cap)
KLEE: WARNING: killing 28606 states (over memory cap)
KLEE: WARNING: killing 29446 states (over memory cap)
KLEE: WARNING: killing 28982 states (over memory cap)
KLEE: WARNING: killing 28313 states (over memory cap)
KLEE: WARNING: killing 30650 states (over memory cap)
KLEE: WARNING: killing 29612 states (over memory cap)
KLEE: WARNING: killing 30631 states (over memory cap)
KLEE: WARNING: killing 31074 states (over memory cap)
KLEE: WARNING: killing 31532 states (over memory cap)
KLEE: WARNING: killing 31633 states (over memory cap)
KLEE: WARNING: killing 31539 states (over memory cap)
KLEE: WARNING: killing 32724 states (over memory cap)
KLEE: WARNING: killing 31897 states (over memory cap)
KLEE: WARNING: killing 32548 states (over memory cap)
KLEE: WARNING: killing 34280 states (over memory cap)
KLEE: WARNING: killing 18327 states (over memory cap)
KLEE: WARNING: killing 32689 states (over memory cap)
KLEE: WARNING: killing 32624 states (over memory cap)
KLEE: WARNING: killing 33807 states (over memory cap)
KLEE: WARNING: killing 32091 states (over memory cap)
KLEE: WARNING: killing 17942 states (over memory cap)
KLEE: WARNING: killing 31984 states (over memory cap)
KLEE: WARNING: killing 33162 states (over memory cap)
KLEE: WARNING: killing 32378 states (over memory cap)
KLEE: WARNING: killing 32310 states (over memory cap)
KLEE: WARNING: killing 32237 states (over memory cap)
KLEE: WARNING: killing 31448 states (over memory cap)
KLEE: WARNING: killing 31912 states (over memory cap)
KLEE: WARNING: killing 31484 states (over memory cap)
KLEE: WARNING: killing 31600 states (over memory cap)
KLEE: WARNING: killing 30455 states (over memory cap)
KLEE: WARNING: killing 30553 states (over memory cap)
KLEE: WARNING: killing 30828 states (over memory cap)
KLEE: WARNING: killing 30403 states (over memory cap)
KLEE: WARNING: killing 30676 states (over memory cap)
KLEE: WARNING: killing 31131 states (over memory cap)
KLEE: WARNING: killing 30719 states (over memory cap)
KLEE: WARNING: killing 17264 states (over memory cap)
KLEE: WARNING: killing 30785 states (over memory cap)
KLEE: WARNING: killing 29341 states (over memory cap)
KLEE: WARNING: killing 31502 states (over memory cap)
KLEE: WARNING: killing 31441 states (over memory cap)
KLEE: WARNING: killing 31540 states (over memory cap)
KLEE: WARNING: killing 31651 states (over memory cap)
KLEE: WARNING: killing 17182 states (over memory cap)
KLEE: WARNING: killing 30842 states (over memory cap)
KLEE: WARNING: killing 30604 states (over memory cap)
KLEE: WARNING: killing 31740 states (over memory cap)
KLEE: WARNING: killing 31655 states (over memory cap)
KLEE: WARNING: killing 17000 states (over memory cap)
KLEE: WARNING: killing 30391 states (over memory cap)
KLEE: WARNING: killing 17124 states (over memory cap)
KLEE: WARNING: killing 30978 states (over memory cap)
KLEE: WARNING: killing 17077 states (over memory cap)
KLEE: WARNING: killing 30042 states (over memory cap)
KLEE: WARNING: killing 17185 states (over memory cap)
KLEE: WARNING: killing 30601 states (over memory cap)
KLEE: WARNING: killing 16627 states (over memory cap)
KLEE: WARNING: killing 29326 states (over memory cap)
KLEE: WARNING: killing 30425 states (over memory cap)
KLEE: WARNING: killing 17026 states (over memory cap)
KLEE: WARNING: killing 30511 states (over memory cap)
KLEE: WARNING: killing 16655 states (over memory cap)
KLEE: WARNING: killing 29761 states (over memory cap)
KLEE: WARNING: killing 16438 states (over memory cap)
KLEE: WARNING: killing 16408 states (over memory cap)
KLEE: WARNING: killing 30139 states (over memory cap)
KLEE: WARNING: killing 16856 states (over memory cap)
KLEE: WARNING: killing 30365 states (over memory cap)
KLEE: WARNING: killing 17625 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-Ts7fSs/linux-3.14__complex_emg__linux-alloc-spinlock__drivers-media-usb-gspca-stv06xx-gspca_stv06xx_true-unreach-call.cil.c:5923: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 29790 states (over memory cap)
KLEE: WARNING: killing 17083 states (over memory cap)
KLEE: WARNING: killing 30355 states (over memory cap)
KLEE: WARNING: killing 17519 states (over memory cap)
KLEE: WARNING: killing 29932 states (over memory cap)
KLEE: WARNING: killing 17136 states (over memory cap)
KLEE: WARNING: killing 29514 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 16762 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 30706 states (over memory cap)
KLEE: WARNING: killing 16701 states (over memory cap)
