[klee-dev] Fwd: Delivery Status Notification (Failure)
shuitao gan
ganshuitao at gmail.com
Fri Aug 2 04:30:55 BST 2013
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)
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list