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-08_1a-drivers--media--usb--dvb-usb--dvb-usb-dw2102.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.: 238 90 1513 9145
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.441164016724
Removed calls to 'msleep' (function is undefined)
Removed calls to '__symbol_put' (function is undefined)
Removed calls to 'rc_keydown' (function is undefined)
Defining function printk as symbolic
Defining function usb_control_msg as symbolic
Defining function __symbol_get as symbolic
Defining function __request_module as symbolic
Defining function i2c_transfer as symbolic
Defining function request_firmware as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible_nested as symbolic
Defining function dvb_usb_generic_rw as symbolic
Removed calls to 'dvb_frontend_detach' (function is undefined)
Removed calls to 'i2c_unregister_device' (function is undefined)
Defining function strlcpy as symbolic
Defining function i2c_new_device as symbolic
Removed calls to 'dvb_usb_device_exit' (function is undefined)
Defining function kmemdup as symbolic
Defining function dvb_usb_device_init as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'usb_deregister' (function is undefined)
Defining function ldv_release_7 as symbolic
Defining function ldv_probe_7 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function ldv_release_6 as symbolic
Defining function ldv_probe_6 as symbolic
Defining function ldv_release_3 as symbolic
Defining function ldv_probe_3 as symbolic
Defining function ldv_release_8 as symbolic
Defining function ldv_probe_8 as symbolic
Defining function ldv_release_4 as symbolic
Defining function ldv_probe_4 as symbolic
Defining function ldv_release_5 as symbolic
Defining function ldv_probe_5 as symbolic
Defining function usb_register_driver as symbolic
Linked our definitions to these undefined functions:
  __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.385400772095
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 337 116 773 4929
INFO: Starting verification
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_1e5417b2-08d9-4b17-a48d-10fe5a6a500f/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING: killing 31439 states (over memory cap)
KLEE: WARNING: killing 22661 states (over memory cap)
KLEE: WARNING: killing 21684 states (over memory cap)
KLEE: WARNING: killing 22348 states (over memory cap)
KLEE: WARNING: killing 20794 states (over memory cap)
KLEE: WARNING: killing 22113 states (over memory cap)
KLEE: WARNING: killing 23300 states (over memory cap)
KLEE: WARNING: killing 22801 states (over memory cap)
KLEE: WARNING: killing 23989 states (over memory cap)
KLEE: WARNING: killing 24079 states (over memory cap)
KLEE: WARNING: killing 24499 states (over memory cap)
KLEE: WARNING: killing 24591 states (over memory cap)
KLEE: WARNING: killing 25916 states (over memory cap)
KLEE: WARNING: killing 26603 states (over memory cap)
KLEE: WARNING: killing 27544 states (over memory cap)
KLEE: WARNING: killing 26166 states (over memory cap)
KLEE: WARNING: killing 24594 states (over memory cap)
KLEE: WARNING: killing 24049 states (over memory cap)
KLEE: WARNING: killing 24589 states (over memory cap)
KLEE: WARNING: killing 24695 states (over memory cap)
KLEE: WARNING: killing 25691 states (over memory cap)
KLEE: WARNING: killing 22019 states (over memory cap)
KLEE: WARNING: killing 23513 states (over memory cap)
KLEE: WARNING: killing 24370 states (over memory cap)
KLEE: WARNING: killing 23386 states (over memory cap)
KLEE: WARNING: killing 24000 states (over memory cap)
KLEE: WARNING: killing 24415 states (over memory cap)
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 23766 states (over memory cap)
KLEE: WARNING: killing 25768 states (over memory cap)
KLEE: WARNING: killing 24344 states (over memory cap)
KLEE: WARNING: killing 23878 states (over memory cap)
KLEE: WARNING: killing 24545 states (over memory cap)
KLEE: WARNING: killing 24771 states (over memory cap)
KLEE: WARNING: killing 25005 states (over memory cap)
KLEE: WARNING: killing 23966 states (over memory cap)
KLEE: WARNING: killing 24631 states (over memory cap)
KLEE: WARNING: killing 25302 states (over memory cap)
KLEE: WARNING: killing 23705 states (over memory cap)
KLEE: WARNING: killing 25180 states (over memory cap)
KLEE: WARNING: killing 22835 states (over memory cap)
KLEE: WARNING: killing 24682 states (over memory cap)
KLEE: WARNING: killing 25604 states (over memory cap)
KLEE: WARNING: killing 24023 states (over memory cap)
KLEE: WARNING: killing 24302 states (over memory cap)
KLEE: WARNING: killing 24155 states (over memory cap)
KLEE: WARNING: killing 24816 states (over memory cap)
KLEE: WARNING: killing 23986 states (over memory cap)
KLEE: WARNING: killing 23833 states (over memory cap)
KLEE: WARNING: killing 26484 states (over memory cap)
KLEE: WARNING: killing 24284 states (over memory cap)
KLEE: WARNING: killing 25306 states (over memory cap)
KLEE: WARNING: killing 24170 states (over memory cap)
KLEE: WARNING: killing 24268 states (over memory cap)
KLEE: WARNING: killing 25660 states (over memory cap)
KLEE: WARNING: killing 24834 states (over memory cap)
KLEE: WARNING: killing 24192 states (over memory cap)
KLEE: WARNING: killing 25217 states (over memory cap)
KLEE: WARNING: killing 23894 states (over memory cap)
KLEE: WARNING: killing 23121 states (over memory cap)
KLEE: WARNING: killing 25250 states (over memory cap)
KLEE: WARNING: killing 24370 states (over memory cap)
KLEE: WARNING: killing 24098 states (over memory cap)
KLEE: WARNING: killing 24137 states (over memory cap)
KLEE: WARNING: killing 24475 states (over memory cap)
KLEE: WARNING: killing 24383 states (over memory cap)
KLEE: WARNING: killing 24796 states (over memory cap)
KLEE: WARNING: killing 24772 states (over memory cap)
KLEE: WARNING: killing 25667 states (over memory cap)
KLEE: WARNING: killing 24368 states (over memory cap)
KLEE: WARNING: killing 24095 states (over memory cap)
KLEE: WARNING: killing 26331 states (over memory cap)
KLEE: WARNING: killing 23628 states (over memory cap)
KLEE: WARNING: killing 23420 states (over memory cap)
KLEE: WARNING: killing 23887 states (over memory cap)
KLEE: WARNING: killing 24890 states (over memory cap)
KLEE: WARNING: killing 25292 states (over memory cap)
KLEE: WARNING: killing 24358 states (over memory cap)
KLEE: WARNING: killing 23970 states (over memory cap)
KLEE: WARNING: killing 24799 states (over memory cap)
KLEE: WARNING: killing 26047 states (over memory cap)
KLEE: WARNING: killing 23186 states (over memory cap)
KLEE: WARNING: killing 24789 states (over memory cap)
KLEE: WARNING: killing 24163 states (over memory cap)
KLEE: WARNING: killing 25591 states (over memory cap)
KLEE: WARNING: killing 24191 states (over memory cap)
KLEE: WARNING: killing 24279 states (over memory cap)
KLEE: WARNING: killing 25042 states (over memory cap)
KLEE: WARNING: killing 23886 states (over memory cap)
KLEE: WARNING: killing 24822 states (over memory cap)
KLEE: WARNING: killing 24853 states (over memory cap)
KLEE: WARNING: killing 25257 states (over memory cap)
KLEE: WARNING: killing 24805 states (over memory cap)
KLEE: WARNING: killing 24196 states (over memory cap)
KLEE: WARNING: killing 23275 states (over memory cap)
KLEE: WARNING: killing 24322 states (over memory cap)
KLEE: WARNING: killing 23994 states (over memory cap)
KLEE: WARNING: killing 24635 states (over memory cap)
KLEE: WARNING: killing 24855 states (over memory cap)
KLEE: WARNING: killing 24715 states (over memory cap)
KLEE: WARNING: killing 25235 states (over memory cap)
KLEE: WARNING: killing 23908 states (over memory cap)
KLEE: WARNING: killing 23532 states (over memory cap)
KLEE: WARNING: killing 25471 states (over memory cap)
KLEE: WARNING: killing 24917 states (over memory cap)
KLEE: WARNING: killing 24662 states (over memory cap)
KLEE: WARNING: killing 23692 states (over memory cap)
KLEE: WARNING: killing 24672 states (over memory cap)
KLEE: WARNING: killing 24294 states (over memory cap)
KLEE: WARNING: killing 25279 states (over memory cap)
KLEE: WARNING: killing 24501 states (over memory cap)
KLEE: WARNING: killing 24245 states (over memory cap)
KLEE: WARNING: killing 24043 states (over memory cap)
KLEE: WARNING: killing 23667 states (over memory cap)
KLEE: WARNING: killing 25949 states (over memory cap)
KLEE: WARNING: killing 23924 states (over memory cap)
KLEE: WARNING: killing 24140 states (over memory cap)
KLEE: WARNING: killing 23940 states (over memory cap)
KLEE: WARNING: killing 24560 states (over memory cap)
KLEE: WARNING: killing 25478 states (over memory cap)
KLEE: WARNING: killing 24472 states (over memory cap)
KLEE: WARNING: killing 24448 states (over memory cap)
KLEE: WARNING: killing 24202 states (over memory cap)
KLEE: WARNING: killing 24942 states (over memory cap)
KLEE: WARNING: killing 24742 states (over memory cap)
KLEE: WARNING: killing 23668 states (over memory cap)
KLEE: WARNING: killing 25225 states (over memory cap)
KLEE: WARNING: killing 24328 states (over memory cap)
KLEE: WARNING: killing 24318 states (over memory cap)
KLEE: WARNING: killing 24172 states (over memory cap)
KLEE: WARNING: killing 24860 states (over memory cap)
KLEE: WARNING: killing 24486 states (over memory cap)
KLEE: WARNING: killing 24286 states (over memory cap)
KLEE: WARNING: killing 24265 states (over memory cap)
KLEE: WARNING: killing 25125 states (over memory cap)
KLEE: WARNING: killing 24063 states (over memory cap)
KLEE: WARNING: killing 24857 states (over memory cap)
KLEE: WARNING: killing 24083 states (over memory cap)
KLEE: WARNING: killing 24300 states (over memory cap)
KLEE: WARNING: killing 24557 states (over memory cap)
KLEE: WARNING: killing 23779 states (over memory cap)
KLEE: WARNING: killing 23983 states (over memory cap)
KLEE: WARNING: killing 25173 states (over memory cap)
KLEE: WARNING: killing 25095 states (over memory cap)
KLEE: WARNING: killing 24327 states (over memory cap)
