[DBG] Will use 32-bit environment [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/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/ [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/include 7.9.0-dev-llvm-8.0.1-symbiotic:52661613-dg:d5c35153-sbt-slicer:85c8cb48-sbt-instrumentation:9df4452d-klee:acd0e7c0 INFO: Looking for invalid dereferences, invalid free, memory leaks, etc. [DBG] Running symbiotic-cc for svcomp |> clang -cc1 --help [DBG] Clang supports lifetime markers, using it |> 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 [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] [DBG] extern int __sigsetjmp (struct __jmp_buf_tag __env[1], int __savemask) __attribute__ ((__nothrow__)); [DBG] ^ [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] [DBG] extern int snprintf (char *__restrict __s, size_t __maxlen, [DBG] ^ [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 *, ...)' [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] [DBG] extern int vsnprintf (char *__restrict __s, size_t __maxlen, [DBG] ^ [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)' [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] [DBG] extern size_t fread (void *__restrict __ptr, size_t __size, [DBG] ^ [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 *)') [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] [DBG] extern size_t fwrite (const void *__restrict __ptr, size_t __size, [DBG] ^ [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 *)') [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] [DBG] extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ; [DBG] ^ [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)' [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] [DBG] extern void *calloc (size_t __nmemb, size_t __size) [DBG] ^ [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)' [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] [DBG] extern void *realloc (void *__ptr, size_t __size) [DBG] ^ [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)' [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] [DBG] extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__)); [DBG] ^ [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)' [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] [DBG] extern void *memcpy (void *__restrict __dest, const void *__restrict __src, [DBG] ^ [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)' [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] [DBG] extern void *memmove (void *__dest, const void *__src, size_t __n) [DBG] ^ [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)' [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] [DBG] extern void *memset (void *__s, int __c, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); [DBG] ^ [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)' [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] [DBG] extern int memcmp (const void *__s1, const void *__s2, size_t __n) [DBG] ^ [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)' [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] [DBG] extern void *memchr (const void *__s, int __c, size_t __n) [DBG] ^ [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)' [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] [DBG] extern char *strncpy (char *__restrict __dest, [DBG] ^ [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)' [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] [DBG] extern char *strncat (char *__restrict __dest, const char *__restrict __src, [DBG] ^ [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)' [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] [DBG] extern int strncmp (const char *__s1, const char *__s2, size_t __n) [DBG] ^ [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)' [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] [DBG] extern size_t strxfrm (char *__restrict __dest, [DBG] ^ [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)' [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] [DBG] extern char *strndup (const char *__string, size_t __n) [DBG] ^ [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)' [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] [DBG] extern size_t strcspn (const char *__s, const char *__reject) [DBG] ^ [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 *)' [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] [DBG] extern size_t strspn (const char *__s, const char *__accept) [DBG] ^ [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 *)' [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] [DBG] extern size_t strlen (const char *__s) [DBG] ^ [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 *)' [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] [DBG] extern void bzero (void *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))); [DBG] ^ [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)' [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] [DBG] extern int strncasecmp (const char *__s1, const char *__s2, size_t __n) [DBG] ^ [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)' [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] [DBG] extern char *stpncpy (char *__restrict __dest, [DBG] ^ [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)' [DBG] /home/jasku/formela/sv-benchmarks/c/busybox-1.22.0/tac-1.i:2735:39: warning: '^' within '|' [-Wbitwise-op-parentheses] [DBG] flags = flags | on_off->switch_on ^ trigger; [DBG] ~ ~~~~~~~~~~~~~~~~~~^~~~~~~~~ [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 [DBG] flags = flags | on_off->switch_on ^ trigger; [DBG] ^ [DBG] ( ) [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] [DBG] } [DBG] ^ [DBG] 27 warnings generated. [DBG] Linking all input files into one file |> llvm-link -o code.bc tac-1.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 -remove-error-calls -remove-infinite-loops |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr.bc INFO: Starting instrumentation |> 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 PredatorPlugin: Running Predator... |> predator_wrapper.py --out predator.log --32 predator_in.bc wrapper: `which slllvm` failed with error code 1 Predator wrapper finished with non-0 exit status PredatorPlugin: failed to open file with predator output Failed loading plugin: libPredatorPlugin.so Running DG points-to analysis with inv... PTA inv done. 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. timeout: the monitored command dumped core PredatorPlugin: Running Predator... |> predator_wrapper.py --out predator.log --32 predator_in.bc wrapper: `which slllvm` failed with error code 1 Predator wrapper finished with non-0 exit status PredatorPlugin: failed to open file with predator output Failed loading plugin: libPredatorPlugin.so Running DG points-to analysis with inv... PTA inv done. 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. timeout: the monitored command dumped core INFO: Instrumentation [FAILED] time: 17.775286436080933 |> 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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.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.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr.bc |> 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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr.bc |> 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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-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/svcomp/__VERIFIER_assume.bc [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [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-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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln.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/__ctype_b_loc.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/libc/__ctype_b_loc.bc [DBG] clang: warning: argument unused during compilation: '-I /home/jasku/formela/symbiotic/install/include' [-Wunused-command-line-argument] |> 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 [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-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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln.bc Linked our definitions to these undefined functions: __VERIFIER_assume strcmp strcpy strerror strlen strtoul __ctype_b_loc __errno_location INFO: After-slicing optimizations and transformations time: 1.0502800941467285 |> 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 [DBG] Made global variable 'optind' non-extern [DBG] Made global variable 'optarg' non-extern |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr.bc |> llvm-nm -undefined-only -just-symbol-name /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-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_make_nondet.bc /home/jasku/formela/symbiotic/install/llvm-8.0.1/lib32/verifier/svcomp/__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-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 |> llvm-dis /home/jasku/formela/symbiotic/install/bin/symbiotic_files/code-pr-pr-pr-pr-ln-ln-pr-ln.bc |> 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 Linked our definitions to these undefined functions: __VERIFIER_make_nondet INFO: 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 -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 KLEE: output directory is "/home/jasku/formela/symbiotic/install/bin/symbiotic_files/klee-out-0" KLEE: Using Z3 solver backend KLEE: Allocating memory with 32-bits addresses KLEE: WARNING: undefined reference to function: __symbiotic_keep_ptr KLEE: WARNING: undefined reference to function: fflush KLEE: WARNING: undefined reference to function: fgetc KLEE: WARNING: undefined reference to function: fopen KLEE: WARNING: undefined reference to variable: stdin KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8. KLEE: ERROR: sv-benchmarks/c/busybox-1.22.0/tac-1.i:9: abort failure KLEE: NOTE: now ignoring this error at this location KLEE: WARNING ONCE: Alignment of memory from call "__VERIFIER_scope_enter" is not modelled. Using alignment of 8. RESULT: ERROR (interrupted) ERROR: == FAILURE == interrupted Waiting for the child process to terminate Killed the child process
Comments