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-drivers-clk1__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 221 2925 15735
Removed infinite loop in ldv_assume
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.50755405426
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 'ldv_initialize' (function is undefined)
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.568137168884
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 385 220 1315 8473
INFO: Starting verification
KLEE: WARNING: undefined reference to function: dvb_usbv2_disconnect
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_5a7dbb63-5747-4d44-9266-57db099e4e04/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 27564 states (over memory cap)
KLEE: WARNING: killing 26310 states (over memory cap)
KLEE: WARNING: killing 26013 states (over memory cap)
KLEE: WARNING: killing 25151 states (over memory cap)
KLEE: WARNING: killing 25050 states (over memory cap)
KLEE: WARNING: killing 24581 states (over memory cap)
KLEE: WARNING: killing 25057 states (over memory cap)
KLEE: WARNING: killing 24396 states (over memory cap)
KLEE: WARNING: killing 24860 states (over memory cap)
KLEE: WARNING: killing 24218 states (over memory cap)
KLEE: WARNING: killing 25807 states (over memory cap)
KLEE: WARNING: killing 25165 states (over memory cap)
KLEE: WARNING: killing 24889 states (over memory cap)
KLEE: WARNING: killing 24812 states (over memory cap)
KLEE: WARNING: killing 25273 states (over memory cap)
KLEE: WARNING: killing 25560 states (over memory cap)
KLEE: WARNING: killing 25842 states (over memory cap)
KLEE: WARNING: killing 26665 states (over memory cap)
KLEE: WARNING: killing 26778 states (over memory cap)
KLEE: WARNING: killing 27237 states (over memory cap)
KLEE: WARNING: killing 27344 states (over memory cap)
KLEE: WARNING: killing 27469 states (over memory cap)
KLEE: WARNING: killing 28111 states (over memory cap)
KLEE: WARNING: killing 27503 states (over memory cap)
KLEE: WARNING: killing 26904 states (over memory cap)
KLEE: WARNING: killing 27197 states (over memory cap)
KLEE: WARNING: killing 27125 states (over memory cap)
KLEE: WARNING: killing 27424 states (over memory cap)
KLEE: WARNING: killing 27883 states (over memory cap)
KLEE: WARNING: killing 27122 states (over memory cap)
KLEE: WARNING: killing 26003 states (over memory cap)
KLEE: WARNING: killing 26119 states (over memory cap)
KLEE: WARNING: killing 26746 states (over memory cap)
KLEE: WARNING: killing 25475 states (over memory cap)
KLEE: WARNING: killing 25238 states (over memory cap)
KLEE: WARNING: killing 25691 states (over memory cap)
KLEE: WARNING: killing 26486 states (over memory cap)
KLEE: WARNING: killing 25572 states (over memory cap)
KLEE: WARNING: killing 25682 states (over memory cap)
KLEE: WARNING: killing 25440 states (over memory cap)
KLEE: WARNING: killing 25556 states (over memory cap)
KLEE: WARNING: killing 26692 states (over memory cap)
KLEE: WARNING: killing 25775 states (over memory cap)
KLEE: WARNING: killing 25382 states (over memory cap)
KLEE: WARNING: killing 25317 states (over memory cap)
KLEE: WARNING: killing 25764 states (over memory cap)
KLEE: WARNING: killing 26037 states (over memory cap)
KLEE: WARNING: killing 25817 states (over memory cap)
KLEE: WARNING: killing 25258 states (over memory cap)
KLEE: WARNING: killing 26376 states (over memory cap)
KLEE: WARNING: killing 26489 states (over memory cap)
KLEE: WARNING: killing 25764 states (over memory cap)
KLEE: WARNING: killing 26377 states (over memory cap)
KLEE: WARNING: killing 25829 states (over memory cap)
KLEE: WARNING: killing 26281 states (over memory cap)
KLEE: WARNING: killing 25906 states (over memory cap)
KLEE: WARNING: killing 26331 states (over memory cap)
KLEE: WARNING: killing 25943 states (over memory cap)
KLEE: WARNING: killing 25730 states (over memory cap)
KLEE: WARNING: killing 26016 states (over memory cap)
KLEE: WARNING: killing 26127 states (over memory cap)
KLEE: WARNING: killing 26244 states (over memory cap)
KLEE: WARNING: killing 25683 states (over memory cap)
KLEE: WARNING: killing 25628 states (over memory cap)
KLEE: WARNING: killing 24917 states (over memory cap)
KLEE: WARNING: killing 25681 states (over memory cap)
KLEE: WARNING: killing 25791 states (over memory cap)
KLEE: WARNING: killing 26393 states (over memory cap)
KLEE: WARNING: killing 26028 states (over memory cap)
KLEE: WARNING: killing 25481 states (over memory cap)
KLEE: WARNING: killing 25753 states (over memory cap)
KLEE: WARNING: killing 26191 states (over memory cap)
KLEE: WARNING: killing 25970 states (over memory cap)
KLEE: WARNING: killing 25602 states (over memory cap)
KLEE: WARNING: killing 26033 states (over memory cap)
KLEE: WARNING: killing 25353 states (over memory cap)
KLEE: WARNING: killing 25772 states (over memory cap)
KLEE: WARNING: killing 26526 states (over memory cap)
KLEE: WARNING: killing 26159 states (over memory cap)
KLEE: WARNING: killing 25002 states (over memory cap)
KLEE: WARNING: killing 26051 states (over memory cap)
KLEE: WARNING: killing 25696 states (over memory cap)
KLEE: WARNING: killing 25002 states (over memory cap)
KLEE: WARNING: killing 25908 states (over memory cap)
KLEE: WARNING: killing 25702 states (over memory cap)
KLEE: WARNING: killing 26583 states (over memory cap)
KLEE: WARNING: killing 24972 states (over memory cap)
KLEE: WARNING: killing 26031 states (over memory cap)
KLEE: WARNING: killing 25657 states (over memory cap)
KLEE: WARNING: killing 26090 states (over memory cap)
KLEE: WARNING: killing 25554 states (over memory cap)
KLEE: WARNING: killing 25659 states (over memory cap)
KLEE: WARNING: killing 26547 states (over memory cap)
KLEE: WARNING: killing 26032 states (over memory cap)
KLEE: WARNING: killing 26759 states (over memory cap)
