bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--usb--misc--idmouse.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.: 48 60 372 1813
Removed infinite loop in ldv_stop___0
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.178635120392
Defining function default_llseek as symbolic
Removed calls to 'mutex_lock_nested' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function usb_find_interface as symbolic
Defining function usb_control_msg as symbolic
Defining function usb_bulk_msg as symbolic
Defining function simple_read_from_buffer as symbolic
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'usb_deregister_dev' (function is undefined)
Defining function _dev_info as symbolic
Defining function dev_err as symbolic
Defining function usb_register_dev 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
Linked our definitions to these undefined functions:
  __kmalloc
  __memcpy
  kfree
  __VERIFIER_assume
  __VERIFIER_calloc0
  __VERIFIER_error
  __VERIFIER_exit
  __VERIFIER_make_symbolic
  __VERIFIER_malloc0
  __VERIFIER_nondet_int_named
  __VERIFIER_nondet_loff_t_named
  __VERIFIER_nondet_pointer_named
  __VERIFIER_nondet_size_t_named
  __VERIFIER_nondet_ulong_named
INFO: After-slicing optimizations and preparation time: 0.205416202545
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 88 62 223 1142
INFO: Starting verification
KLEE: WARNING ONCE: function "idmouse_open" 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_dc2f3fc9-73fc-4ba5-b859-c04057257717/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-utxmiw/linux-3.12-rc1.tar.xz-144_2a-drivers--usb--misc--idmouse.ko-entry_point_false-unreach-call.cil.out.c:3483: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-utxmiw/linux-3.12-rc1.tar.xz-144_2a-drivers--usb--misc--idmouse.ko-entry_point_false-unreach-call.cil.out.c:4024: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-utxmiw/linux-3.12-rc1.tar.xz-144_2a-drivers--usb--misc--idmouse.ko-entry_point_false-unreach-call.cil.out.c:4025: 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 11988 states (over memory cap)
KLEE: WARNING: killing 12607 states (over memory cap)
KLEE: WARNING: killing 12648 states (over memory cap)
KLEE: WARNING: killing 12471 states (over memory cap)
KLEE: WARNING: killing 12966 states (over memory cap)
KLEE: WARNING: killing 13129 states (over memory cap)
KLEE: WARNING: killing 13403 states (over memory cap)
KLEE: WARNING: killing 13451 states (over memory cap)
KLEE: WARNING: killing 13507 states (over memory cap)
KLEE: WARNING: killing 13671 states (over memory cap)
KLEE: WARNING: killing 14058 states (over memory cap)
KLEE: WARNING: killing 14229 states (over memory cap)
KLEE: WARNING: killing 14396 states (over memory cap)
KLEE: WARNING: killing 14561 states (over memory cap)
KLEE: WARNING: killing 14299 states (over memory cap)
KLEE: WARNING: killing 14577 states (over memory cap)
KLEE: WARNING: killing 14634 states (over memory cap)
KLEE: WARNING: killing 14691 states (over memory cap)
KLEE: WARNING: killing 14961 states (over memory cap)
KLEE: WARNING: killing 14801 states (over memory cap)
KLEE: WARNING: killing 14532 states (over memory cap)
KLEE: WARNING: killing 10728 states (over memory cap)
KLEE: WARNING: killing 15085 states (over memory cap)
KLEE: WARNING: killing 10881 states (over memory cap)
KLEE: WARNING: killing 15325 states (over memory cap)
KLEE: WARNING: killing 10930 states (over memory cap)
KLEE: WARNING: killing 14934 states (over memory cap)
KLEE: WARNING: killing 10872 states (over memory cap)
KLEE: WARNING: killing 14852 states (over memory cap)
KLEE: WARNING: killing 10400 states (over memory cap)
KLEE: WARNING: killing 10584 states (over memory cap)
KLEE: WARNING: killing 10864 states (over memory cap)
KLEE: WARNING: killing 14908 states (over memory cap)
KLEE: WARNING: killing 11210 states (over memory cap)
KLEE: WARNING: killing 10986 states (over memory cap)
KLEE: WARNING: killing 10352 states (over memory cap)
KLEE: WARNING: killing 10737 states (over memory cap)
KLEE: WARNING: killing 10718 states (over memory cap)
KLEE: WARNING: killing 10698 states (over memory cap)
KLEE: WARNING: killing 10571 states (over memory cap)
KLEE: WARNING: killing 10750 states (over memory cap)
KLEE: WARNING: killing 10625 states (over memory cap)
KLEE: WARNING: killing 10700 states (over memory cap)
KLEE: WARNING: killing 10875 states (over memory cap)
KLEE: WARNING: killing 10754 states (over memory cap)
KLEE: WARNING: killing 10829 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 10779 states (over memory cap)
KLEE: WARNING: killing 10461 states (over memory cap)
KLEE: WARNING: killing 10829 states (over memory cap)
KLEE: WARNING: killing 10614 states (over memory cap)
KLEE: WARNING: killing 10393 states (over memory cap)
KLEE: WARNING: killing 10662 states (over memory cap)
KLEE: WARNING: killing 10743 states (over memory cap)
KLEE: WARNING: killing 11116 states (over memory cap)
KLEE: WARNING: killing 10701 states (over memory cap)
KLEE: WARNING: killing 10775 states (over memory cap)
KLEE: WARNING: killing 10850 states (over memory cap)
KLEE: WARNING: killing 10738 states (over memory cap)
KLEE: WARNING: killing 10809 states (over memory cap)
KLEE: WARNING: killing 10887 states (over memory cap)
KLEE: WARNING: killing 10767 states (over memory cap)
KLEE: WARNING: killing 10554 states (over memory cap)
KLEE: WARNING: killing 10631 states (over memory cap)
KLEE: WARNING: killing 11089 states (over memory cap)
KLEE: WARNING: killing 11164 states (over memory cap)
KLEE: WARNING: killing 10761 states (over memory cap)
KLEE: WARNING: killing 10833 states (over memory cap)
KLEE: WARNING: killing 10903 states (over memory cap)
KLEE: WARNING: killing 10886 states (over memory cap)
KLEE: WARNING: killing 10958 states (over memory cap)
KLEE: WARNING: killing 10848 states (over memory cap)
KLEE: WARNING: killing 10544 states (over memory cap)
KLEE: WARNING: killing 10714 states (over memory cap)
KLEE: WARNING: killing 10976 states (over memory cap)
KLEE: WARNING: killing 10770 states (over memory cap)
KLEE: WARNING: killing 10556 states (over memory cap)
KLEE: WARNING: killing 10913 states (over memory cap)
KLEE: WARNING: killing 11270 states (over memory cap)
KLEE: WARNING: killing 11066 states (over memory cap)
KLEE: WARNING: killing 11043 states (over memory cap)
KLEE: WARNING: killing 11023 states (over memory cap)
KLEE: WARNING: killing 10719 states (over memory cap)
KLEE: WARNING: killing 10794 states (over memory cap)
KLEE: WARNING: killing 10960 states (over memory cap)
KLEE: WARNING: killing 11034 states (over memory cap)
KLEE: WARNING: killing 11016 states (over memory cap)
KLEE: WARNING: killing 10901 states (over memory cap)
KLEE: WARNING: killing 10879 states (over memory cap)
KLEE: WARNING: killing 11044 states (over memory cap)
KLEE: WARNING: killing 11119 states (over memory cap)
KLEE: WARNING: killing 10647 states (over memory cap)
KLEE: WARNING: killing 10809 states (over memory cap)
KLEE: WARNING: killing 10611 states (over memory cap)
KLEE: WARNING: killing 10856 states (over memory cap)
