bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko-entry_point_true-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.: 123 145 1119 6425
Removed infinite loop in ttusb_process_frame
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.423829078674
Defining function printk as symbolic
Removed calls to 'mutex_unlock' (function is undefined)
Defining function usb_bulk_msg as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function request_firmware as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'release_firmware' (function is undefined)
Removed calls to 'dvb_dmxdev_release' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'dvb_frontend_detach' (function is undefined)
Removed calls to 'dvb_dmx_release' (function is undefined)
Removed calls to 'i2c_del_adapter' (function is undefined)
Removed calls to 'usb_kill_urb' (function is undefined)
Removed calls to 'dvb_net_release' (function is undefined)
Defining function dvb_unregister_frontend as symbolic
Defining function dvb_unregister_adapter as symbolic
Removed calls to 'usb_free_urb' (function is undefined)
Removed calls to 'dma_free_attrs' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function dvb_register_adapter as symbolic
Defining function i2c_add_adapter as symbolic
Defining function dvb_dmx_init as symbolic
Defining function dvb_dmxdev_init as symbolic
Defining function dvb_net_init as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Removed calls to 'msleep' (function is undefined)
Defining function dvb_register_frontend as symbolic
Defining function i2c_transfer as symbolic
Removed calls to 'dvb_dmx_swfilter_packets' (function is undefined)
Defining function usb_submit_urb as symbolic
Defining function usb_alloc_urb as symbolic
Defining function dma_alloc_attrs as symbolic
Defining function usb_set_interface as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function usb_register_driver as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memcmp
  strcpy
  __kmalloc
  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.405011892319
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 172 146 686 3595
INFO: Starting verification
KLEE: WARNING ONCE: function "ttusb_iso_irq" has inline asm
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_c541213a-d1dd-49d6-950c-5dab5f26e63f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3TTgJh/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko-entry_point_true-unreach-call.cil.out.c:8463: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-3TTgJh/linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--ttusb-budget--dvb-ttusb-budget.ko-entry_point_true-unreach-call.cil.out.c:9197: 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 17944 states (over memory cap)
KLEE: WARNING: killing 15871 states (over memory cap)
KLEE: WARNING: killing 15683 states (over memory cap)
KLEE: WARNING: killing 15252 states (over memory cap)
KLEE: WARNING: killing 15679 states (over memory cap)
KLEE: WARNING: killing 15493 states (over memory cap)
KLEE: WARNING: killing 15439 states (over memory cap)
KLEE: WARNING: killing 15259 states (over memory cap)
KLEE: WARNING: killing 15808 states (over memory cap)
KLEE: WARNING: killing 15635 states (over memory cap)
KLEE: WARNING: killing 16065 states (over memory cap)
KLEE: WARNING: killing 16255 states (over memory cap)
KLEE: WARNING: killing 16326 states (over memory cap)
KLEE: WARNING: killing 16283 states (over memory cap)
KLEE: WARNING: killing 16949 states (over memory cap)
KLEE: WARNING: killing 16908 states (over memory cap)
KLEE: WARNING: killing 16629 states (over memory cap)
KLEE: WARNING: killing 16574 states (over memory cap)
KLEE: WARNING: killing 16417 states (over memory cap)
KLEE: WARNING: killing 16367 states (over memory cap)
KLEE: WARNING: killing 16559 states (over memory cap)
KLEE: WARNING: killing 16518 states (over memory cap)
KLEE: WARNING: killing 16468 states (over memory cap)
KLEE: WARNING: killing 16315 states (over memory cap)
KLEE: WARNING: killing 16272 states (over memory cap)
KLEE: WARNING: killing 16221 states (over memory cap)
KLEE: WARNING: killing 16759 states (over memory cap)
KLEE: WARNING: killing 16714 states (over memory cap)
KLEE: WARNING: killing 16103 states (over memory cap)
KLEE: WARNING: killing 16407 states (over memory cap)
KLEE: WARNING: killing 16244 states (over memory cap)
KLEE: WARNING: killing 16202 states (over memory cap)
KLEE: WARNING: killing 15811 states (over memory cap)
KLEE: WARNING: killing 16455 states (over memory cap)
KLEE: WARNING: killing 16190 states (over memory cap)
KLEE: WARNING: killing 16485 states (over memory cap)
KLEE: WARNING: killing 15541 states (over memory cap)
KLEE: WARNING: killing 15949 states (over memory cap)
KLEE: WARNING: killing 16468 states (over memory cap)
KLEE: WARNING: killing 16094 states (over memory cap)
KLEE: WARNING: killing 16509 states (over memory cap)
KLEE: WARNING: killing 16243 states (over memory cap)
KLEE: WARNING: killing 16430 states (over memory cap)
KLEE: WARNING: killing 16509 states (over memory cap)
KLEE: WARNING: killing 16692 states (over memory cap)
KLEE: WARNING: killing 16661 states (over memory cap)
KLEE: WARNING: killing 16406 states (over memory cap)
KLEE: WARNING: killing 16146 states (over memory cap)
KLEE: WARNING: killing 16664 states (over memory cap)
KLEE: WARNING: killing 16520 states (over memory cap)
KLEE: WARNING: killing 16698 states (over memory cap)
KLEE: WARNING: killing 16007 states (over memory cap)
KLEE: WARNING: killing 16629 states (over memory cap)
KLEE: WARNING: killing 16373 states (over memory cap)
KLEE: WARNING: killing 16338 states (over memory cap)
KLEE: WARNING: killing 16313 states (over memory cap)
KLEE: WARNING: killing 16272 states (over memory cap)
KLEE: WARNING: killing 16234 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16283 states (over memory cap)
KLEE: WARNING: killing 16784 states (over memory cap)
KLEE: WARNING: killing 16430 states (over memory cap)
KLEE: WARNING: killing 16075 states (over memory cap)
KLEE: WARNING: killing 16467 states (over memory cap)
KLEE: WARNING: killing 16109 states (over memory cap)
KLEE: WARNING: killing 16724 states (over memory cap)
KLEE: WARNING: killing 16264 states (over memory cap)
KLEE: WARNING: killing 16442 states (over memory cap)
KLEE: WARNING: killing 16527 states (over memory cap)
KLEE: WARNING: killing 16490 states (over memory cap)
KLEE: WARNING: killing 16248 states (over memory cap)
KLEE: WARNING: killing 16211 states (over memory cap)
KLEE: WARNING: killing 16288 states (over memory cap)
KLEE: WARNING: killing 16466 states (over memory cap)
KLEE: WARNING: killing 16642 states (over memory cap)
KLEE: WARNING: killing 16093 states (over memory cap)
KLEE: WARNING: killing 16486 states (over memory cap)
KLEE: WARNING: killing 16245 states (over memory cap)
KLEE: WARNING: killing 16316 states (over memory cap)
KLEE: WARNING: killing 16080 states (over memory cap)
KLEE: WARNING: killing 16049 states (over memory cap)
KLEE: WARNING: killing 16424 states (over memory cap)
KLEE: WARNING: killing 16600 states (over memory cap)
KLEE: WARNING: killing 16157 states (over memory cap)
KLEE: WARNING: killing 16224 states (over memory cap)
KLEE: WARNING: killing 16503 states (over memory cap)
KLEE: WARNING: killing 16481 states (over memory cap)
KLEE: WARNING: killing 16140 states (over memory cap)
KLEE: WARNING: killing 16210 states (over memory cap)
KLEE: WARNING: killing 16085 states (over memory cap)
KLEE: WARNING: killing 16160 states (over memory cap)
KLEE: WARNING: killing 16122 states (over memory cap)
KLEE: WARNING: killing 16400 states (over memory cap)
KLEE: WARNING: killing 16779 states (over memory cap)
KLEE: WARNING: killing 16850 states (over memory cap)
KLEE: WARNING: killing 16221 states (over memory cap)
KLEE: WARNING: killing 16095 states (over memory cap)
KLEE: WARNING: killing 16063 states (over memory cap)
KLEE: WARNING: killing 16231 states (over memory cap)
KLEE: WARNING: killing 16206 states (over memory cap)
KLEE: WARNING: killing 16276 states (over memory cap)
KLEE: WARNING: killing 15753 states (over memory cap)
KLEE: WARNING: killing 16314 states (over memory cap)
KLEE: WARNING: killing 16484 states (over memory cap)
KLEE: WARNING: killing 15948 states (over memory cap)
KLEE: WARNING: killing 16116 states (over memory cap)
KLEE: WARNING: killing 16289 states (over memory cap)
KLEE: WARNING: killing 16661 states (over memory cap)
KLEE: WARNING: killing 16533 states (over memory cap)
KLEE: WARNING: killing 16315 states (over memory cap)
KLEE: WARNING: killing 15985 states (over memory cap)
KLEE: WARNING: killing 16450 states (over memory cap)
KLEE: WARNING: killing 16030 states (over memory cap)
KLEE: WARNING: killing 16204 states (over memory cap)
KLEE: WARNING: killing 16658 states (over memory cap)
KLEE: WARNING: killing 16442 states (over memory cap)
KLEE: WARNING: killing 16418 states (over memory cap)
KLEE: WARNING: killing 16578 states (over memory cap)
KLEE: WARNING: killing 16167 states (over memory cap)
KLEE: WARNING: killing 15938 states (over memory cap)
KLEE: WARNING: killing 16397 states (over memory cap)
KLEE: WARNING: killing 16261 states (over memory cap)
KLEE: WARNING: killing 16143 states (over memory cap)
KLEE: WARNING: killing 16111 states (over memory cap)
KLEE: WARNING: killing 9518 states (over memory cap)
KLEE: WARNING: killing 15406 states (over memory cap)
KLEE: WARNING: killing 16234 states (over memory cap)
KLEE: WARNING: killing 16305 states (over memory cap)
