Hi, kLEE group. when I test corutils-8.20 using " klee --simplify-sym-indices --write-cvcs --write-cov --output-module --max-memory=10000 --disable-inlining --use-forked-stp --use-cex-cache --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --run-in=/tmp/sandbox --max-sym-array-size=4096 --ignore-solver-failures --max-instruction-time=30. --max-time=1000000 --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search -check-div-zero --batch-instructions=10000 ./fmt.bc (or many other command) --sym-args 0 1 2 --sym-args 0 1 300 --sym-files 1 8 --sym-stdout", it sometimes comes across the problem below after it run only 1 hour or less to generate some paths, and I think it is not the problem "ulimit -s unlimited"that because I try it. How to solve the problem?
...... klee: ClauseAllocator.cpp:124: void* MINISAT::ClauseAllocator::allocEnough(uint32_t): Assertion `dataStart != __null' failed. 0 klee 0x089ff898 1 klee 0x089ffe04 2 0x40022400 __kernel_sigreturn + 0 3 0x40022424 __kernel_vsyscall + 16 4 libc.so.6 0x401b71df gsignal + 79 5 libc.so.6 0x401ba825 abort + 373 6 libc.so.6 0x401b0085 7 libc.so.6 0x401b0137 8 klee 0x08ae922d MINISAT::ClauseAllocator::allocEnough(unsigned int) + 925 9 klee 0x08aea69f MINISAT::Clause* MINISAT::ClauseAllocator::Clause_new<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit> const&, unsigned int, bool) + 47 10 klee 0x08a66efb MINISAT::Clause* MINISAT::Solver::addClauseInt<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit>&, unsigned int) + 507 11 klee 0x08a67189 bool MINISAT::Solver::addClause<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit>&, unsigned int, char*) + 457 12 klee 0x08a52f59 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 921 13 klee 0x08a53fea BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int, BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const, BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 122 14 klee 0x08a54b8a BEEV::ToSAT::CallSAT(MINISAT::Solver&, BEEV::ASTNode const&) + 2954 15 klee 0x08a51017 BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 39 16 klee 0x08a3f0eb BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&) + 8187 17 klee 0x08a403cc BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 252 18 klee 0x08a18e06 vc_query + 166 19 klee 0x08218f2e STPSolverImpl::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 2942 20 klee 0x08203166 CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 294 21 klee 0x08203b2b CexCachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 283 22 klee 0x08201e9f CachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 79 23 klee 0x08211473 IndependentSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 291 24 klee 0x08216abb klee::Solver::getValue(klee::Query const&, klee::ref<klee::ConstantExpr>&) + 187 25 klee 0x081e34ed klee::TimingSolver::getValue(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 637 26 klee 0x081e5470 klee::AddressSpace::resolveOne(klee::ExecutionState&, klee::TimingSolver*, klee::ref<klee::Expr>, std::pair<klee::MemoryObject const*, klee::ObjectState const*>&, bool&) + 288 27 klee 0x081ba1b5 klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 229 28 klee 0x081c10c0 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 10736 29 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803 30 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2151 31 klee 0x0819a6ce main + 11358 32 libc.so.6 0x401a24d3 __libc_start_main + 243 33 klee 0x081a7fc1 ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited' klee: ClauseAllocator.cpp:124: void* MINISAT::ClauseAllocator::allocEnough(uint32_t): Assertion `dataStart != __null' failed. 0 klee 0x089ff898 1 klee 0x089ffe04 2 0x40022400 __kernel_sigreturn + 0 3 0x40022424 __kernel_vsyscall + 16 4 libc.so.6 0x401b71df gsignal + 79 5 libc.so.6 0x401ba825 abort + 373 6 libc.so.6 0x401b0085 7 libc.so.6 0x401b0137 8 klee 0x08ae922d MINISAT::ClauseAllocator::allocEnough(unsigned int) + 925 9 klee 0x08aea69f MINISAT::Clause* MINISAT::ClauseAllocator::Clause_new<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit> const&, unsigned int, bool) + 47 10 klee 0x08a66efb MINISAT::Clause* MINISAT::Solver::addClauseInt<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit>&, unsigned int) + 507 11 klee 0x08a67189 bool MINISAT::Solver::addClause<MINISAT::vec<MINISAT::Lit> >(MINISAT::vec<MINISAT::Lit>&, unsigned int, char*) + 457 12 klee 0x08a52f59 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 921 13 klee 0x08a53fea BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int, BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const, BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 122 14 klee 0x08a54b8a BEEV::ToSAT::CallSAT(MINISAT::Solver&, BEEV::ASTNode const&) + 2954 15 klee 0x08a51017 BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 39 16 klee 0x08a3f0eb BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&) + 8187 17 klee 0x08a403cc BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 252 18 klee 0x08a18e06 vc_query + 166 19 klee 0x08218f2e STPSolverImpl::computeInitialValues(klee::Query const&, std::vector<klee::Array const*, std::allocator<klee::Array const*> > const&, std::vector<std::vector<unsigned char, std::allocator<unsigned char> >, std::allocator<std::vector<unsigned char, std::allocator<unsigned char> > > >&, bool&) + 2942 20 klee 0x08203166 CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 294 21 klee 0x08203b2b CexCachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 283 22 klee 0x08201e9f CachingSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 79 23 klee 0x08211473 IndependentSolver::computeValue(klee::Query const&, klee::ref<klee::Expr>&) + 291 24 klee 0x08216abb klee::Solver::getValue(klee::Query const&, klee::ref<klee::ConstantExpr>&) + 187 25 klee 0x081e34ed klee::TimingSolver::getValue(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::ref<klee::ConstantExpr>&) + 637 26 klee 0x081b3124 klee::Executor::toConstant(klee::ExecutionState&, klee::ref<klee::Expr>, char const*) + 292 27 klee 0x081ba219 klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 329 28 klee 0x081c10c0 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 10736 29 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803 30 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2151 31 klee 0x0819a6ce main + 11358 32 libc.so.6 0x401a24d3 __libc_start_main + 243 33 klee 0x081a7fc1 ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited' klee: Executor.cpp:1009: klee::ref<klee::ConstantExpr> klee::Executor::toConstant(klee::ExecutionState&, klee::ref<klee::Expr>, const char*): Assertion `success && "FIXME: Unhandled solver failure"' failed. 0 klee 0x089ff898 1 klee 0x089ffe04 2 0x40022400 __kernel_sigreturn + 0 3 0x40022424 __kernel_vsyscall + 16 4 libc.so.6 0x401b71df gsignal + 79 5 libc.so.6 0x401ba825 abort + 373 6 libc.so.6 0x401b0085 7 libc.so.6 0x401b0137 8 klee 0x081b3764 klee::Executor::toConstant(klee::ExecutionState&, klee::ref<klee::Expr>, char const*) + 1892 9 klee 0x081ba219 klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 329 10 klee 0x081c10c0 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 10736 11 klee 0x081c46fb klee::Executor::run(klee::ExecutionState&) + 1803 12 klee 0x081c5337 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2151 13 klee 0x0819a6ce main + 11358 14 libc.so.6 0x401a24d3 __libc_start_main + 243 15 klee 0x081a7fc1 Aborted (core dumped)
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
