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--mousedev.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.: 50 163 921 5277
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.285446882248
Defining function noop_llseek as symbolic
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 '_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 '__copy_to_user_overflow' (function is undefined)
Removed calls to 'kill_fasync' (function is undefined)
Removed calls to '__wake_up' (function is undefined)
Removed calls to '__raw_spin_lock_init' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '__list_add_rcu' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function fasync_helper as symbolic
Removed calls to '__list_del_entry' (function is undefined)
Removed calls to 'synchronize_sched' (function is undefined)
Defining function nonseekable_open as symbolic
Defining function prepare_to_wait_event as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__list_add' (function is undefined)
Removed calls to 'put_device' (function is undefined)
Removed calls to 'device_del' (function is undefined)
Removed calls to 'input_free_minor' (function is undefined)
Removed calls to 'input_unregister_handle' (function is undefined)
Removed calls to 'cdev_del' (function is undefined)
Removed calls to 'input_close_device' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Removed calls to 'lockdep_init_map' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to 'device_initialize' (function is undefined)
Removed calls to 'cdev_init' (function is undefined)
Defining function get_device as symbolic
Defining function input_open_device as symbolic
Defining function mutex_lock_interruptible as symbolic
Defining function dev_set_name as symbolic
Defining function input_register_handle as symbolic
Defining function cdev_add as symbolic
Defining function device_add as symbolic
Defining function input_get_new_minor as symbolic
Defining function printk as symbolic
Removed calls to 'lock_acquire' (function is undefined)
Removed calls to 'lockdep_rcu_suspicious' (function is undefined)
Removed calls to 'lock_release' (function is undefined)
Defining function debug_lockdep_rcu_enabled as symbolic
Defining function rcu_is_watching as symbolic
Defining function __msecs_to_jiffies as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'input_unregister_handler' (function is undefined)
Defining function ldv_release_1 as symbolic
Defining function ldv_bind_1 as symbolic
Defining function input_register_handler as symbolic
Defining function misc_register as symbolic
Defining function misc_deregister 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.29803609848
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 94 141 584 3012
INFO: Starting verification
KLEE: WARNING ONCE: function "mousedev_write" has inline asm
KLEE: WARNING ONCE: function "mousedev_event" has inline asm
KLEE: WARNING ONCE: function "mousedev_notify_readers" has inline asm
KLEE: WARNING ONCE: function "mousedev_key_event" 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_91056833-e1f7-497a-a247-0cce1dfb1127/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-r31jmH/linux-4.2-rc1.tar.xz-32_7a-drivers--input--mousedev.ko-entry_point_false-unreach-call.cil.out.c:5124: 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 10696 states (over memory cap)
KLEE: WARNING: killing 12291 states (over memory cap)
KLEE: WARNING: killing 12959 states (over memory cap)
KLEE: WARNING: killing 13078 states (over memory cap)
KLEE: WARNING: killing 13105 states (over memory cap)
KLEE: WARNING: killing 9206 states (over memory cap)
KLEE: WARNING: killing 9268 states (over memory cap)
KLEE: WARNING: killing 9153 states (over memory cap)
KLEE: WARNING: killing 9122 states (over memory cap)
KLEE: WARNING: killing 9188 states (over memory cap)
KLEE: WARNING: killing 8983 states (over memory cap)
KLEE: WARNING: killing 9484 states (over memory cap)
KLEE: WARNING: killing 9372 states (over memory cap)
KLEE: WARNING: killing 9611 states (over memory cap)
KLEE: WARNING: killing 9411 states (over memory cap)
KLEE: WARNING: killing 9210 states (over memory cap)
KLEE: WARNING: killing 9361 states (over memory cap)
KLEE: WARNING: killing 9431 states (over memory cap)
KLEE: WARNING: killing 9488 states (over memory cap)
KLEE: WARNING: killing 9379 states (over memory cap)
KLEE: WARNING: killing 9352 states (over memory cap)
KLEE: WARNING: killing 9327 states (over memory cap)
KLEE: WARNING: killing 9217 states (over memory cap)
KLEE: WARNING: killing 9189 states (over memory cap)
KLEE: WARNING: killing 9334 states (over memory cap)
KLEE: WARNING: killing 9308 states (over memory cap)
KLEE: WARNING: killing 9369 states (over memory cap)
KLEE: WARNING: killing 9516 states (over memory cap)
KLEE: WARNING: killing 9322 states (over memory cap)
KLEE: WARNING: killing 9386 states (over memory cap)
KLEE: WARNING: killing 9616 states (over memory cap)
KLEE: WARNING: killing 9591 states (over memory cap)
KLEE: WARNING: killing 9399 states (over memory cap)
KLEE: WARNING: killing 9377 states (over memory cap)
KLEE: WARNING: killing 9519 states (over memory cap)
KLEE: WARNING: killing 9416 states (over memory cap)
KLEE: WARNING: killing 9226 states (over memory cap)
KLEE: WARNING: killing 9201 states (over memory cap)
KLEE: WARNING: killing 9595 states (over memory cap)
KLEE: WARNING: killing 9081 states (over memory cap)
KLEE: WARNING: killing 9387 states (over memory cap)
KLEE: WARNING: killing 9364 states (over memory cap)
KLEE: WARNING: killing 9588 states (over memory cap)
KLEE: WARNING: killing 9078 states (over memory cap)
KLEE: WARNING: killing 9142 states (over memory cap)
KLEE: WARNING: killing 9280 states (over memory cap)
KLEE: WARNING: killing 9504 states (over memory cap)
KLEE: WARNING: killing 9563 states (over memory cap)
KLEE: WARNING: killing 9464 states (over memory cap)
KLEE: WARNING: killing 9358 states (over memory cap)
KLEE: WARNING: killing 9423 states (over memory cap)
KLEE: WARNING: killing 9407 states (over memory cap)
KLEE: WARNING: killing 9146 states (over memory cap)
KLEE: WARNING: killing 9042 states (over memory cap)
KLEE: WARNING: killing 9106 states (over memory cap)
KLEE: WARNING: killing 9406 states (over memory cap)
KLEE: WARNING: killing 9304 states (over memory cap)
KLEE: WARNING: killing 9288 states (over memory cap)
KLEE: WARNING: killing 9427 states (over memory cap)
KLEE: WARNING: killing 9566 states (over memory cap)
KLEE: WARNING: killing 9312 states (over memory cap)
KLEE: WARNING: killing 9452 states (over memory cap)
KLEE: WARNING: killing 9039 states (over memory cap)
KLEE: WARNING: killing 9100 states (over memory cap)
KLEE: WARNING: killing 9474 states (over memory cap)
KLEE: WARNING: killing 9144 states (over memory cap)
KLEE: WARNING: killing 9358 states (over memory cap)
KLEE: WARNING: killing 9108 states (over memory cap)
KLEE: WARNING: killing 9327 states (over memory cap)
KLEE: WARNING: killing 9074 states (over memory cap)
KLEE: WARNING: killing 9129 states (over memory cap)
KLEE: WARNING: killing 9111 states (over memory cap)
KLEE: WARNING: killing 9173 states (over memory cap)
KLEE: WARNING: killing 9387 states (over memory cap)
KLEE: WARNING: killing 9295 states (over memory cap)
KLEE: WARNING: killing 9282 states (over memory cap)
KLEE: WARNING: killing 9189 states (over memory cap)
KLEE: WARNING: killing 9094 states (over memory cap)
KLEE: WARNING: killing 8927 states (over memory cap)
KLEE: WARNING: killing 9294 states (over memory cap)
KLEE: WARNING: killing 9122 states (over memory cap)
KLEE: WARNING: killing 9336 states (over memory cap)
KLEE: WARNING: killing 9088 states (over memory cap)
KLEE: WARNING: killing 9375 states (over memory cap)
KLEE: WARNING: killing 9283 states (over memory cap)
KLEE: WARNING: killing 8812 states (over memory cap)
KLEE: WARNING: killing 9021 states (over memory cap)
KLEE: WARNING: killing 9081 states (over memory cap)
KLEE: WARNING: killing 9369 states (over memory cap)
KLEE: WARNING: killing 9282 states (over memory cap)
KLEE: WARNING: killing 9115 states (over memory cap)
KLEE: WARNING: killing 9473 states (over memory cap)
KLEE: WARNING: killing 9231 states (over memory cap)
KLEE: WARNING: killing 9140 states (over memory cap)
KLEE: WARNING: killing 9048 states (over memory cap)
KLEE: WARNING: killing 9182 states (over memory cap)
KLEE: WARNING: killing 8949 states (over memory cap)
KLEE: WARNING: killing 9077 states (over memory cap)
KLEE: WARNING: killing 9212 states (over memory cap)
KLEE: WARNING: killing 9273 states (over memory cap)
KLEE: WARNING: killing 9334 states (over memory cap)
KLEE: WARNING: killing 9248 states (over memory cap)
KLEE: WARNING: killing 9016 states (over memory cap)
KLEE: WARNING: killing 9442 states (over memory cap)
KLEE: WARNING: killing 9128 states (over memory cap)
KLEE: WARNING: killing 9040 states (over memory cap)
KLEE: WARNING: killing 9101 states (over memory cap)
KLEE: WARNING: killing 9159 states (over memory cap)
KLEE: WARNING: killing 9441 states (over memory cap)
KLEE: WARNING: killing 8917 states (over memory cap)
KLEE: WARNING: killing 9191 states (over memory cap)
KLEE: WARNING: killing 9108 states (over memory cap)
KLEE: WARNING: killing 8945 states (over memory cap)
KLEE: WARNING: killing 8784 states (over memory cap)
