API tools faq
paste
tomsik68

symbiotic --prp unreach-call 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

tomsik68
Nov 23rd, 2020
350
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 34.58 KB | None | 0 0
raw download clone embed print report
  1. [DBG] Symbiotic dir: /home/jasku/formela/symbiotic/install
  2. [DBG] 'clang' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/clang'
  3. [DBG] 'opt' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/opt'
  4. [DBG] 'llvm-link' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-link'
  5. [DBG] 'llvm-nm' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-nm'
  6. [DBG] 'sbt-instr' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-instr'
  7. [DBG] 'sbt-slicer' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-slicer'
  8. [DBG] 'klee' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee'
  9. [DBG] Working directory: /home/jasku/formela/symbiotic/install/bin/symbiotic_files
  10. [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/
  11. [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
  12. [DBG] C_INCLUDE_DIR=/home/jasku/formela/symbiotic/install/include
  13. 7.0.0-dev-llvm-8.0.1-symbiotic:2e2ceb47-dg:ccbc3536-sbt-slicer:85c8cb48-sbt-instrumentation:62c48199-klee:236d9920
  14. INFO: Looking for reachability of calls to reach_error
  15. [DBG] Running symbiotic-cc for klee
  16. |> 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
  17. [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]
  18. [DBG] extern int sprintf(char * , char * , ...) ;
  19. [DBG] ^
  20. [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 *, ...)'
  21. [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]
  22. [DBG] extern void *memcpy(void * , void * , size_t ) ;
  23. [DBG] ^
  24. [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)'
  25. [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]
  26. [DBG] extern void *memset(void * , int , size_t ) ;
  27. [DBG] ^
  28. [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)'
  29. [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]
  30. [DBG] __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
  31. [DBG] ~~~~~~~~~~ ^ ~~~~~~~~~~~~~~~~~~~~
  32. [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]
  33. [DBG] extern void *malloc(size_t size);
  34. [DBG] ^
  35. [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)'
  36. [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]
  37. [DBG] __builtin_expect(__cil_tmp23, 0L);
  38. [DBG] ^~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~
  39. [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]
  40. [DBG] __builtin_expect(__cil_tmp20, 0L);
  41. [DBG] ^~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~
  42. [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]
  43. [DBG] void main(void)
  44. [DBG] ^
  45. [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'
  46. [DBG] void main(void)
  47. [DBG] ^~~~
  48. [DBG] int
  49. [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]
  50. [DBG] extern void *calloc(size_t, size_t) ;
  51. [DBG] ^
  52. [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)'
  53. [DBG] 9 warnings generated.
  54. [DBG] Linking all input files into one file
  55. |> 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
  56. |> llvm-dis code.bc
  57. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code.bc
  58. |> 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
  59. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc
  60. |> 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
  61. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc
  62. |> 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 -lowerswitch
  63. Removed infinite loop in arch_local_save_flags
  64. Removed infinite loop in adpt_scsi_to_i2o
  65. INFO: Optimizations time: 3.1919498443603516
  66. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc
  67. |> 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
  68. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc
  69. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt.bc
  70. |> 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
  71. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc
  72. INFO: Starting slicing
  73. [DBG] Slicing the code for the 1. time
  74. |> timeout 300 sbt-slicer -c reach_error -pta fi /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc
  75. IntToPtr with constant: <badref> = inttoptr i32 -1 to i8*
  76. PTA: Inline assembly found, analysis may be unsound
  77. [RWG] WARNING: Inline assembler found
  78. [RWG] error: could not determine the called function in a call via pointer:
  79. adpt_fail_posted_scbs:: call void %36(%struct.scsi_cmnd* %37), !dbg !5403
  80. [RWG] error: could not determine the called function in a call via pointer:
  81. dma_free_attrs:: call void %34(%struct.device* %35, i32 %36, i8* %37, i64 %38, %struct.dma_attrs* %39), !dbg !5370
  82. [RWG] error: could not determine the called function in a call via pointer:
  83. dma_alloc_attrs:: %call11 = call i8* %25(%struct.device* %26, i32 %27, i64* %28, i32 %29, %struct.dma_attrs* %30), !dbg !5341
  84. [RWG] error: could not determine the called function in a call via pointer:
  85. adpt_i2o_to_scsi:: call void %453(%struct.scsi_cmnd* %454), !dbg !6655
  86. [llvm-slicer] CPU time of pointer analysis: 1.296470e-01 s
  87. [llvm-slicer] CPU time of reaching definitions analysis: 6.588100e-02 s
  88. [llvm-slicer] CPU time of control dependence analysis: 1.341300e-02 s
  89. [llvm-slicer] Finding dependent nodes took 0 sec 11 ms
  90. [llvm-slicer] Slicing dependence graph took 0 sec 35 ms
  91. [llvm-slicer] Sliced away 9174 from 29383 nodes in DG
  92. [llvm-slicer] saving sliced module to: /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.sliced
  93. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.sliced
  94. INFO: Total slicing time: 3.799220085144043
  95. |> 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
  96. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc
  97. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr.bc
  98. |> 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
  99. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  100. |> 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
  101. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bc
  102. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln.bc
  103. Linked our definitions to these undefined functions:
  104. __VERIFIER_assume
  105. |> 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 -verify
  106. INFO: Optimizations time: 2.0953357219696045
  107. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt.bc
  108. INFO: After-slicing optimizations and transformations time: 0.5340344905853271
  109. |> 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
  110. [DBG] Made global variable 'dma_ops' non-extern
  111. [DBG] Made global variable 'jiffies' non-extern
  112. [DBG] Made global variable 'current_task' non-extern
  113. [DBG] Made global variable 'x86_dma_fallback_dev' non-extern
  114. [DBG] Made global variable '__this_module' non-extern
  115. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr.bc
  116. |> 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 -O3
  117. INFO: Optimizations time: 2.7137928009033203
  118. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt.bc
  119. |> 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
  120. |> 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
  121. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  122. |> 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
  123. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-pr-ln-opt-pr-opt-ln.bc
  124. |> 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.bc
  125. Linked our definitions to these undefined functions:
  126. __VERIFIER_make_nondet
  127. INFO: Starting verification
  128. |> /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.bc
  129. KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0"
  130. KLEE: Using Z3 solver backend
  131. KLEE: Allocating memory with 32-bits addresses
  132. b'KLEE: WARNING ONCE: function "readl" has inline asm'
  133. b'KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm'
  134. b'KLEE: WARNING ONCE: function "get_current" has inline asm'
  135. b'KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm'
  136. b'KLEE: WARNING ONCE: function "readb" has inline asm'
  137. b'KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm'
  138. b'KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm'
  139. b'KLEE: WARNING: undefined reference to function: adpt_info'
  140. b'KLEE: WARNING: undefined reference to function: adpt_slave_configure'
  141. b'KLEE: WARNING: undefined reference to function: noop_llseek'
  142. b'KLEE: WARNING: undefined reference to function: printk'
  143. b'KLEE: WARNING: undefined reference to function: sprintf'
  144. #0 0x000056464de99ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4)
  145. #1 0x000056464de9a0e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9)
  146. #2 0x000056464de97fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8)
  147. #3 0x000056464de9a84e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e)
  148. #4 0x00007f42c9cff0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0)
  149. #5 0x00007f42c97dcad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3)
  150. #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)
  151. #7 0x000056464b95b36d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d)
  152. #8 0x000056464b966385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385)
  153. #9 0x000056464b8b2fe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)
  154. #10 0x00007f42c969f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)
  155. #11 0x000056464b93244e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)
  156. [DBG] The verifier return non-0 return status
  157. INFO: Verification time: 1.2384181022644043
  158. [DBG] Tool result: ERROR
  159. KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0"
  160. KLEE: Using Z3 solver backend
  161. KLEE: Allocating memory with 32-bits addresses
  162. KLEE: WARNING ONCE: function "readl" has inline asm
  163. KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm
  164. KLEE: WARNING ONCE: function "get_current" has inline asm
  165. KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm
  166. KLEE: WARNING ONCE: function "readb" has inline asm
  167. KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm
  168. KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm
  169. KLEE: WARNING: undefined reference to function: adpt_info
  170. KLEE: WARNING: undefined reference to function: adpt_slave_configure
  171. KLEE: WARNING: undefined reference to function: noop_llseek
  172. KLEE: WARNING: undefined reference to function: printk
  173. KLEE: WARNING: undefined reference to function: sprintf
  174. #0 0x000056464de99ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4)
  175. #1 0x000056464de9a0e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9)
  176. #2 0x000056464de97fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8)
  177. #3 0x000056464de9a84e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e)
  178. #4 0x00007f42c9cff0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0)
  179. #5 0x00007f42c97dcad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3)
  180. #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)
  181. #7 0x000056464b95b36d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d)
  182. #8 0x000056464b966385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385)
  183. #9 0x000056464b8b2fe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)
  184. #10 0x00007f42c969f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)
  185. #11 0x000056464b93244e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)
  186. INFO: Failed on the sliced code, trying on the unsliced code
  187. |> 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
  188. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc
  189. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr.bc
  190. |> 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
  191. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  192. |> 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
  193. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bc
  194. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln.bc
  195. Linked our definitions to these undefined functions:
  196. __VERIFIER_assume
  197. |> 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 -verify
  198. INFO: Optimizations time: 3.073033094406128
  199. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt.bc
  200. INFO: After-slicing optimizations and transformations time: 0.9150681495666504
  201. |> 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
  202. [DBG] Made global variable 'pv_irq_ops' non-extern
  203. [DBG] Made global variable 'dma_ops' non-extern
  204. [DBG] Made global variable 'jiffies' non-extern
  205. [DBG] Made global variable 'current_task' non-extern
  206. [DBG] Made global variable 'x86_dma_fallback_dev' non-extern
  207. [DBG] Made global variable '__this_module' non-extern
  208. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr.bc
  209. |> 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 -O3
  210. INFO: Optimizations time: 3.857717752456665
  211. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt.bc
  212. |> 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
  213. |> 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
  214. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  215. |> 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
  216. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-opt-pr-ln-opt-pr-opt-ln.bc
  217. |> 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.bc
  218. Linked our definitions to these undefined functions:
  219. __VERIFIER_make_nondet
  220. INFO: Starting verification
  221. |> /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.bc
  222. KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-1"
  223. KLEE: Using Z3 solver backend
  224. KLEE: Allocating memory with 32-bits addresses
  225. b'KLEE: WARNING ONCE: function "adpt_isr" has inline asm'
  226. b'KLEE: WARNING ONCE: function "readl" has inline asm'
  227. b'KLEE: WARNING ONCE: function "writel" has inline asm'
  228. b'KLEE: WARNING ONCE: function "adpt_send_nop" has inline asm'
  229. b'KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm'
  230. b'KLEE: WARNING ONCE: function "get_current" has inline asm'
  231. b'KLEE: WARNING ONCE: function "adpt_i2o_post_this" has inline asm'
  232. b'KLEE: WARNING ONCE: function "adpt_i2o_status_get" has inline asm'
  233. b'KLEE: WARNING ONCE: function "adpt_i2o_reset_hba" has inline asm'
  234. b'KLEE: WARNING ONCE: function "adpt_i2o_init_outbound_q" has inline asm'
  235. b'KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm'
  236. b'KLEE: WARNING ONCE: function "readb" has inline asm'
  237. b'KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm'
  238. b'KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm'
  239. b'KLEE: WARNING: undefined reference to function: noop_llseek'
  240. b'KLEE: WARNING: undefined reference to function: sprintf'
  241. #0 0x000055d5a1d62ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4)
  242. #1 0x000055d5a1d630e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9)
  243. #2 0x000055d5a1d60fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8)
  244. #3 0x000055d5a1d6384e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e)
  245. #4 0x00007fa87f99f0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0)
  246. #5 0x00007fa87f47cad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3)
  247. #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)
  248. #7 0x000055d59f82436d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d)
  249. #8 0x000055d59f82f385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385)
  250. #9 0x000055d59f77bfe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)
  251. #10 0x00007fa87f33f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)
  252. #11 0x000055d59f7fb44e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)
  253. [DBG] The verifier return non-0 return status
  254. INFO: Verification time: 2.0022876262664795
  255. [DBG] Tool result: ERROR
  256. KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-1"
  257. KLEE: Using Z3 solver backend
  258. KLEE: Allocating memory with 32-bits addresses
  259. KLEE: WARNING ONCE: function "adpt_isr" has inline asm
  260. KLEE: WARNING ONCE: function "readl" has inline asm
  261. KLEE: WARNING ONCE: function "writel" has inline asm
  262. KLEE: WARNING ONCE: function "adpt_send_nop" has inline asm
  263. KLEE: WARNING ONCE: function "adpt_i2o_post_wait" has inline asm
  264. KLEE: WARNING ONCE: function "get_current" has inline asm
  265. KLEE: WARNING ONCE: function "adpt_i2o_post_this" has inline asm
  266. KLEE: WARNING ONCE: function "adpt_i2o_status_get" has inline asm
  267. KLEE: WARNING ONCE: function "adpt_i2o_reset_hba" has inline asm
  268. KLEE: WARNING ONCE: function "adpt_i2o_init_outbound_q" has inline asm
  269. KLEE: WARNING ONCE: function "adpt_i2o_passthru" has inline asm
  270. KLEE: WARNING ONCE: function "readb" has inline asm
  271. KLEE: WARNING ONCE: function "adpt_queue_lck" has inline asm
  272. KLEE: WARNING ONCE: function "adpt_scsi_to_i2o" has inline asm
  273. KLEE: WARNING: undefined reference to function: noop_llseek
  274. KLEE: WARNING: undefined reference to function: sprintf
  275. #0 0x000055d5a1d62ef4 llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0cef4)
  276. #1 0x000055d5a1d630e9 (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d0e9)
  277. #2 0x000055d5a1d60fa8 llvm::sys::RunSignalHandlers() (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0afa8)
  278. #3 0x000055d5a1d6384e (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x2d0d84e)
  279. #4 0x00007fa87f99f0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0)
  280. #5 0x00007fa87f47cad3 __memmove_avx_unaligned_erms (/usr/lib/libc.so.6+0x165ad3)
  281. #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)
  282. #7 0x000055d59f82436d klee::Executor::initializeGlobals(klee::ExecutionState&) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7ce36d)
  283. #8 0x000055d59f82f385 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7d9385)
  284. #9 0x000055d59f77bfe8 main (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x725fe8)
  285. #10 0x00007fa87f33f152 __libc_start_main (/usr/lib/libc.so.6+0x28152)
  286. #11 0x000055d59f7fb44e _start (/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee+0x7a544e)
  287. INFO: Running on unsliced code time: 0.0005645751953125
  288. [DBG] ERROR
  289. Generating correctness witness: /home/jasku/formela/symbiotic/install/bin/witness.graphml
  290. Failure!
  291. RESULT: ERROR
  292. INFO: Total time elapsed: 55.98403978347778
  293.  
Advertisement
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!