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-usb-dev__drivers-media-usb-dvb-usb-v2-dvb-usb-mxl111sf_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.: 350 237 2974 15995
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.504697799683
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Defining function usb_set_interface as symbolic
Defining function printk as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Defining function dvb_usbv2_generic_write as symbolic
Defining function dvb_usbv2_generic_rw as symbolic
Defining function i2c_transfer as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'tveeprom_hauppauge_analog' (function is undefined)
Defining function tveeprom_read 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 dvb_usbv2_probe as symbolic
Defining function dvb_usbv2_suspend as symbolic
Defining function dvb_usbv2_resume as symbolic
Defining function mutex_lock_interruptible_nested as symbolic
Defining function external_allocated_data as symbolic
Removed calls to 'dvb_usbv2_disconnect' (function is undefined)
Removed calls to 'ldv_pre_probe' (function is undefined)
Removed calls to 'ldv_check_alloc_flags' (function is undefined)
Removed calls to 'ldv_after_alloc' (function is undefined)
Removed calls to 'ldv_assert' (function is undefined)
Linked our definitions to these undefined functions:
  __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.573929071426
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 385 235 1348 8603
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usbv2_disconnect
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_c14e4188-2d95-4e5d-be10-9f9e3f572490/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 29684 states (over memory cap)
KLEE: WARNING: killing 26692 states (over memory cap)
KLEE: WARNING: killing 24875 states (over memory cap)
KLEE: WARNING: killing 25158 states (over memory cap)
KLEE: WARNING: killing 24308 states (over memory cap)
KLEE: WARNING: killing 24398 states (over memory cap)
KLEE: WARNING: killing 23375 states (over memory cap)
KLEE: WARNING: killing 24219 states (over memory cap)
KLEE: WARNING: killing 24308 states (over memory cap)
KLEE: WARNING: killing 24033 states (over memory cap)
KLEE: WARNING: killing 24510 states (over memory cap)
KLEE: WARNING: killing 24238 states (over memory cap)
KLEE: WARNING: killing 25440 states (over memory cap)
KLEE: WARNING: killing 25555 states (over memory cap)
KLEE: WARNING: killing 26012 states (over memory cap)
KLEE: WARNING: killing 25204 states (over memory cap)
KLEE: WARNING: killing 26384 states (over memory cap)
KLEE: WARNING: killing 26130 states (over memory cap)
KLEE: WARNING: killing 26767 states (over memory cap)
KLEE: WARNING: killing 27244 states (over memory cap)
KLEE: WARNING: killing 27536 states (over memory cap)
KLEE: WARNING: killing 27644 states (over memory cap)
KLEE: WARNING: killing 28283 states (over memory cap)
KLEE: WARNING: killing 27682 states (over memory cap)
KLEE: WARNING: killing 27967 states (over memory cap)
KLEE: WARNING: killing 27900 states (over memory cap)
KLEE: WARNING: killing 26774 states (over memory cap)
KLEE: WARNING: killing 28310 states (over memory cap)
KLEE: WARNING: killing 26827 states (over memory cap)
KLEE: WARNING: killing 26946 states (over memory cap)
KLEE: WARNING: killing 26358 states (over memory cap)
KLEE: WARNING: killing 26475 states (over memory cap)
KLEE: WARNING: killing 25362 states (over memory cap)
KLEE: WARNING: killing 25991 states (over memory cap)
KLEE: WARNING: killing 25412 states (over memory cap)
KLEE: WARNING: killing 25693 states (over memory cap)
KLEE: WARNING: killing 25479 states (over memory cap)
KLEE: WARNING: killing 26096 states (over memory cap)
KLEE: WARNING: killing 26035 states (over memory cap)
KLEE: WARNING: killing 25462 states (over memory cap)
KLEE: WARNING: killing 25235 states (over memory cap)
KLEE: WARNING: killing 26372 states (over memory cap)
KLEE: WARNING: killing 25277 states (over memory cap)
KLEE: WARNING: killing 25396 states (over memory cap)
KLEE: WARNING: killing 26184 states (over memory cap)
KLEE: WARNING: killing 25279 states (over memory cap)
KLEE: WARNING: killing 26236 states (over memory cap)
KLEE: WARNING: killing 26175 states (over memory cap)
KLEE: WARNING: killing 26296 states (over memory cap)
KLEE: WARNING: killing 25549 states (over memory cap)
KLEE: WARNING: killing 25662 states (over memory cap)
KLEE: WARNING: killing 24612 states (over memory cap)
KLEE: WARNING: killing 26228 states (over memory cap)
KLEE: WARNING: killing 25838 states (over memory cap)
KLEE: WARNING: killing 26459 states (over memory cap)
KLEE: WARNING: killing 26890 states (over memory cap)
KLEE: WARNING: killing 27508 states (over memory cap)
KLEE: WARNING: killing 26782 states (over memory cap)
KLEE: WARNING: killing 26230 states (over memory cap)
KLEE: WARNING: killing 25508 states (over memory cap)
KLEE: WARNING: killing 26118 states (over memory cap)
KLEE: WARNING: killing 26061 states (over memory cap)
KLEE: WARNING: killing 25670 states (over memory cap)
KLEE: WARNING: killing 25288 states (over memory cap)
KLEE: WARNING: killing 26050 states (over memory cap)
KLEE: WARNING: killing 25518 states (over memory cap)
KLEE: WARNING: killing 25458 states (over memory cap)
KLEE: WARNING: killing 25729 states (over memory cap)
KLEE: WARNING: killing 25852 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xaIdDD/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-v2-dvb-usb-mxl111sf_true-unreach-call.cil.c:9075: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xaIdDD/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-v2-dvb-usb-mxl111sf_true-unreach-call.cil.c:7472: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 24981 states (over memory cap)
KLEE: WARNING: killing 25736 states (over memory cap)
KLEE: WARNING: killing 25195 states (over memory cap)
KLEE: WARNING: killing 25298 states (over memory cap)
KLEE: WARNING: killing 26538 states (over memory cap)
KLEE: WARNING: killing 25999 states (over memory cap)
KLEE: WARNING: killing 25799 states (over memory cap)
KLEE: WARNING: killing 25432 states (over memory cap)
KLEE: WARNING: killing 26479 states (over memory cap)
KLEE: WARNING: killing 26115 states (over memory cap)
KLEE: ERROR: /tmp/symbiotic-xaIdDD/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-v2-dvb-usb-mxl111sf_true-unreach-call.cil.c:17050: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xaIdDD/linux-3.14__complex_emg__linux-usb-dev__drivers-media-usb-dvb-usb-v2-dvb-usb-mxl111sf_true-unreach-call.cil.c:7094: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 26385 states (over memory cap)
