[DBG] Symbiotic dir: /home/jasku/formela/symbiotic/install[DBG] 'clang' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/clang'[DBG] 'opt' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/opt'[DBG] 'llvm-link' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-link'[DBG] 'llvm-nm' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-nm'[DBG] 'sbt-instr' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-instr'[DBG] 'sbt-slicer' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-slicer'[DBG] 'klee' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee'[DBG] Working directory: /home/jasku/formela/symbiotic/install/bin/symbiotic_files[DBG] PATH=/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin:/home/jasku/formela/symbiotic/install/bin:/usr/local/sbin:/usr/local/bin:/usr/bin:/home/jasku/dotfiles/scripts:/home/jasku/.cargo/bin:/home/jasku/go/bin:/home/jasku/bin:/home/jasku/.config/composer/vendor/bin:/home/jasku/.local/share/radare2/prefix/bin:/home/jasku/.gem/ruby/2.6.0/bin/:/home/jasku/.local/bin/:/usr/bin/site_perl:/usr/bin/vendor_perl:/usr/bin/core_perl:/opt/devkitpro/tools/bin:/home/jasku/dotfiles/scripts:/home/jasku/.cargo/bin:/home/jasku/go/bin:/home/jasku/bin:/home/jasku/.config/composer/vendor/bin:/home/jasku/.local/share/radare2/prefix/bin:/home/jasku/.gem/ruby/2.6.0/bin/:/home/jasku/.local/bin/[DBG] LD_LIBRARY_PATH=/home/jasku/formela/symbiotic/install/llvm-8.0.1/predator/lib:/home/jasku/formela/symbiotic/install/llvm-8.0.1/lib:/home/jasku/formela/symbiotic/install/lib[DBG] C_INCLUDE_DIR=/home/jasku/formela/symbiotic/install/include7.0.0-dev-llvm-8.0.1-symbiotic:2e2ceb47-dg:ccbc3536-sbt-slicer:85c8cb48-sbt-instrumentation:62c48199-klee:236d9920INFO: Looking for reachability of calls to reach_error[DBG] Running symbiotic-cc for klee|> clang -c -emit-llvm -D__inline= -Wno-unused-parameter -Wno-unknown-attributes -Wno-unused-label -Wno-unknown-pragmas -Wno-unused-command-line-argument -O0 -disable-llvm-passes -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o 43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.bc /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4209:12: warning: incompatible redeclaration of library function 'sprintf' [-Wincompatible-library-redeclaration][DBG] extern int sprintf(char * , char * , ...) ;[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4209:12: note: 'sprintf' is a builtin with type 'int (char *, const char *, ...)'[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4256:14: warning: incompatible redeclaration of library function 'memcpy' [-Wincompatible-library-redeclaration][DBG] extern void *memcpy(void * , void * , size_t ) ;[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4256:14: note: 'memcpy' is a builtin with type 'void *(void *, const void *, unsigned int)'[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4257:14: warning: incompatible redeclaration of library function 'memset' [-Wincompatible-library-redeclaration][DBG] extern void *memset(void * , int , size_t ) ;[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4257:14: note: 'memset' is a builtin with type 'void *(void *, int, unsigned int)'[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4310:27: warning: result of comparison of constant 18446744073709547520 with expression of type 'unsigned long' is always false [-Wtautological-constant-out-of-range-compare][DBG] __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;[DBG] ~~~~~~~~~~ ^ ~~~~~~~~~~~~~~~~~~~~[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4485:14: warning: incompatible redeclaration of library function 'malloc' [-Wincompatible-library-redeclaration][DBG] extern void *malloc(size_t size);[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4485:14: note: 'malloc' is a builtin with type 'void *(unsigned int)'[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4587:7: warning: ignoring return value of function declared with const attribute [-Wunused-value][DBG] __builtin_expect(__cil_tmp23, 0L);[DBG] ^~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:4877:3: warning: ignoring return value of function declared with const attribute [-Wunused-value][DBG] __builtin_expect(__cil_tmp20, 0L);[DBG] ^~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:19431:1: warning: return type of 'main' is not 'int' [-Wmain-return-type][DBG] void main(void)[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:19431:1: note: change return type to 'int'[DBG] void main(void)[DBG] ^~~~[DBG] int[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:19772:14: warning: incompatible redeclaration of library function 'calloc' [-Wincompatible-library-redeclaration][DBG] extern void *calloc(size_t, size_t) ;[DBG] ^[DBG] /home/jasku/formela/sv-benchmarks/c/ldv-linux-3.4-simple/43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:19772:14: note: 'calloc' is a builtin with type 'void *(unsigned int, unsigned int)'[DBG] 9 warnings generated.[DBG] Linking all input files into one file|> llvm-link -o code.bc 43_1a_cilled_ok_linux-43_1a-drivers--scsi--dpt_i2o.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.bc|> llvm-dis code.bc|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code.bc|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc -prepare|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc -remove-infinite-loops|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc|> opt -load LLVMsbt.so -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc -tti -targetlibinfo -tbaa -scoped-noalias -assumption-cache-tracker -verify -simplifycfg -domtree -sroa -early-cse -lower-expect -targetlibinfo -tti -tbaa -scoped-noalias -assumption-cache-tracker -forceattrs -inferattrs -ipsccp -globalopt -domtree -mem2reg -deadargelim -basicaa -aa -domtree -instcombine -simplifycfg -basiccg -globals-aa -prune-eh -inline-threshold=70 -inline -functionattrs -argpromotion -domtree -sroa -early-cse -lazy-value-info -jump-threading -correlated-propagation -simplifycfg -basicaa -aa -domtree -instcombine -tailcallelim -simplifycfg -reassociate -domtree -loops -loop-simplify -lcssa -basicaa -aa -licm -loop-unswitch -simplifycfg -basicaa -aa -domtree -instcombine -loops -scalar-evolution -loop-simplify -lcssa -indvars -aa -loop-idiom -loop-deletion -loop-unroll -basicaa -aa -mldst-motion -aa -memdep -gvn -basicaa -aa -memdep -memcpyopt -sccp -domtree -demanded-bits -bdce -basicaa -aa -instcombine -lazy-value-info -jump-threading -correlated-propagation -domtree -basicaa -aa -memdep -dse -loops -loop-simplify -lcssa -aa -licm -adce -simplifycfg -basicaa -aa -domtree -instcombine -barrier -basiccg -rpo-functionattrs -elim-avail-extern -basiccg -globals-aa -float2int -domtree -loops -loop-simplify -lcssa -branch-prob -block-freq -scalar-evolution -basicaa -aa -loop-accesses -demanded-bits -instcombine -scalar-evolution -aa -simplifycfg -basicaa -aa -domtree -instcombine -loops -loop-simplify -lcssa -scalar-evolution -loop-unroll -basicaa -aa -instcombine -loop-simplify -lcssa -aa -licm -scalar-evolution -alignment-from-assumptions -strip-dead-prototypes -globaldce -constmerge -verify -reg2mem -break-infinite-loops -remove-infinite-loops -mem2reg -break-crit-loops -lowerswitchRemoved infinite loop in arch_local_save_flagsRemoved infinite loop in adpt_scsi_to_i2oINFO: Optimizations time: 3.1919498443603516|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc|> opt -q -load LLVMsbt.so -check-module -detect-calls=pthread_create -o=/dev/null /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc -explicit-consdes|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bcINFO: Starting slicing[DBG] Slicing the code for the 1. time|> timeout 300 sbt-slicer -c reach_error -pta fi /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bcIntToPtr with constant: <badref> = inttoptr i32 -1 to i8*PTA: Inline assembly found, analysis may be unsound[RWG] WARNING: Inline assembler found[RWG] error: could not determine the called function in a call via pointer: adpt_fail_posted_scbs:: call void %36(%struct.scsi_cmnd* %37), !dbg !5403[RWG] error: could not determine the called function in a call via pointer: dma_free_attrs:: call void %34(%struct.device* %35, i32 %36, i8* %37, i64 %38, %struct.dma_attrs* %39), !dbg !5370[RWG] error: could not determine the called function in a call via pointer: dma_alloc_attrs:: %call11 = call i8* %25(%struct.device* %26, i32 %27, i64* %28, i32 %29, %struct.dma_attrs* %30), !dbg !5341[RWG] error: could not determine the called function in a call via pointer: adpt_i2o_to_scsi:: call void %453(%struct.scsi_cmnd* %454), !dbg !6655[llvm-slicer] CPU time of pointer analysis: 1.296470e-01 s[llvm-slicer] CPU time of reaching definitions analysis: 6.588100e-02 s[llvm-slicer] CPU time of control dependence analysis: 1.341300e-02 s[llvm-slicer] Finding dependent nodes took 0 sec 11 ms[llvm-slicer] Slicing dependence graph took 0 sec 35 ms[llvm-slicer] Sliced away 9174 from 29383 nodes in DG[llvm-slicer] saving sliced module to: /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.sliced|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.slicedINFO: Total slicing time: 3.799220085144043|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.sliced -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc -remove-infinite-loops|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc|> clang -c -emit-llvm -D__inline= -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_assume.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/verifier/klee/__VERIFIER_assume.bc[DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]|> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_assume.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bcLinked our definitions to these undefined functions: __VERIFIER_assume|> opt -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bc -tti -targetlibinfo -tbaa -scoped-noalias -assumption-cache-tracker -verify -simplifycfg -domtree -sroa -early-cse -lower-expect -targetlibinfo -tti -tbaa -scoped-noalias -assumption-cache-tracker -forceattrs -inferattrs -ipsccp -globalopt -domtree -mem2reg -deadargelim -basicaa -aa -domtree -instcombine -simplifycfg -basiccg -globals-aa -prune-eh -inline-threshold=70 -inline -functionattrs -argpromotion -domtree -sroa -early-cse -lazy-value-info -jump-threading -correlated-propagation -simplifycfg -basicaa -aa -domtree -instcombine -tailcallelim -simplifycfg -reassociate -domtree -loops -loop-simplify -lcssa -basicaa -aa -licm -loop-unswitch -simplifycfg -basicaa -aa -domtree -instcombine -loops -scalar-evolution -loop-simplify -lcssa -indvars -aa -loop-idiom -loop-deletion -loop-unroll -basicaa -aa -mldst-motion -aa -memdep -gvn -basicaa -aa -memdep -memcpyopt -sccp -domtree -demanded-bits -bdce -basicaa -aa -instcombine -lazy-value-info -jump-threading -correlated-propagation -domtree -basicaa -aa -memdep -dse -loops -loop-simplify -lcssa -aa -licm -adce -simplifycfg -basicaa -aa -domtree -instcombine -barrier -basiccg -rpo-functionattrs -elim-avail-extern -basiccg -globals-aa -float2int -domtree -loops -loop-simplify -lcssa -branch-prob -block-freq -scalar-evolution -basicaa -aa -loop-accesses -demanded-bits -instcombine -scalar-evolution -aa -simplifycfg -basicaa -aa -domtree -instcombine -loops -loop-simplify -lcssa -scalar-evolution -loop-unroll -basicaa -aa -instcombine -loop-simplify -lcssa -aa -licm -scalar-evolution -alignment-from-assumptions -strip-dead-prototypes -globaldce -constmerge -verifyINFO: Optimizations time: 2.0953357219696045|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt.bcINFO: After-slicing optimizations and transformations time: 0.5340344905853271|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr.bc -internalize-globals[DBG] Made global variable 'dma_ops' non-extern[DBG] Made global variable 'jiffies' non-extern[DBG] Made global variable 'current_task' non-extern[DBG] Made global variable 'x86_dma_fallback_dev' non-extern[DBG] Made global variable '__this_module' non-extern|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr.bc|> opt -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr.bc -O3INFO: Optimizations time: 2.7137928009033203|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt.bc|> clang -c -emit-llvm -D__inline= -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_make_nondet.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/verifier/klee/__VERIFIER_make_nondet.bc[DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]|> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_make_nondet.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt.bc|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt-ln.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt-ln.bcLinked our definitions to these undefined functions: __VERIFIER_make_nondetINFO: Starting verification|> /home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee -dump-states-on-halt=0 --output-stats=0 --use-call-paths=0 --optimize=false -silent-klee-assume=1 -istats-write-interval=60s -only-output-states-covering-new=1 -use-forked-solver=0 -max-time=0 -external-calls=pure -max-memory=8000 -error-fn=reach_error -exit-on-error-type=Assert -write-witness -output-source=false /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt-ln.bcKLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0"KLEE: Using Z3 solver backendKLEE: Allocating memory with 32-bits addressesb'KLEE: WARNING ONCE: function "readl" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm'b'KLEE: WARNING ONCE: function "get_current" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm'b'KLEE: WARNING ONCE: function "readb" has inline asm'b'KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm'b'KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm'b'KLEE: WARNING: undefined reference to function: adpt_info'b'KLEE: WARNING: undefined reference to function: adpt_slave_configure'b'KLEE: WARNING: undefined reference to function: noop_llseek'b'KLEE: WARNING: undefined reference to function: printk'b'KLEE: WARNING: undefined reference to function: sprintf' #0 0x000056464de99ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4) #1 0x000056464de9a0e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9) #2 0x000056464de97fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8) #3 0x000056464de9a84e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e) #4 0x00007f42c9cff0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0) #5 0x00007f42c97dcad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3) #6 0x000056464b9a7e62 klee::AddressSpace::copyOutConcretes(std::map<unsigned long const, unsigned long const, std::less<unsigned long const>, std::allocator<std::pair<unsigned long const, unsigned long const> > > const&, bool) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x81ae62) #7 0x000056464b95b36d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d) #8 0x000056464b966385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385) #9 0x000056464b8b2fe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)#10 0x00007f42c969f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)#11 0x000056464b93244e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)[DBG] The verifier return non-0 return statusINFO: Verification time: 1.2384181022644043[DBG] Tool result: ERRORKLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0"KLEE: Using Z3 solver backendKLEE: Allocating memory with 32-bits addressesKLEE: WARNING ONCE: function "readl" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asmKLEE: WARNING ONCE: function "get_current" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asmKLEE: WARNING ONCE: function "readb" has inline asmKLEE: WARNING ONCE: function "adpt_queue_lck" has inline asmKLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asmKLEE: WARNING: undefined reference to function: adpt_infoKLEE: WARNING: undefined reference to function: adpt_slave_configureKLEE: WARNING: undefined reference to function: noop_llseekKLEE: WARNING: undefined reference to function: printkKLEE: WARNING: undefined reference to function: sprintf #0 0x000056464de99ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4) #1 0x000056464de9a0e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9) #2 0x000056464de97fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8) #3 0x000056464de9a84e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e) #4 0x00007f42c9cff0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0) #5 0x00007f42c97dcad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3) #6 0x000056464b9a7e62 klee::AddressSpace::copyOutConcretes(std::map<unsigned long const, unsigned long const, std::less<unsigned long const>, std::allocator<std::pair<unsigned long const, unsigned long const> > > const&, bool) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x81ae62) #7 0x000056464b95b36d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d) #8 0x000056464b966385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385) #9 0x000056464b8b2fe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)#10 0x00007f42c969f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)#11 0x000056464b93244e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)INFO: Failed on the sliced code, trying on the unsliced code|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc -remove-infinite-loops|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc|> clang -c -emit-llvm -D__inline= -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_assume.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/verifier/klee/__VERIFIER_assume.bc[DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]|> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_assume.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bcLinked our definitions to these undefined functions: __VERIFIER_assume|> opt -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bc -tti -targetlibinfo -tbaa -scoped-noalias -assumption-cache-tracker -verify -simplifycfg -domtree -sroa -early-cse -lower-expect -targetlibinfo -tti -tbaa -scoped-noalias -assumption-cache-tracker -forceattrs -inferattrs -ipsccp -globalopt -domtree -mem2reg -deadargelim -basicaa -aa -domtree -instcombine -simplifycfg -basiccg -globals-aa -prune-eh -inline-threshold=70 -inline -functionattrs -argpromotion -domtree -sroa -early-cse -lazy-value-info -jump-threading -correlated-propagation -simplifycfg -basicaa -aa -domtree -instcombine -tailcallelim -simplifycfg -reassociate -domtree -loops -loop-simplify -lcssa -basicaa -aa -licm -loop-unswitch -simplifycfg -basicaa -aa -domtree -instcombine -loops -scalar-evolution -loop-simplify -lcssa -indvars -aa -loop-idiom -loop-deletion -loop-unroll -basicaa -aa -mldst-motion -aa -memdep -gvn -basicaa -aa -memdep -memcpyopt -sccp -domtree -demanded-bits -bdce -basicaa -aa -instcombine -lazy-value-info -jump-threading -correlated-propagation -domtree -basicaa -aa -memdep -dse -loops -loop-simplify -lcssa -aa -licm -adce -simplifycfg -basicaa -aa -domtree -instcombine -barrier -basiccg -rpo-functionattrs -elim-avail-extern -basiccg -globals-aa -float2int -domtree -loops -loop-simplify -lcssa -branch-prob -block-freq -scalar-evolution -basicaa -aa -loop-accesses -demanded-bits -instcombine -scalar-evolution -aa -simplifycfg -basicaa -aa -domtree -instcombine -loops -loop-simplify -lcssa -scalar-evolution -loop-unroll -basicaa -aa -instcombine -loop-simplify -lcssa -aa -licm -scalar-evolution -alignment-from-assumptions -strip-dead-prototypes -globaldce -constmerge -verifyINFO: Optimizations time: 3.073033094406128|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt.bcINFO: After-slicing optimizations and transformations time: 0.9150681495666504|> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr.bc -internalize-globals[DBG] Made global variable 'pv_irq_ops' non-extern[DBG] Made global variable 'dma_ops' non-extern[DBG] Made global variable 'jiffies' non-extern[DBG] Made global variable 'current_task' non-extern[DBG] Made global variable 'x86_dma_fallback_dev' non-extern[DBG] Made global variable '__this_module' non-extern|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr.bc|> opt -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr.bc -O3INFO: Optimizations time: 3.857717752456665|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt.bc|> clang -c -emit-llvm -D__inline= -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_make_nondet.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/verifier/klee/__VERIFIER_make_nondet.bc[DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]|> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_make_nondet.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt.bc|> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt-ln.bc|> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt-ln.bcLinked our definitions to these undefined functions: __VERIFIER_make_nondetINFO: Starting verification|> /home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee -dump-states-on-halt=0 --output-stats=0 --use-call-paths=0 --optimize=false -silent-klee-assume=1 -istats-write-interval=60s -only-output-states-covering-new=1 -use-forked-solver=0 -max-time=0 -external-calls=pure -max-memory=8000 -error-fn=reach_error -exit-on-error-type=Assert -write-witness -output-source=false /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt-ln.bcKLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-1"KLEE: Using Z3 solver backendKLEE: Allocating memory with 32-bits addressesb'KLEE: WARNING ONCE: function "adpt_isr" has inline asm'b'KLEE: WARNING ONCE: function "readl" has inline asm'b'KLEE: WARNING ONCE: function "writel" has inline asm'b'KLEE: WARNING ONCE: function "adpt_send_nop" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm'b'KLEE: WARNING ONCE: function "get_current" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_post_this" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_status_get" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_reset_hba" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_init_outbound_q" has inline asm'b'KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm'b'KLEE: WARNING ONCE: function "readb" has inline asm'b'KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm'b'KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm'b'KLEE: WARNING: undefined reference to function: noop_llseek'b'KLEE: WARNING: undefined reference to function: sprintf' #0 0x000055d5a1d62ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4) #1 0x000055d5a1d630e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9) #2 0x000055d5a1d60fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8) #3 0x000055d5a1d6384e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e) #4 0x00007fa87f99f0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0) #5 0x00007fa87f47cad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3) #6 0x000055d59f870e62 klee::AddressSpace::copyOutConcretes(std::map<unsigned long const, unsigned long const, std::less<unsigned long const>, std::allocator<std::pair<unsigned long const, unsigned long const> > > const&, bool) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x81ae62) #7 0x000055d59f82436d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d) #8 0x000055d59f82f385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385) #9 0x000055d59f77bfe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)#10 0x00007fa87f33f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)#11 0x000055d59f7fb44e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)[DBG] The verifier return non-0 return statusINFO: Verification time: 2.0022876262664795[DBG] Tool result: ERRORKLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-1"KLEE: Using Z3 solver backendKLEE: Allocating memory with 32-bits addressesKLEE: WARNING ONCE: function "adpt_isr" has inline asmKLEE: WARNING ONCE: function "readl" has inline asmKLEE: WARNING ONCE: function "writel" has inline asmKLEE: WARNING ONCE: function "adpt_send_nop" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asmKLEE: WARNING ONCE: function "get_current" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_post_this" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_status_get" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_reset_hba" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_init_outbound_q" has inline asmKLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asmKLEE: WARNING ONCE: function "readb" has inline asmKLEE: WARNING ONCE: function "adpt_queue_lck" has inline asmKLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asmKLEE: WARNING: undefined reference to function: noop_llseekKLEE: WARNING: undefined reference to function: sprintf #0 0x000055d5a1d62ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4) #1 0x000055d5a1d630e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9) #2 0x000055d5a1d60fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8) #3 0x000055d5a1d6384e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e) #4 0x00007fa87f99f0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0) #5 0x00007fa87f47cad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3) #6 0x000055d59f870e62 klee::AddressSpace::copyOutConcretes(std::map<unsigned long const, unsigned long const, std::less<unsigned long const>, std::allocator<std::pair<unsigned long const, unsigned long const> > > const&, bool) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x81ae62) #7 0x000055d59f82436d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d) #8 0x000055d59f82f385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385) #9 0x000055d59f77bfe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)#10 0x00007fa87f33f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)#11 0x000055d59f7fb44e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)INFO: Running on unsliced code time: 0.0005645751953125[DBG] ERRORGenerating correctness witness: /home/jasku/formela/symbiotic/install/bin/witness.graphmlFailure!RESULT: ERRORINFO: Total time elapsed: 55.98403978347778
Comments