bin/symbiotic --witness witness.graphml --no-slice --no-prepare --prp=../sv-benchmarks/c/Systems_DeviceDriversLinux64_ReachSafety.prp ../sv-benchmarks/c/ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--input--gameport--ns558.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.: 24 38 209 1175
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.108359098434
Defining function printk as symbolic
Defining function __request_region as symbolic
Defining function pnp_get_resource as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'gameport_unregister_port' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Removed calls to 'pnp_unregister_driver' (function is undefined)
Removed calls to 'msleep' (function is undefined)
Removed calls to 'ldv_check_final_state' (function is undefined)
Defining function ldv_release_1 as symbolic
Defining function pnp_register_driver as symbolic
Defining function kmem_cache_alloc as symbolic
Defining function ldv_some_page as symbolic
Linked our definitions to these undefined functions:
  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.154741048813
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 61 34 122 593
INFO: Starting verification
KLEE: WARNING ONCE: function "main" 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_19b018dc-19e6-4e7f-84b9-5cdd728b9dab/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-xvNNWo/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--input--gameport--ns558.ko-entry_point_true-unreach-call.cil.out.c:1461: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_19b018dc-19e6-4e7f-84b9-5cdd728b9dab/symbiotic/lib/kernel/kfree.c:5: memory error: invalid pointer: free
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 11006 states (over memory cap)
KLEE: WARNING: killing 11119 states (over memory cap)
KLEE: WARNING: killing 10735 states (over memory cap)
KLEE: WARNING: killing 10763 states (over memory cap)
KLEE: WARNING: killing 10792 states (over memory cap)
KLEE: WARNING: killing 11220 states (over memory cap)
KLEE: WARNING: killing 11449 states (over memory cap)
KLEE: WARNING: killing 11388 states (over memory cap)
KLEE: WARNING: killing 11322 states (over memory cap)
KLEE: WARNING: killing 11264 states (over memory cap)
KLEE: WARNING: killing 11397 states (over memory cap)
KLEE: WARNING: killing 11343 states (over memory cap)
KLEE: WARNING: killing 11087 states (over memory cap)
KLEE: WARNING: killing 10749 states (over memory cap)
KLEE: WARNING: killing 10979 states (over memory cap)
KLEE: WARNING: killing 11012 states (over memory cap)
KLEE: WARNING: killing 11146 states (over memory cap)
KLEE: WARNING: killing 11096 states (over memory cap)
KLEE: WARNING: killing 10679 states (over memory cap)
KLEE: WARNING: killing 10904 states (over memory cap)
KLEE: WARNING: killing 10765 states (over memory cap)
KLEE: WARNING: killing 10808 states (over memory cap)
KLEE: WARNING: killing 11124 states (over memory cap)
KLEE: WARNING: killing 11169 states (over memory cap)
KLEE: WARNING: killing 11031 states (over memory cap)
KLEE: WARNING: killing 10897 states (over memory cap)
KLEE: WARNING: killing 10940 states (over memory cap)
KLEE: WARNING: killing 10634 states (over memory cap)
KLEE: WARNING: killing 11031 states (over memory cap)
KLEE: WARNING: killing 10900 states (over memory cap)
KLEE: WARNING: killing 10859 states (over memory cap)
KLEE: WARNING: killing 10721 states (over memory cap)
KLEE: WARNING: killing 10855 states (over memory cap)
KLEE: WARNING: killing 8658 states (over memory cap)
KLEE: WARNING: killing 10525 states (over memory cap)
KLEE: WARNING: killing 8598 states (over memory cap)
KLEE: WARNING: killing 10629 states (over memory cap)
KLEE: WARNING: killing 8718 states (over memory cap)
KLEE: WARNING: killing 10388 states (over memory cap)
KLEE: WARNING: killing 10686 states (over memory cap)
KLEE: WARNING: killing 8621 states (over memory cap)
KLEE: WARNING: killing 10363 states (over memory cap)
KLEE: WARNING: killing 8399 states (over memory cap)
KLEE: WARNING: killing 10466 states (over memory cap)
