API tools faq
paste
tomsik68

dg vr issue #369

tomsik68
Nov 26th, 2020
317
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 25.51 KB | None | 0 0
raw download clone embed print report
  1. [DBG] Will use 32-bit environment
  2. [DBG] Symbiotic dir: /home/jasku/formela/symbiotic/install
  3. [DBG] 'clang' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/clang'
  4. [DBG] 'opt' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/opt'
  5. [DBG] 'llvm-link' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-link'
  6. [DBG] 'llvm-nm' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/llvm-nm'
  7. [DBG] 'sbt-instr' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-instr'
  8. [DBG] 'sbt-slicer' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/sbt-slicer'
  9. [DBG] 'klee' is '/home/jasku/formela/symbiotic/install/llvm-8.0.1/bin/klee'
  10. [DBG] Working directory: /home/jasku/formela/symbiotic/install/bin/symbiotic_files
  11. [DBG] PATH=/home/jasku/formela/symbiotic/install/slowbeast:/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/:/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/
  12. [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
  13. [DBG] C_INCLUDE_DIR=/home/jasku/formela/symbiotic/install/include
  14. 7.9.0-dev-llvm-8.0.1-symbiotic:52661613-dg:d5c35153-sbt-slicer:85c8cb48-sbt-instrumentation:9df4452d-klee:acd0e7c0
  15. INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
  16. [DBG] Running symbiotic-cc for svcomp
  17. |> clang -cc1 --help
  18. [DBG] Clang supports lifetime markers, using it
  19. |> clang -c -emit-llvm -D__inline= -Wno-unused-parameter -Wno-unknown-attributes -Wno-unused-label -Wno-unknown-pragmas -Wno-unused-command-line-argument -Xclang -fsanitize-address-use-after-scope -O0 -disable-llvm-passes -g -fbracket-depth=-1 -I/home/jasku/formela/symbiotic/install/include -m32 -fno-discard-value-names -o tac-1.bc /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i
  20. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:233:12: warning: declaration of built-in function '__sigsetjmp' requires inclusion of the header <setjmp.h> [-Wbuiltin-requires-header]
  21. [DBG] extern int __sigsetjmp (struct __jmp_buf_tag __env[1], int __savemask) __attribute__ ((__nothrow__));
  22. [DBG] ^
  23. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:847:12: warning: incompatible redeclaration of library function 'snprintf' [-Wincompatible-library-redeclaration]
  24. [DBG] extern int snprintf (char *__restrict __s, size_t __maxlen,
  25. [DBG] ^
  26. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:847:12: note: 'snprintf' is a builtin with type 'int (char *, unsigned int, const char *, ...)'
  27. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:850:12: warning: incompatible redeclaration of library function 'vsnprintf' [-Wincompatible-library-redeclaration]
  28. [DBG] extern int vsnprintf (char *__restrict __s, size_t __maxlen,
  29. [DBG] ^
  30. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:850:12: note: 'vsnprintf' is a builtin with type 'int (char *, unsigned int, const char *, __builtin_va_list)'
  31. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:922:15: warning: incompatible redeclaration of library function 'fread' [-Wincompatible-library-redeclaration]
  32. [DBG] extern size_t fread (void *__restrict __ptr, size_t __size,
  33. [DBG] ^
  34. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:922:15: note: 'fread' is a builtin with type 'unsigned int (void *, unsigned int, unsigned int, FILE *)' (aka 'unsigned int (void *, unsigned int, unsigned int, struct _IO_FILE *)')
  35. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:924:15: warning: incompatible redeclaration of library function 'fwrite' [-Wincompatible-library-redeclaration]
  36. [DBG] extern size_t fwrite (const void *__restrict __ptr, size_t __size,
  37. [DBG] ^
  38. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:924:15: note: 'fwrite' is a builtin with type 'unsigned int (const void *, unsigned int, unsigned int, FILE *)' (aka 'unsigned int (const void *, unsigned int, unsigned int, struct _IO_FILE *)')
  39. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1293:14: warning: incompatible redeclaration of library function 'malloc' [-Wincompatible-library-redeclaration]
  40. [DBG] extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;
  41. [DBG] ^
  42. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1293:14: note: 'malloc' is a builtin with type 'void *(unsigned int)'
  43. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1294:14: warning: incompatible redeclaration of library function 'calloc' [-Wincompatible-library-redeclaration]
  44. [DBG] extern void *calloc (size_t __nmemb, size_t __size)
  45. [DBG] ^
  46. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1294:14: note: 'calloc' is a builtin with type 'void *(unsigned int, unsigned int)'
  47. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1298:14: warning: incompatible redeclaration of library function 'realloc' [-Wincompatible-library-redeclaration]
  48. [DBG] extern void *realloc (void *__ptr, size_t __size)
  49. [DBG] ^
  50. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1298:14: note: 'realloc' is a builtin with type 'void *(void *, unsigned int)'
  51. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1304:14: warning: incompatible redeclaration of library function 'alloca' [-Wincompatible-library-redeclaration]
  52. [DBG] extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));
  53. [DBG] ^
  54. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1304:14: note: 'alloca' is a builtin with type 'void *(unsigned int)'
  55. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1440:14: warning: incompatible redeclaration of library function 'memcpy' [-Wincompatible-library-redeclaration]
  56. [DBG] extern void *memcpy (void *__restrict __dest, const void *__restrict __src,
  57. [DBG] ^
  58. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1440:14: note: 'memcpy' is a builtin with type 'void *(void *, const void *, unsigned int)'
  59. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1442:14: warning: incompatible redeclaration of library function 'memmove' [-Wincompatible-library-redeclaration]
  60. [DBG] extern void *memmove (void *__dest, const void *__src, size_t __n)
  61. [DBG] ^
  62. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1442:14: note: 'memmove' is a builtin with type 'void *(void *, const void *, unsigned int)'
  63. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1449:14: warning: incompatible redeclaration of library function 'memset' [-Wincompatible-library-redeclaration]
  64. [DBG] extern void *memset (void *__s, int __c, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
  65. [DBG] ^
  66. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1449:14: note: 'memset' is a builtin with type 'void *(void *, int, unsigned int)'
  67. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1450:12: warning: incompatible redeclaration of library function 'memcmp' [-Wincompatible-library-redeclaration]
  68. [DBG] extern int memcmp (const void *__s1, const void *__s2, size_t __n)
  69. [DBG] ^
  70. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1450:12: note: 'memcmp' is a builtin with type 'int (const void *, const void *, unsigned int)'
  71. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1452:14: warning: incompatible redeclaration of library function 'memchr' [-Wincompatible-library-redeclaration]
  72. [DBG] extern void *memchr (const void *__s, int __c, size_t __n)
  73. [DBG] ^
  74. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1452:14: note: 'memchr' is a builtin with type 'void *(const void *, int, unsigned int)'
  75. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1462:14: warning: incompatible redeclaration of library function 'strncpy' [-Wincompatible-library-redeclaration]
  76. [DBG] extern char *strncpy (char *__restrict __dest,
  77. [DBG] ^
  78. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1462:14: note: 'strncpy' is a builtin with type 'char *(char *, const char *, unsigned int)'
  79. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1467:14: warning: incompatible redeclaration of library function 'strncat' [-Wincompatible-library-redeclaration]
  80. [DBG] extern char *strncat (char *__restrict __dest, const char *__restrict __src,
  81. [DBG] ^
  82. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1467:14: note: 'strncat' is a builtin with type 'char *(char *, const char *, unsigned int)'
  83. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1471:12: warning: incompatible redeclaration of library function 'strncmp' [-Wincompatible-library-redeclaration]
  84. [DBG] extern int strncmp (const char *__s1, const char *__s2, size_t __n)
  85. [DBG] ^
  86. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1471:12: note: 'strncmp' is a builtin with type 'int (const char *, const char *, unsigned int)'
  87. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1475:15: warning: incompatible redeclaration of library function 'strxfrm' [-Wincompatible-library-redeclaration]
  88. [DBG] extern size_t strxfrm (char *__restrict __dest,
  89. [DBG] ^
  90. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1475:15: note: 'strxfrm' is a builtin with type 'unsigned int (char *, const char *, unsigned int)'
  91. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1485:14: warning: incompatible redeclaration of library function 'strndup' [-Wincompatible-library-redeclaration]
  92. [DBG] extern char *strndup (const char *__string, size_t __n)
  93. [DBG] ^
  94. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1485:14: note: 'strndup' is a builtin with type 'char *(const char *, unsigned int)'
  95. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1496:15: warning: incompatible redeclaration of library function 'strcspn' [-Wincompatible-library-redeclaration]
  96. [DBG] extern size_t strcspn (const char *__s, const char *__reject)
  97. [DBG] ^
  98. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1496:15: note: 'strcspn' is a builtin with type 'unsigned int (const char *, const char *)'
  99. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1498:15: warning: incompatible redeclaration of library function 'strspn' [-Wincompatible-library-redeclaration]
  100. [DBG] extern size_t strspn (const char *__s, const char *__accept)
  101. [DBG] ^
  102. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1498:15: note: 'strspn' is a builtin with type 'unsigned int (const char *, const char *)'
  103. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1526:15: warning: incompatible redeclaration of library function 'strlen' [-Wincompatible-library-redeclaration]
  104. [DBG] extern size_t strlen (const char *__s)
  105. [DBG] ^
  106. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1526:15: note: 'strlen' is a builtin with type 'unsigned int (const char *)'
  107. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1540:13: warning: incompatible redeclaration of library function 'bzero' [-Wincompatible-library-redeclaration]
  108. [DBG] extern void bzero (void *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));
  109. [DBG] ^
  110. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1540:13: note: 'bzero' is a builtin with type 'void (void *, unsigned int)'
  111. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1553:12: warning: incompatible redeclaration of library function 'strncasecmp' [-Wincompatible-library-redeclaration]
  112. [DBG] extern int strncasecmp (const char *__s1, const char *__s2, size_t __n)
  113. [DBG] ^
  114. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1553:12: note: 'strncasecmp' is a builtin with type 'int (const char *, const char *, unsigned int)'
  115. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1572:14: warning: incompatible redeclaration of library function 'stpncpy' [-Wincompatible-library-redeclaration]
  116. [DBG] extern char *stpncpy (char *__restrict __dest,
  117. [DBG] ^
  118. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:1572:14: note: 'stpncpy' is a builtin with type 'char *(char *, const char *, unsigned int)'
  119. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:2735:39: warning: '^' within '|' [-Wbitwise-op-parentheses]
  120. [DBG] flags = flags | on_off->switch_on ^ trigger;
  121. [DBG] ~ ~~~~~~~~~~~~~~~~~~^~~~~~~~~
  122. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:2735:39: note: place parentheses around the '^' expression to silence this warning
  123. [DBG] flags = flags | on_off->switch_on ^ trigger;
  124. [DBG] ^
  125. [DBG] ( )
  126. [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:3033:1: warning: control may reach end of non-void function [-Wreturn-type]
  127. [DBG] }
  128. [DBG] ^
  129. [DBG] 27 warnings generated.
  130. [DBG] Linking all input files into one file
  131. |> llvm-link -o code.bc tac-1.bc
  132. |> llvm-dis code.bc
  133. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code.bc
  134. |> 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 -remove-error-calls -remove-infinite-loops
  135. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc
  136. INFO: Starting instrumentation
  137. |> timeout 400 sbt-instr /home/jasku/formela/symbiotic/install/llvm-8.0.1/share/sbt-instrumentation/memsafety/config-marker.json /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/marker.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-inst.bc --no-linking
  138. PredatorPlugin: Running Predator...
  139. |> predator_wrapper.py --out predator.log --32 predator_in.bc
  140. wrapper: `which slllvm` failed with error code 1
  141.  
  142. Predator wrapper finished with non-0 exit status
  143. PredatorPlugin: failed to open file with predator output
  144. Failed loading plugin: libPredatorPlugin.so
  145. Running DG points-to analysis with inv...
  146. PTA inv done.
  147. sbt-instr: /var/local/opt/llvm-8/llvm-8.0.1.src/lib/Support/APInt.cpp:195: llvm::APInt &llvm::APInt::operator+=(const llvm::APInt &): Assertion `BitWidth == RHS.BitWidth && "Bit widths must be the same"' failed.
  148. timeout: the monitored command dumped core
  149. PredatorPlugin: Running Predator...
  150. |> predator_wrapper.py --out predator.log --32 predator_in.bc
  151. wrapper: `which slllvm` failed with error code 1
  152. Predator wrapper finished with non-0 exit status
  153. PredatorPlugin: failed to open file with predator output
  154. Failed loading plugin: libPredatorPlugin.so
  155. Running DG points-to analysis with inv...
  156. PTA inv done.
  157. sbt-instr: /var/local/opt/llvm-8/llvm-8.0.1.src/lib/Support/APInt.cpp:195: llvm::APInt &llvm::APInt::operator+=(const llvm::APInt &): Assertion `BitWidth == RHS.BitWidth && "Bit widths must be the same"' failed.
  158. timeout: the monitored command dumped core
  159. INFO: Instrumentation [FAILED] time: 17.775286436080933
  160. |> 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 -replace-lifetime-markers -mark-volatile
  161. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc
  162. |> 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.bc
  163. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc
  164. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc
  165. |> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr.bc -explicit-consdes
  166. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr.bc
  167. |> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr.bc -remove-infinite-loops -remove-readonly-attr -dummy-marker
  168. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr.bc
  169. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr.bc
  170. |> 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/svcomp/__VERIFIER_assume.bc
  171. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  172. |> 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/strcmp.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/strcmp.bc
  173. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  174. |> 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/strcpy.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/strcpy.bc
  175. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  176. |> 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/strerror.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/strerror.bc
  177. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  178. |> 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/strlen.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/strlen.bc
  179. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  180. |> 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/strtoul.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/strtoul.bc
  181. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  182. |> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__VERIFIER_assume.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/strcmp.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/strcpy.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/strerror.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/strlen.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/strtoul.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr.bc
  183. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.bc
  184. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.bc
  185. |> 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/__ctype_b_loc.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/__ctype_b_loc.bc
  186. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  187. |> 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/__errno_location.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/__errno_location.bc
  188. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  189. |> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__ctype_b_loc.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/__errno_location.bc /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.bc
  190. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc
  191. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc
  192. Linked our definitions to these undefined functions:
  193. __VERIFIER_assume
  194. strcmp
  195. strcpy
  196. strerror
  197. strlen
  198. strtoul
  199. __ctype_b_loc
  200. __errno_location
  201. INFO: After-slicing optimizations and transformations time: 1.0502800941467285
  202. |> opt -load LLVMsbt.so /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr.bc -internalize-globals -remove-readonly-attr -O3 -remove-constant-exprs
  203. [DBG] Made global variable 'optind' non-extern
  204. [DBG] Made global variable 'optarg' non-extern
  205. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr.bc
  206. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr.bc
  207. |> 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/svcomp/__VERIFIER_make_nondet.bc
  208. [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument]
  209. |> llvm-link -o /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr-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-pr-pr-ln-ln-pr.bc
  210. |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr-ln.bc
  211. |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr-ln.bc
  212. Linked our definitions to these undefined functions:
  213. __VERIFIER_make_nondet
  214. INFO: Starting verification
  215. |> /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 -check-leaks -exit-on-error-type=Ptr -exit-on-error-type=Leak -exit-on-error-type=ReadOnly -exit-on-error-type=Free -exit-on-error-type=BadVectorAccess -write-witness -output-source=false /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr-ln.bc
  216. KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0"
  217. KLEE: Using Z3 solver backend
  218. KLEE: Allocating memory with 32-bits addresses
  219. KLEE: WARNING: undefined reference to function: __symbiotic_keep_ptr
  220. KLEE: WARNING: undefined reference to function: fflush
  221. KLEE: WARNING: undefined reference to function: fgetc
  222. KLEE: WARNING: undefined reference to function: fopen
  223. KLEE: WARNING: undefined reference to variable: stdin
  224. KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
  225. KLEE: ERROR: sv-benchmarks/c/busybox-1.22.0/tac-1.i:9: abort failure
  226. KLEE: NOTE: now ignoring this error at this location
  227. KLEE: WARNING ONCE: Alignment of memory from call "__VERIFIER_scope_enter" is not modelled. Using alignment of 8.
  228. RESULT: ERROR (interrupted)
  229. ERROR: == FAILURE ==
  230. interrupted
  231. Waiting for the child process to terminate
  232. Killed the child process
  233.  
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!