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-08_1a-drivers--watchdog--pc87413_wdt.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.: 38 57 253 1431
Removed infinite loop in ldv_stop
Removed infinite loop in ldv_module_put_and_exit
INFO: Compilation, preparation and instrumentation time: 0.122210979462
Defining function no_llseek as symbolic
Removed calls to '__might_fault' (function is undefined)
Removed calls to '_raw_spin_lock' (function is undefined)
Removed calls to '_raw_spin_unlock' (function is undefined)
Defining function printk as symbolic
Defining function _copy_to_user as symbolic
Removed calls to 'ldv_initialize' (function is undefined)
Removed calls to '__release_region' (function is undefined)
Defining function __request_region as symbolic
Defining function register_reboot_notifier as symbolic
Defining function unregister_reboot_notifier as symbolic
Defining function misc_deregister as symbolic
Defining function misc_register as symbolic
Linked our definitions to these undefined functions:
  __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.178045034409
INFO: Before verification stats: Globals/Functions/Blocks/Instr.: 68 50 140 1082
INFO: Starting verification
KLEE: WARNING ONCE: function "pc87413_ioctl" has inline asm
KLEE: WARNING ONCE: function "pc87413_open" has inline asm
KLEE: WARNING ONCE: function "pc87413_release" has inline asm
KLEE: WARNING ONCE: function "pc87413_refresh" has inline asm
KLEE: WARNING ONCE: function "pc87413_disable" has inline asm
KLEE: WARNING ONCE: function "pc87413_enable" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_3e805f0c-fc12-4663-88fd-8a3edf54c8b5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-nI8REb/linux-4.2-rc1.tar.xz-08_1a-drivers--watchdog--pc87413_wdt.ko-entry_point_false-unreach-call.cil.out.c:3246: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15110 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12884 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 13040 states (over memory cap)
KLEE: WARNING: killing 13448 states (over memory cap)
KLEE: WARNING: killing 13982 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14870 states (over memory cap)
KLEE: WARNING: killing 11595 states (over memory cap)
KLEE: WARNING: killing 14437 states (over memory cap)
KLEE: WARNING: killing 14963 states (over memory cap)
KLEE: WARNING: killing 11597 states (over memory cap)
KLEE: WARNING: killing 11451 states (over memory cap)
KLEE: WARNING: killing 11534 states (over memory cap)
KLEE: WARNING: killing 11389 states (over memory cap)
KLEE: WARNING: killing 11587 states (over memory cap)
KLEE: WARNING: killing 11669 states (over memory cap)
KLEE: WARNING: killing 12090 states (over memory cap)
KLEE: WARNING: killing 11830 states (over memory cap)
KLEE: WARNING: killing 12364 states (over memory cap)
KLEE: WARNING: killing 12333 states (over memory cap)
KLEE: WARNING: killing 12308 states (over memory cap)
KLEE: WARNING: killing 12612 states (over memory cap)
KLEE: WARNING: killing 12359 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12513 states (over memory cap)
KLEE: WARNING: killing 12817 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 12965 states (over memory cap)
KLEE: WARNING: killing 12707 states (over memory cap)
KLEE: WARNING: killing 13109 states (over memory cap)
KLEE: WARNING: killing 13183 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13006 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 13365 states (over memory cap)
KLEE: WARNING: killing 13328 states (over memory cap)
KLEE: WARNING: killing 13837 states (over memory cap)
KLEE: WARNING: killing 13480 states (over memory cap)
KLEE: WARNING: killing 13760 states (over memory cap)
KLEE: WARNING: killing 13509 states (over memory cap)
KLEE: WARNING: killing 13577 states (over memory cap)
KLEE: WARNING: killing 13745 states (over memory cap)
KLEE: WARNING: killing 13708 states (over memory cap)
KLEE: WARNING: killing 13456 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13698 states (over memory cap)
KLEE: WARNING: killing 14080 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 14117 states (over memory cap)
KLEE: WARNING: killing 13858 states (over memory cap)
KLEE: WARNING: killing 13926 states (over memory cap)
KLEE: WARNING: killing 13880 states (over memory cap)
KLEE: WARNING: killing 14161 states (over memory cap)
KLEE: WARNING: killing 14018 states (over memory cap)
KLEE: WARNING: killing 14081 states (over memory cap)
KLEE: WARNING: killing 10184 states (over memory cap)
KLEE: WARNING: killing 13506 states (over memory cap)
KLEE: WARNING: killing 14073 states (over memory cap)
KLEE: WARNING: killing 13935 states (over memory cap)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 10149 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 10002 states (over memory cap)
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: WARNING: killing 13827 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-nI8REb/klee-out-0"
KLEE: Using STP solver backend
KLEE: WARNING ONCE: function "pc87413_ioctl" has inline asm
KLEE: WARNING ONCE: function "pc87413_open" has inline asm
KLEE: WARNING ONCE: function "pc87413_release" has inline asm
KLEE: WARNING ONCE: function "pc87413_refresh" has inline asm
KLEE: WARNING ONCE: function "pc87413_disable" has inline asm
KLEE: WARNING ONCE: function "pc87413_enable" has inline asm
KLEE: WARNING ONCE: function "main" has inline asm
KLEE: ERROR: /tmp/vcloud-vcloud-master/worker/working_dir_3e805f0c-fc12-4663-88fd-8a3edf54c8b5/symbiotic/lib/verifier/__VERIFIER_exit.c:6: abort failure
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
KLEE: ERROR: /tmp/symbiotic-nI8REb/linux-4.2-rc1.tar.xz-08_1a-drivers--watchdog--pc87413_wdt.ko-entry_point_false-unreach-call.cil.out.c:3246: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location
KLEE: WARNING ONCE: skipping fork (memory cap exceeded)
KLEE: WARNING: killing 15110 states (over memory cap)
KLEE: WARNING: killing 13525 states (over memory cap)
KLEE: WARNING: killing 12812 states (over memory cap)
KLEE: WARNING: killing 12723 states (over memory cap)
KLEE: WARNING: killing 12884 states (over memory cap)
KLEE: WARNING: killing 12939 states (over memory cap)
KLEE: WARNING: killing 13224 states (over memory cap)
KLEE: WARNING: killing 13040 states (over memory cap)
KLEE: WARNING: killing 13448 states (over memory cap)
KLEE: WARNING: killing 13982 states (over memory cap)
KLEE: WARNING: killing 14168 states (over memory cap)
KLEE: WARNING: killing 14227 states (over memory cap)
KLEE: WARNING: killing 14870 states (over memory cap)
KLEE: WARNING: killing 11595 states (over memory cap)
KLEE: WARNING: killing 14437 states (over memory cap)
KLEE: WARNING: killing 14963 states (over memory cap)
KLEE: WARNING: killing 11597 states (over memory cap)
KLEE: WARNING: killing 11451 states (over memory cap)
KLEE: WARNING: killing 11534 states (over memory cap)
KLEE: WARNING: killing 11389 states (over memory cap)
KLEE: WARNING: killing 11587 states (over memory cap)
KLEE: WARNING: killing 11669 states (over memory cap)
KLEE: WARNING: killing 12090 states (over memory cap)
KLEE: WARNING: killing 11830 states (over memory cap)
KLEE: WARNING: killing 12364 states (over memory cap)
KLEE: WARNING: killing 12333 states (over memory cap)
KLEE: WARNING: killing 12308 states (over memory cap)
KLEE: WARNING: killing 12612 states (over memory cap)
KLEE: WARNING: killing 12359 states (over memory cap)
KLEE: WARNING: killing 12544 states (over memory cap)
KLEE: WARNING: killing 12513 states (over memory cap)
KLEE: WARNING: killing 12817 states (over memory cap)
KLEE: WARNING: killing 12780 states (over memory cap)
KLEE: WARNING: killing 12965 states (over memory cap)
KLEE: WARNING: killing 12707 states (over memory cap)
KLEE: WARNING: killing 13109 states (over memory cap)
KLEE: WARNING: killing 13183 states (over memory cap)
KLEE: WARNING: killing 13473 states (over memory cap)
KLEE: WARNING: killing 13006 states (over memory cap)
KLEE: WARNING: killing 13398 states (over memory cap)
KLEE: WARNING: killing 13365 states (over memory cap)
KLEE: WARNING: killing 13328 states (over memory cap)
KLEE: WARNING: killing 13837 states (over memory cap)
KLEE: WARNING: killing 13480 states (over memory cap)
KLEE: WARNING: killing 13760 states (over memory cap)
KLEE: WARNING: killing 13509 states (over memory cap)
KLEE: WARNING: killing 13577 states (over memory cap)
KLEE: WARNING: killing 13745 states (over memory cap)
KLEE: WARNING: killing 13708 states (over memory cap)
KLEE: WARNING: killing 13456 states (over memory cap)
KLEE: WARNING: killing 13737 states (over memory cap)
KLEE: WARNING: killing 13698 states (over memory cap)
KLEE: WARNING: killing 14080 states (over memory cap)
KLEE: WARNING: killing 14258 states (over memory cap)
KLEE: WARNING: killing 14117 states (over memory cap)
KLEE: WARNING: killing 13858 states (over memory cap)
KLEE: WARNING: killing 13926 states (over memory cap)
KLEE: WARNING: killing 13880 states (over memory cap)
KLEE: WARNING: killing 14161 states (over memory cap)
KLEE: WARNING: killing 14018 states (over memory cap)
KLEE: WARNING: killing 14081 states (over memory cap)
KLEE: WARNING: killing 10184 states (over memory cap)
KLEE: WARNING: killing 13506 states (over memory cap)
KLEE: WARNING: killing 14073 states (over memory cap)
KLEE: WARNING: killing 13935 states (over memory cap)
KLEE: WARNING: killing 14002 states (over memory cap)
KLEE: WARNING: killing 10149 states (over memory cap)
KLEE: WARNING: killing 13531 states (over memory cap)
KLEE: WARNING: killing 10002 states (over memory cap)
KLEE: WARNING: killing 13374 states (over memory cap)
KLEE: WARNING: killing 13827 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 0x00007fc84914d390
4  libc.so.6       0x00007fc848506428 gsignal + 56
5  libc.so.6       0x00007fc84850802a abort + 362
6  libc.so.6       0x00007fc8484febd7
7  libc.so.6       0x00007fc8484fec82
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       0x00007fc8484f1830 __libc_start_main + 240
16 klee            0x00000000005bed49 _start + 41
Running the verifier failed
RESULT: unknown
INFO: Total time elapsed: 790.011579037
