gazer/build/tools/gazer-theta/gazer-theta --inline all --search ERR --domain PRED_CART --refinement BW_BIN_ITP --initprec EMPTY --trace -test-harness=s3_clnt.blast.01.i.cil-2.c.ll sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:4:14: warning: incompatible redeclaration of library function 'malloc' [-Wincompatible-library-redeclaration] extern void *malloc(unsigned int sz ); ^ /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:4:14: note: 'malloc' is a builtin with type 'void *(unsigned long)' /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:1023:14: warning: incompatible redeclaration of library function 'memcpy' [-Wincompatible-library-redeclaration] extern void *memcpy(void * __restrict __dest , void const * __restrict __src , ^ /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:1023:14: note: 'memcpy' is a builtin with type 'void *(void *, const void *, unsigned long)' /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:1649:14: warning: incompatible redeclaration of library function 'calloc' [-Wincompatible-library-redeclaration] extern void *calloc(size_t, size_t); ^ /home/solarowl/Egyetem/ftsrg/ftsrg_tools/sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c:1649:14: note: 'calloc' is a builtin with type 'void *(unsigned long, unsigned long)' 3 warnings generated. warning: -math-int mode forces havoc memory model, analysis may be unsound Running theta verification backend. Writing theta CFA into '/tmp/gazer_theta_cfa-db4973.theta'. Building theta configuration. Built command: 'java -Djava.library.path=/home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/tools/gazer-theta/theta/lib -jar /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/tools/gazer-theta/theta/theta-cfa-cli.jar --model /tmp/gazer_theta_cfa-db4973.theta --domain PRED_CART --encoding LBE --initprec EMPTY --prunestrategy LAZY --precgranularity GLOBAL --predsplit WHOLE --refinement BW_BIN_ITP --search ERR --maxenum 0 --loglevel RESULT --cex /tmp/gazer_theta_cex-d59913'. Running theta... Verification FAILED. Assertion failure in sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c at line 1645 column 11. Error trace: ------------ #0 in function main(): call malloc() returned ??? at 1066:18 s := ??? at 1066:12 call malloc() returned ??? at 1070:11 call malloc() returned ??? at 1071:12 call malloc() returned ??? at 1072:16 call __VERIFIER_nondet_int() returned ??? at 1074:16 #1 in function ssl3_connect(undef): s := ??? at 1066:12 call __VERIFIER_nondet_ulong() returned ??? at 1081:29 buf := False at 1081:18 call __VERIFIER_nondet_int() returned ??? at 1090:17 tmp___1 := ??? at 1090:17 call __VERIFIER_nondet_int() returned ??? at 1091:17 tmp___2 := ??? at 1091:17 blastFlag := 0 (0b00000000000000000000000000000000) call __VERIFIER_nondet_int() returned ??? at 1104:10 call __VERIFIER_nondet_int() returned ??? at 1106:9 tmp := ??? cb := ??? ret := -1 (0b11111111111111111111111111111111) skip := 0 (0b00000000000000000000000000000000) blastFlag := 0 at 1103:13 skip := 0 (0b00000000000000000000000000000000) state := 6 at 1132:16 call __VERIFIER_nondet_int() returned 1 at 1289:79 ret := 1 at 1289:79 blastFlag := ??? blastFlag := 1 blastFlag := 1 skip := 0 skip := 0 (0b00000000000000000000000000000000) blastFlag := 1 at 1103:13 skip := 0 (0b00000000000000000000000000000000) state := 12 at 1132:16 call __VERIFIER_nondet_int() returned 1 at 1310:79 ret := 1 at 1310:79 blastFlag := 2 blastFlag := 2 skip := 0 call __VERIFIER_nondet_int() returned 1 at 1607:17 ret := 1 at 1607:17 skip := 0 (0b00000000000000000000000000000000) blastFlag := 2 at 1103:13 skip := 0 (0b00000000000000000000000000000000) state := 20 at 1132:16 call __VERIFIER_nondet_int() returned 1 at 1333:81 ret := 1 at 1333:81 blastFlag := 3 blastFlag := 3 skip := 0 blastFlag := 3 skip := 0 skip := 0 (0b00000000000000000000000000000000) blastFlag := 3 at 1103:13 skip := 0 (0b00000000000000000000000000000000) state := 29 at 1132:16 call __VERIFIER_nondet_int() returned 1 at 1350:79 ret := 1 at 1350:79 blastFlag := ??? blastFlag := 4 call __VERIFIER_nondet_int() returned 40 at 1363:83 tmp___6 := 40 at 1363:83 blastFlag := 4 skip := 0 skip := 0 (0b00000000000000000000000000000000) blastFlag := 4 at 1103:13 skip := 0 (0b00000000000000000000000000000000) state := 42 at 1132:16 call __VERIFIER_nondet_int() returned 63 at 1389:79 ret := 63 at 1389:79 Generating test harness. gazer-theta: /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/Trace/TestHarnessGenerator.cpp:32: llvm::Constant* exprToLLVMValue(gazer::ExprRef&, llvm::LLVMContext&, llvm::Type*): Assertion `targetTy->isIntegerTy() || (!expr->getType().isBvType() && !expr->getType().isIntType() && !expr->getType().isBoolType()) && "Bitvectors, integers, and booleans may only have integer as their target type!"' failed. #0 0x00007f8ceae49e9b llvm::sys::PrintStackTrace(llvm::raw_ostream&) (/home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/src/Core/libGazerCore.so+0x1a8e9b) #1 0x00007f8ceae47d44 llvm::sys::RunSignalHandlers() (/home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/src/Core/libGazerCore.so+0x1a6d44) #2 0x00007f8ceae47e93 SignalHandler(int) (/home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/src/Core/libGazerCore.so+0x1a6e93) #3 0x00007f8ceabab0f0 __restore_rt (/usr/lib/libpthread.so.0+0x140f0) #4 0x00007f8cea6ce615 raise (/usr/lib/libc.so.6+0x3d615) #5 0x00007f8cea6b7862 abort (/usr/lib/libc.so.6+0x26862) #6 0x00007f8cea6b7747 _nl_load_domain.cold (/usr/lib/libc.so.6+0x26747) #7 0x00007f8cea6c6bf6 (/usr/lib/libc.so.6+0x35bf6) #8 0x00007f8cecc33da0 exprToLLVMValue(boost::intrusive_ptr&, llvm::LLVMContext&, llvm::Type*) /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/Trace/TestHarnessGenerator.cpp:32:5 #9 0x00007f8cecc34816 auto gazer::GenerateTestHarnessModuleFromTrace(gazer::Trace&, llvm::LLVMContext&, llvm::Module const&)::'lambda'(auto&)::operator() >(auto&) const /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/Trace/TestHarnessGenerator.cpp:83:91 #10 0x00007f8cecc34881 std::back_insert_iterator > std::transform<__gnu_cxx::__normal_iterator*, std::vector, std::allocator > > >, std::back_insert_iterator >, gazer::GenerateTestHarnessModuleFromTrace(gazer::Trace&, llvm::LLVMContext&, llvm::Module const&)::'lambda'(auto&)>(auto, auto, std::back_insert_iterator >, gazer::GenerateTestHarnessModuleFromTrace(gazer::Trace&, llvm::LLVMContext&, llvm::Module const&)::'lambda'(auto&)) /usr/include/c++/10.2.0/bits/stl_algo.h:4313:24 #11 0x00007f8cecc342dc gazer::GenerateTestHarnessModuleFromTrace(gazer::Trace&, llvm::LLVMContext&, llvm::Module const&) /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/Trace/TestHarnessGenerator.cpp:86:42 #12 0x00007f8cecc879ad (anonymous namespace)::RunVerificationBackendPass::runOnModule(llvm::Module&) /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/LLVMFrontend.cpp:237:42 #13 0x00007f8cecda3240 llvm::legacy::PassManagerImpl::run(llvm::Module&) (/home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/build/src/LLVM/libGazerLLVM.so+0x548240) #14 0x00007f8cecc87e10 gazer::LLVMFrontend::run() /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/src/LLVM/LLVMFrontend.cpp:310:1 #15 0x00005558fac0a0bc main /home/solarowl/Egyetem/ftsrg/ftsrg_tools/gazer/tools/gazer-theta/gazer-theta.cpp:134:22 #16 0x00007f8cea6b9152 __libc_start_main (/usr/lib/libc.so.6+0x28152) #17 0x00005558fac09c9e _start (gazer/build/tools/gazer-theta/gazer-theta+0x53c9e) Stack dump: 0. Running pass 'Verification backend pass' on module '/tmp/gazer_workdir_-7fa65c/gazer_llvm_output.bc'. Aborted (core dumped)