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--input--serio--serio_raw.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.: 36 122 581 3078
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.20371389389
Defining function noop_llseek as symbolic
Removed calls to '_raw_spin_lock_irq' (function is undefined)
Removed calls to '_raw_spin_unlock_irq' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to 'warn_slowpath_null' (function is undefined)
Removed calls to '__list_add' (function is undefined)
Removed calls to 'list_del' (function is undefined)
Defining function fasync_helper as symbolic
Removed calls to 'put_device' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function mutex_lock_interruptible as symbolic
Defining function prepare_to_wait_event as symbolic
Removed calls to 'kill_fasync' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'dev_err' (function is undefined)
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to '_dev_info' (function is undefined)
Removed calls to 'serio_close' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Defining function misc_deregister as symbolic
Defining function snprintf as symbolic
Defining function get_device as symbolic
Defining function serio_open as symbolic
Defining function misc_register as symbolic
Defining function mutex_lock_killable as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'serio_unregister_driver' (function is undefined)
Defining function __serio_register_driver as symbolic
Defining function mutex_trylock 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.22371006012
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 75 115 409 1925
INFO: Starting verification
KLEE: WARNING ONCE: function "serio_raw_read" has inline asm
KLEE: WARNING ONCE: function "serio_raw_write" has inline asm
KLEE: WARNING ONCE: function "serio_raw_open" has inline asm
KLEE: WARNING ONCE: function "kref_put" has inline asm
KLEE: WARNING ONCE: function "serio_raw_connect" 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_ba19dbe2-ecf8-47e6-9664-71774af88458/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gHR5ju/linux-4.2-rc1.tar.xz-32_7a-drivers--input--serio--serio_raw.ko-entry_point_true-unreach-call.cil.out.c:3249: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 12457 states (over memory cap)
KLEE: WARNING: killing 13317 states (over memory cap)
KLEE: WARNING: killing 13703 states (over memory cap)
KLEE: WARNING: killing 13635 states (over memory cap)
KLEE: WARNING: killing 13221 states (over memory cap)
KLEE: WARNING: killing 13382 states (over memory cap)
KLEE: WARNING: killing 13656 states (over memory cap)
KLEE: WARNING: killing 13589 states (over memory cap)
KLEE: WARNING: killing 14204 states (over memory cap)
KLEE: WARNING: killing 14476 states (over memory cap)
KLEE: WARNING: killing 14304 states (over memory cap)
KLEE: WARNING: killing 14589 states (over memory cap)
KLEE: WARNING: killing 14756 states (over memory cap)
KLEE: WARNING: killing 14695 states (over memory cap)
KLEE: WARNING: killing 14864 states (over memory cap)
KLEE: WARNING: killing 14590 states (over memory cap)
KLEE: WARNING: killing 15081 states (over memory cap)
KLEE: WARNING: killing 14699 states (over memory cap)
KLEE: WARNING: killing 14875 states (over memory cap)
KLEE: WARNING: killing 14600 states (over memory cap)
KLEE: WARNING: killing 14975 states (over memory cap)
KLEE: WARNING: killing 14804 states (over memory cap)
KLEE: WARNING: killing 10708 states (over memory cap)
KLEE: WARNING: killing 15038 states (over memory cap)
KLEE: WARNING: killing 15203 states (over memory cap)
KLEE: WARNING: killing 15047 states (over memory cap)
KLEE: WARNING: killing 14885 states (over memory cap)
KLEE: WARNING: killing 14839 states (over memory cap)
KLEE: WARNING: killing 10505 states (over memory cap)
KLEE: WARNING: killing 14858 states (over memory cap)
KLEE: WARNING: killing 10548 states (over memory cap)
KLEE: WARNING: killing 14557 states (over memory cap)
KLEE: WARNING: killing 10380 states (over memory cap)
KLEE: WARNING: killing 14376 states (over memory cap)
KLEE: WARNING: killing 10529 states (over memory cap)
KLEE: WARNING: killing 10303 states (over memory cap)
KLEE: WARNING: killing 10281 states (over memory cap)
KLEE: WARNING: killing 14543 states (over memory cap)
KLEE: WARNING: killing 10529 states (over memory cap)
KLEE: WARNING: killing 10406 states (over memory cap)
KLEE: WARNING: killing 14538 states (over memory cap)
KLEE: WARNING: killing 10551 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10102 states (over memory cap)
KLEE: WARNING: killing 14398 states (over memory cap)
KLEE: WARNING: killing 10449 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 10594 states (over memory cap)
KLEE: WARNING: killing 10471 states (over memory cap)
KLEE: WARNING: killing 10151 states (over memory cap)
KLEE: WARNING: killing 14195 states (over memory cap)
KLEE: WARNING: killing 10794 states (over memory cap)
KLEE: WARNING: killing 10081 states (over memory cap)
KLEE: WARNING: killing 10458 states (over memory cap)
KLEE: WARNING: killing 9947 states (over memory cap)
KLEE: WARNING: killing 10024 states (over memory cap)
KLEE: WARNING: killing 10193 states (over memory cap)
KLEE: WARNING: killing 10078 states (over memory cap)
KLEE: WARNING: killing 10157 states (over memory cap)
KLEE: WARNING: killing 10430 states (over memory cap)
KLEE: WARNING: killing 9824 states (over memory cap)
KLEE: WARNING: killing 10291 states (over memory cap)
KLEE: WARNING: killing 10174 states (over memory cap)
KLEE: WARNING: killing 10350 states (over memory cap)
KLEE: WARNING: killing 10139 states (over memory cap)
KLEE: WARNING: killing 9923 states (over memory cap)
KLEE: WARNING: killing 9905 states (over memory cap)
KLEE: WARNING: killing 9884 states (over memory cap)
KLEE: WARNING: killing 9959 states (over memory cap)
KLEE: WARNING: killing 10130 states (over memory cap)
KLEE: WARNING: killing 10399 states (over memory cap)
KLEE: WARNING: killing 10288 states (over memory cap)
KLEE: WARNING: killing 9980 states (over memory cap)
KLEE: WARNING: killing 9773 states (over memory cap)
KLEE: WARNING: killing 10135 states (over memory cap)
KLEE: WARNING: killing 10115 states (over memory cap)
KLEE: WARNING: killing 10195 states (over memory cap)
KLEE: WARNING: killing 10178 states (over memory cap)
KLEE: WARNING: killing 10156 states (over memory cap)
KLEE: WARNING: killing 9762 states (over memory cap)
KLEE: WARNING: killing 10121 states (over memory cap)
KLEE: WARNING: killing 10103 states (over memory cap)
KLEE: WARNING: killing 9991 states (over memory cap)
KLEE: WARNING: killing 10161 states (over memory cap)
KLEE: WARNING: killing 10148 states (over memory cap)
KLEE: WARNING: killing 10127 states (over memory cap)
KLEE: WARNING: killing 10014 states (over memory cap)
KLEE: WARNING: killing 9811 states (over memory cap)
KLEE: WARNING: killing 9975 states (over memory cap)
KLEE: WARNING: killing 10328 states (over memory cap)
KLEE: WARNING: killing 10123 states (over memory cap)
KLEE: WARNING: killing 9835 states (over memory cap)
KLEE: WARNING: killing 10183 states (over memory cap)
KLEE: WARNING: killing 10167 states (over memory cap)
KLEE: WARNING: killing 9873 states (over memory cap)
KLEE: WARNING: killing 9675 states (over memory cap)
KLEE: WARNING: killing 10205 states (over memory cap)
KLEE: WARNING: killing 9913 states (over memory cap)
KLEE: WARNING: killing 10172 states (over memory cap)
KLEE: WARNING: killing 9792 states (over memory cap)
KLEE: WARNING: killing 10231 states (over memory cap)
KLEE: WARNING: killing 10305 states (over memory cap)
KLEE: WARNING: killing 10200 states (over memory cap)
KLEE: WARNING: killing 10094 states (over memory cap)
KLEE: WARNING: killing 9807 states (over memory cap)
KLEE: WARNING: killing 9882 states (over memory cap)
KLEE: WARNING: killing 10309 states (over memory cap)
