Hello Everyone, I wonder if I can ask a question about KLEE FP here, I am getting an assertion in Solver.cpp after 1 hour of klee-fp run and I am trying to understand why.
What is the meaning of this assertion? Am I doing something wrong? How can I find which line in my code has triggered it? Any directions would be appreciated! Thank you very much! $ clang -emit-llvm -c -g main.cpp $ time klee -libc=uclibc main.o KLEE: output directory = "klee-out-2" KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitC1Ev KLEE: WARNING: undefined reference to function: _ZNSt8ios_base4InitD1Ev KLEE: WARNING: undefined reference to function: _ZSt17__throw_bad_allocv KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_decrementPKSt18_Rb_tree_node_base KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_decrementPSt18_Rb_tree_node_base KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_incrementPKSt18_Rb_tree_node_base KLEE: WARNING: undefined reference to function: _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base KLEE: WARNING: undefined reference to function: _ZSt20__throw_out_of_rangePKc KLEE: WARNING: undefined reference to function: _ZSt28_Rb_tree_rebalance_for_erasePSt18_Rb_tree_node_baseRS_ KLEE: WARNING: undefined reference to function: _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_ KLEE: WARNING: undefined reference to function: _ZSt9terminatev KLEE: WARNING: undefined reference to function: __cxa_begin_catch KLEE: WARNING: undefined reference to function: __cxa_end_catch KLEE: WARNING: undefined reference to function: __cxa_rethrow KLEE: WARNING: undefined reference to function: __gxx_personality_v0 KLEE: WARNING: undefined reference to function: __restore_rt KLEE: WARNING: undefined reference to function: exp KLEE: WARNING: undefined reference to function: fcntl KLEE: WARNING: undefined reference to function: floor KLEE: WARNING: undefined reference to function: klee_cos KLEE: WARNING: undefined reference to function: klee_cosf KLEE: WARNING: undefined reference to function: klee_sin KLEE: WARNING: undefined reference to function: klee_sinf KLEE: WARNING: undefined reference to function: klee_sqrt KLEE: WARNING: undefined reference to function: klee_sqrtf KLEE: WARNING: undefined reference to function: lseek64 KLEE: WARNING: undefined reference to function: syscall KLEE: WARNING: undefined reference to function: time KLEE: WARNING: executable has module level assembly (ignoring) KLEE: WARNING: calling external: _ZNSt8ios_base4InitC1Ev(139919863132416) KLEE: WARNING: calling external: syscall(16, 0, 21505, 139919863148000) KLEE: WARNING: calling __user_main with extra arguments. KLEE: WARNING: calling external: time(0) KLEE: WARNING: calling external: _ZSt29_Rb_tree_insert_and_rebalancebPSt18_Rb_tree_node_baseS0_RS_(true, 139919863156288, 139919863151184, 139919863151184) KLEE: WARNING: calling external: exp(0) KLEE: WARNING: calling external: _ZSt18_Rb_tree_incrementPSt18_Rb_tree_node_base(139919863234656) klee: Solver.cpp:1103: MINISAT::PropagatedFrom MINISAT::Solver::propagate(bool): Assertion `c[1] == false_lit' failed. 0 klee 0x0000000000e6bdcf 1 klee 0x0000000000e6c2d9 2 libpthread.so.0 0x00007f41b29b7cb0 3 libc.so.6 0x00007f41b1c08425 gsignal + 53 4 libc.so.6 0x00007f41b1c0bb8b abort + 379 5 libc.so.6 0x00007f41b1c010ee 6 libc.so.6 0x00007f41b1c01192 7 klee 0x0000000000ec6c85 MINISAT::Solver::propagate(bool) + 1461 8 klee 0x0000000000ece364 MINISAT::Solver::search(int, int, bool) + 196 9 klee 0x0000000000ecf009 MINISAT::Solver::solve(MINISAT::vec<MINISAT::Lit> const&) + 1465 10 klee 0x0000000000ebfbe9 BEEV::ToSAT::toSATandSolve(MINISAT::Solver&, BEEV::ClauseList&, bool, BEEV::CNFMgr*&, bool, bool) + 3609 11 klee 0x0000000000ec021d BEEV::ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver&, std::map<int, BEEV::ClauseList*, BEEV::ltint, std::allocator<std::pair<int const, BEEV::ClauseList*> > >*, BEEV::CNFMgr*&) + 125 12 klee 0x0000000000ec0dcc BEEV::ToSAT::CallSAT(MINISAT::Solver&, BEEV::ASTNode const&) + 2956 13 klee 0x0000000000ebce2f BEEV::AbsRefine_CounterExample::CallSAT_ResultCheck(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&, BEEV::ToSATBase*) + 31 14 klee 0x0000000000eabab2 BEEV::STP::TopLevelSTPAux(MINISAT::Solver&, BEEV::ASTNode const&, BEEV::ASTNode const&) + 8050 15 klee 0x0000000000eacd8e BEEV::STP::TopLevelSTP(BEEV::ASTNode const&, BEEV::ASTNode const&) + 238 16 klee 0x0000000000e85a4d vc_query + 157 17 klee 0x0000000000617fa5 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&) + 1477 18 klee 0x00000000006024ee CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 254 19 klee 0x0000000000603829 CexCachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 1065 20 klee 0x0000000000600ff0 CachingSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 144 21 klee 0x00000000006114cc IndependentSolver::computeValidity(klee::Query const&, klee::Solver::Validity&) + 348 22 klee 0x00000000005d59f2 klee::TimingSolver::evaluate(klee::ExecutionState const&, klee::ref<klee::Expr>, klee::Solver::Validity&) + 546 23 klee 0x000000000059ab3f klee::Executor::fork(klee::ExecutionState&, klee::ref<klee::Expr>, bool, int) + 303 24 klee 0x00000000005a3f02 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 12706 25 klee 0x00000000005a71a2 klee::Executor::run(klee::ExecutionState&) + 1906 26 klee 0x00000000005a7c1f klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1823 27 klee 0x000000000057ddf8 main + 5320 28 libc.so.6 0x00007f41b1bf376d __libc_start_main + 237 29 klee 0x000000000058df81 Aborted (core dumped) real 100m21.991s user 99m41.830s sys 0m20.345s
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
