You may want to check if you have stack limit set to unlimited (you can do this using ulimit -s).
Best regards, Tomek > On 27 Feb 2015, at 10:52, Cristian Cadar <[email protected]> wrote: > > I cannot reproduce this on my machine. Can you open an issue at > https://github.com/klee/klee/issues, giving more details on your > configuration and how you ran KLEE? > > Best, > Cristian > > On 26/02/15 09:52, Yu-Fang Chen wrote: >> We tried two versions of STP (r940 and the latest) and KLEE gives us >> the message "BVTypeCheck: terms in atomic formulas must be of equal >> length" with both versions. >> >> Below is the program we run using klee and the output. >> >> PROGRAM: >> >> #include <assert.h> >> #include <klee/klee.h> >> #define N 5 >> >> int avg (int x[N]) >> { >> int i; >> int ret; >> ret = 0; >> for (i = 0; i < N; i++) { >> ret = ret + x[i]; >> } >> return ret / N; >> } >> >> int main () >> { >> int x[N]; >> int temp; >> int ret; >> int ret2; >> int ret5; >> >> klee_make_symbolic(x, sizeof x, "x"); >> >> ret = avg(x); >> >> temp=x[0];x[0] = x[1]; x[1] = temp; >> ret2 = avg(x); >> temp=x[0]; >> int i; >> for(i =0 ; i<N-1; i++){ >> x[i] = x[i+1]; >> } >> x[N-1] = temp; >> ret5 = avg(x); >> >> if(ret != ret2 || ret !=ret5){ >> ERROR: >> goto ERROR; >> } >> return 1; >> } >> >> >> >> OUTPUT: >> >> KLEE: output directory is "XXXXXX" >> valuewidth of lhs of EQ: 32 >> valuewidth of rhs of EQ: 64 >> indexwidth of lhs of EQ: 0 >> indexwidth of rhs of EQ: 0 >> Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length >> >> 338:(EQ >> 142:0x00000002 >> 336:0x000000000000003F) >> >> 0 >> error: STP Error: BVTypeCheck: terms in atomic formulas must be of equal >> length >> 0 klee 0x0000000000d9cb7f >> 1 klee 0x0000000000d9d089 >> 2 libpthread.so.0 0x00007f0ac3162bd0 >> 3 libc.so.6 0x00007f0ac239f037 gsignal + 55 >> 4 libc.so.6 0x00007f0ac23a2698 abort + 328 >> 5 klee 0x000000000062cbc9 >> 6 klee 0x0000000000dcebcf BEEV::FatalError(char const*, >> BEEV::ASTNode const&, int) + 127 >> 7 klee 0x0000000000dcf4f4 BEEV::BVTypeCheck(BEEV::ASTNode >> const&) + 1940 >> 8 klee 0x0000000000db37a6 vc_iteExpr + 54 >> 9 klee 0x0000000000632731 >> klee::STPBuilder::bvVarRightShift(klee::ExprHandle, klee::ExprHandle) >> + 225 >> 10 klee 0x000000000063380c >> klee::STPBuilder::constructSDivByConstant(klee::ExprHandle, unsigned >> int, unsigned long) + 428 >> 11 klee 0x00000000006365d1 >> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 7649 >> 12 klee 0x0000000000633f13 >> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323 >> 13 klee 0x0000000000634c72 >> klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*) + 1154 >> 14 klee 0x0000000000633f13 >> klee::STPBuilder::construct(klee::ref<klee::Expr>, int*) + 323 >> 15 klee 0x0000000000630393 >> 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&) + 387 >> 16 klee 0x000000000061bd15 >> CexCachingSolver::getAssignment(klee::Query const&, >> klee::Assignment*&) + 245 >> 17 klee 0x000000000061cf6b >> CexCachingSolver::computeValidity(klee::Query const&, >> klee::Solver::Validity&) + 843 >> 18 klee 0x000000000061a815 >> CachingSolver::computeValidity(klee::Query const&, >> klee::Solver::Validity&) + 149 >> 19 klee 0x000000000062956b >> IndependentSolver::computeValidity(klee::Query const&, >> klee::Solver::Validity&) + 315 >> 20 klee 0x00000000005f7eee >> klee::TimingSolver::evaluate(klee::ExecutionState const&, >> klee::ref<klee::Expr>, klee::Solver::Validity&) + 366 >> 21 klee 0x00000000005caaa2 >> klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, >> bool) + 226 >> 22 klee 0x00000000005d6ae3 >> klee::Executor::executeInstruction(klee::ExecutionState&, >> klee::KInstruction*) + 9123 >> 23 klee 0x00000000005d96d6 >> klee::Executor::run(klee::ExecutionState&) + 1798 >> 24 klee 0x00000000005d9fdd >> klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, >> char**) + 1805 >> 25 klee 0x00000000005b5c1c main + 6956 >> 26 libc.so.6 0x00007f0ac2389ea5 __libc_start_main + 245 >> 27 klee 0x00000000005bed31 >> Aborted (core dumped) >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
