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--char--lp.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.: 60 140 897 4599
Removed infinite loop in ldv_stop
INFO: Compilation, preparation and instrumentation time: 0.326809167862
Removed calls to 'parport_release' (function is undefined)
Defining function parport_claim as symbolic
Defining function parport_set_timeout as symbolic
Defining function parport_negotiate as symbolic
Defining function parport_write as symbolic
Defining function unregister_console as symbolic
Defining function printk as symbolic
Removed calls to 'register_console' (function is undefined)
Defining function parport_register_device as symbolic
Defining function device_create as symbolic
Defining function parport_claim_or_block as symbolic
Defining function noop_llseek as symbolic
Removed calls to 'prepare_to_wait' (function is undefined)
Removed calls to 'finish_wait' (function is undefined)
Removed calls to '___might_sleep' (function is undefined)
Removed calls to 'schedule' (function is undefined)
Removed calls to 'mutex_lock' (function is undefined)
Removed calls to 'mutex_unlock' (function is undefined)
Defining function compat_get_timeval as symbolic
Removed calls to '__const_udelay' (function is undefined)
Removed calls to '__might_fault' (function is undefined)
Removed calls to '__copy_to_user_overflow' (function is undefined)
Defining function mutex_lock_interruptible as symbolic
Defining function _copy_to_user as symbolic
Removed calls to '__copy_from_user_overflow' (function is undefined)
Defining function _copy_from_user as symbolic
Defining function autoremove_wake_function as symbolic
Defining function schedule_timeout as symbolic
Defining function parport_read as symbolic
Defining function _cond_resched as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to 'parport_unregister_driver' (function is undefined)
Removed calls to '__unregister_chrdev' (function is undefined)
Removed calls to 'parport_unregister_device' (function is undefined)
Removed calls to 'device_destroy' (function is undefined)
Removed calls to 'class_destroy' (function is undefined)
Removed calls to '__init_waitqueue_head' (function is undefined)
Removed calls to '__mutex_init' (function is undefined)
Defining function ldv_release_1 as symbolic
Defining function ldv_open_1 as symbolic
Defining function ldv_close_1 as symbolic
Defining function ldv_probe_1 as symbolic
Defining function ldv_release_2 as symbolic
Defining function ldv_probe_2 as symbolic
Defining function __class_create as symbolic
Defining function __parport_register_driver as symbolic
Defining function __register_chrdev as symbolic
Defining function mutex_trylock as symbolic
Linked our definitions to these undefined functions:
  memchr
  strncmp
  __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.338928937912
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 98 152 655 2992
INFO: Starting verification
KLEE: WARNING ONCE: function "lp_preempt" has inline asm
KLEE: WARNING ONCE: function "lp_read" has inline asm
KLEE: WARNING ONCE: function "lp_write" has inline asm
KLEE: WARNING ONCE: function "lp_open" has inline asm
KLEE: WARNING ONCE: function "lp_claim_parport_or_block" has inline asm
KLEE: WARNING ONCE: function "lp_release_parport" has inline asm
KLEE: WARNING ONCE: function "lp_wait_ready" has inline asm
KLEE: WARNING ONCE: function "lp_error" 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_57ff2320-60f9-4f11-887e-ff9f3b07403d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gJwmDN/linux-4.2-rc1.tar.xz-32_7a-drivers--char--lp.ko-entry_point_true-unreach-call.cil.out.c:3698: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gJwmDN/linux-4.2-rc1.tar.xz-32_7a-drivers--char--lp.ko-entry_point_true-unreach-call.cil.out.c:4625: 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 11431 states (over memory cap)
KLEE: WARNING: killing 12468 states (over memory cap)
KLEE: WARNING: killing 12716 states (over memory cap)
KLEE: WARNING: killing 12667 states (over memory cap)
KLEE: WARNING: killing 12329 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 12533 states (over memory cap)
KLEE: WARNING: killing 13076 states (over memory cap)
KLEE: WARNING: killing 12941 states (over memory cap)
KLEE: WARNING: killing 13378 states (over memory cap)
KLEE: WARNING: killing 13530 states (over memory cap)
KLEE: WARNING: killing 13298 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13510 states (over memory cap)
KLEE: WARNING: killing 13761 states (over memory cap)
KLEE: WARNING: killing 13917 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13717 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13986 states (over memory cap)
KLEE: WARNING: killing 14132 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 13893 states (over memory cap)
KLEE: WARNING: killing 13946 states (over memory cap)
KLEE: WARNING: killing 13816 states (over memory cap)
KLEE: WARNING: killing 14050 states (over memory cap)
KLEE: WARNING: killing 14023 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 14045 states (over memory cap)
KLEE: WARNING: killing 14202 states (over memory cap)
KLEE: WARNING: killing 14075 states (over memory cap)
KLEE: WARNING: killing 14221 states (over memory cap)
KLEE: WARNING: killing 13920 states (over memory cap)
KLEE: WARNING: killing 14157 states (over memory cap)
KLEE: WARNING: killing 13947 states (over memory cap)
KLEE: WARNING: killing 14184 states (over memory cap)
KLEE: WARNING: killing 14053 states (over memory cap)
KLEE: WARNING: killing 14292 states (over memory cap)
KLEE: WARNING: killing 13806 states (over memory cap)
KLEE: WARNING: killing 14214 states (over memory cap)
KLEE: WARNING: killing 14715 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 14129 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
KLEE: output directory is "/tmp/symbiotic-gJwmDN/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "lp_preempt" has inline asm
KLEE: WARNING ONCE: function "lp_read" has inline asm
KLEE: WARNING ONCE: function "lp_write" has inline asm
KLEE: WARNING ONCE: function "lp_open" has inline asm
KLEE: WARNING ONCE: function "lp_claim_parport_or_block" has inline asm
KLEE: WARNING ONCE: function "lp_release_parport" has inline asm
KLEE: WARNING ONCE: function "lp_wait_ready" has inline asm
KLEE: WARNING ONCE: function "lp_error" 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_57ff2320-60f9-4f11-887e-ff9f3b07403d/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gJwmDN/linux-4.2-rc1.tar.xz-32_7a-drivers--char--lp.ko-entry_point_true-unreach-call.cil.out.c:3698: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: /tmp/symbiotic-gJwmDN/linux-4.2-rc1.tar.xz-32_7a-drivers--char--lp.ko-entry_point_true-unreach-call.cil.out.c:4625: 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 11431 states (over memory cap)
KLEE: WARNING: killing 12468 states (over memory cap)
KLEE: WARNING: killing 12716 states (over memory cap)
KLEE: WARNING: killing 12667 states (over memory cap)
KLEE: WARNING: killing 12329 states (over memory cap)
KLEE: WARNING: killing 12673 states (over memory cap)
KLEE: WARNING: killing 12533 states (over memory cap)
KLEE: WARNING: killing 13076 states (over memory cap)
KLEE: WARNING: killing 12941 states (over memory cap)
KLEE: WARNING: killing 13378 states (over memory cap)
KLEE: WARNING: killing 13530 states (over memory cap)
KLEE: WARNING: killing 13298 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13510 states (over memory cap)
KLEE: WARNING: killing 13761 states (over memory cap)
KLEE: WARNING: killing 13917 states (over memory cap)
KLEE: WARNING: killing 14068 states (over memory cap)
KLEE: WARNING: killing 13844 states (over memory cap)
KLEE: WARNING: killing 13717 states (over memory cap)
KLEE: WARNING: killing 13773 states (over memory cap)
KLEE: WARNING: killing 13645 states (over memory cap)
KLEE: WARNING: killing 13986 states (over memory cap)
KLEE: WARNING: killing 14132 states (over memory cap)
KLEE: WARNING: killing 14287 states (over memory cap)
KLEE: WARNING: killing 13687 states (over memory cap)
KLEE: WARNING: killing 13561 states (over memory cap)
KLEE: WARNING: killing 13893 states (over memory cap)
KLEE: WARNING: killing 13946 states (over memory cap)
KLEE: WARNING: killing 13816 states (over memory cap)
KLEE: WARNING: killing 14050 states (over memory cap)
KLEE: WARNING: killing 14023 states (over memory cap)
KLEE: WARNING: killing 14171 states (over memory cap)
KLEE: WARNING: killing 14045 states (over memory cap)
KLEE: WARNING: killing 14202 states (over memory cap)
KLEE: WARNING: killing 14075 states (over memory cap)
KLEE: WARNING: killing 14221 states (over memory cap)
KLEE: WARNING: killing 13920 states (over memory cap)
KLEE: WARNING: killing 14157 states (over memory cap)
KLEE: WARNING: killing 13947 states (over memory cap)
KLEE: WARNING: killing 14184 states (over memory cap)
KLEE: WARNING: killing 14053 states (over memory cap)
KLEE: WARNING: killing 14292 states (over memory cap)
KLEE: WARNING: killing 13806 states (over memory cap)
KLEE: WARNING: killing 14214 states (over memory cap)
KLEE: WARNING: killing 14715 states (over memory cap)
KLEE: WARNING: killing 14420 states (over memory cap)
KLEE: WARNING: killing 14129 states (over memory cap)
klee: /var/xchalup4/symbiotic/klee/include/klee/Internal/ADT/DiscretePDF.inc:116: void klee::DiscretePDF<T>::remove(T) [with T = klee::ExecutionState*]: Assertion `0 && "remove: argument(item) not in tree"' failed.
0  klee            0x00000000012fcca8 llvm::sys::PrintStackTrace(llvm::raw_ostream&) + 56
1  klee            0x00000000012fac7e llvm::sys::RunSignalHandlers() + 62
2  klee            0x00000000012fadcc
3  libpthread.so.0 0x00007f0fd35e4390
4  libc.so.6       0x00007f0fd299d428 gsignal + 56
5  libc.so.6       0x00007f0fd299f02a abort + 362
6  libc.so.6       0x00007f0fd2995bd7
7  libc.so.6       0x00007f0fd2995c82
8  klee            0x000000000061be59 klee::DiscretePDF<klee::ExecutionState*>::remove(klee::ExecutionState*) + 73
9  klee            0x00000000006195f1 klee::WeightedRandomSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 241
10 klee            0x0000000000617416 klee::InterleavedSearcher::update(klee::ExecutionState*, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&, std::vector<klee::ExecutionState*, std::allocator<klee::ExecutionState*> > const&) + 54
11 klee            0x00000000005cecfe klee::Executor::updateStates(klee::ExecutionState*) + 46
12 klee            0x00000000005da8eb klee::Executor::run(klee::ExecutionState&) + 2155
13 klee            0x00000000005daeef klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1391
14 klee            0x0000000000593c63 main + 8867
15 libc.so.6       0x00007f0fd2988830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 373.737787008
