Hello all, I am testing a program with klee-fp. I use around 12 symbolic variables without problems, but when i make a specific variable symbolic i get this overflow.
Any ideas? *** buffer overflow detected ***: klee terminated ======= Backtrace: ========= /lib/x86_64-linux-gnu/libc.so.6(__fortify_fail+0x37)[0x7f8c47620f47] /lib/x86_64-linux-gnu/libc.so.6(+0x109e40)[0x7f8c4761fe40] /lib/x86_64-linux-gnu/libc.so.6(+0x1092a9)[0x7f8c4761f2a9] /lib/x86_64-linux-gnu/libc.so.6(_IO_default_xsputn+0xdd)[0x7f8c4759213d] /lib/x86_64-linux-gnu/libc.so.6(_IO_vfprintf+0x1d42)[0x7f8c47560702] /lib/x86_64-linux-gnu/libc.so.6(__vsprintf_chk+0x94)[0x7f8c4761f344] /lib/x86_64-linux-gnu/libc.so.6(__sprintf_chk+0x7d)[0x7f8c4761f28d] klee(_ZN4klee10STPBuilder15getInitialArrayEPKNS_5ArrayE+0x81)[0x603741] klee(_ZN4klee10STPBuilder17getArrayForUpdateEPKNS_5ArrayEPKNS_10UpdateNodeE+0x155)[0x603c15] klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1932)[0x605552] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3] klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3] klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3] klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x15b2)[0x6051d2] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3] klee(_ZN4klee10STPBuilder15constructActualENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x427)[0x604047] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiPNS0_11STPExprTypeE+0x1f7)[0x603287] klee(_ZN4klee10STPBuilder9constructENS_3refINS_4ExprEEEPiNS0_11STPExprTypeE+0x43)[0x6034b3] klee(_ZN13STPSolverImpl20computeInitialValuesERKN4klee5QueryERKSt6vectorIPKNS0_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EERb+0xbc)[0x5ff64c] klee(_ZN16CexCachingSolver13getAssignmentERKN4klee5QueryERPNS0_10AssignmentE+0xfe)[0x5ea0ce] klee(_ZN16CexCachingSolver20computeInitialValuesERKN4klee5QueryERKSt6vectorIPKNS0_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EERb+0x41)[0x5ea781] klee(_ZN4klee6Solver16getInitialValuesERKNS_5QueryERKSt6vectorIPKNS_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EE+0x13)[0x5fdef3] klee(_ZN4klee12TimingSolver16getInitialValuesERKNS_14ExecutionStateERKSt6vectorIPKNS_5ArrayESaIS7_EERS4_IS4_IhSaIhEESaISD_EE+0x15c)[0x5bcebc] klee(_ZN4klee8Executor19getSymbolicSolutionERKNS_14ExecutionStateERSt6vectorISt4pairISsS4_IhSaIhEEESaIS8_EE+0x28c)[0x57a89c] klee[0x5a0e03] klee(_ZN4klee8Executor20terminateStateOnExitERNS_14ExecutionStateE+0x2e)[0x57d1fe] klee(_ZN4klee8Executor18executeInstructionERNS_14ExecutionStateEPNS_12KInstructionE+0x5832)[0x58cfa2] klee(_ZN4klee8Executor3runERNS_14ExecutionStateE+0x772)[0x58dd52] klee(_ZN4klee8Executor17runFunctionAsMainEPN4llvm8FunctionEiPPcS5_+0x71f)[0x58e7af] klee(main+0x14c8)[0x568458] /lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xed)[0x7f8c4753776d] klee[0x574a31] ======= Memory map: ======== 00400000-01248000 r-xp 00000000 08:05 725940 /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee 01447000-0149e000 r--p 00e47000 08:05 725940 /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee 0149e000-0152b000 rw-p 00e9e000 08:05 725940 /home/fraunhofer/Desktop/klee-fp/klee-fp/bin/Release+Asserts/bin/klee 0152b000-01538000 rw-p 00000000 00:00 0 02dc3000-063cf000 rw-p 00000000 00:00 0 [heap] 7f8c37516000-7f8c47516000 rw-p 00000000 00:00 0 7f8c47516000-7f8c476cb000 r-xp 00000000 08:05 130848 /lib/x86_64-linux-gnu/libc-2.15.so 7f8c476cb000-7f8c478cb000 ---p 001b5000 08:05 130848 /lib/x86_64-linux-gnu/libc-2.15.so 7f8c478cb000-7f8c478cf000 r--p 001b5000 08:05 130848 /lib/x86_64-linux-gnu/libc-2.15.so 7f8c478cf000-7f8c478d1000 rw-p 001b9000 08:05 130848 /lib/x86_64-linux-gnu/libc-2.15.so 7f8c478d1000-7f8c478d6000 rw-p 00000000 00:00 0 7f8c478d6000-7f8c478eb000 r-xp 00000000 08:05 135220 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f8c478eb000-7f8c47aea000 ---p 00015000 08:05 135220 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f8c47aea000-7f8c47aeb000 r--p 00014000 08:05 135220 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f8c47aeb000-7f8c47aec000 rw-p 00015000 08:05 135220 /lib/x86_64-linux-gnu/libgcc_s.so.1 7f8c47aec000-7f8c47be7000 r-xp 00000000 08:05 130957 /lib/x86_64-linux-gnu/libm-2.15.so 7f8c47be7000-7f8c47de6000 ---p 000fb000 08:05 130957 /lib/x86_64-linux-gnu/libm-2.15.so 7f8c47de6000-7f8c47de7000 r--p 000fa000 08:05 130957 /lib/x86_64-linux-gnu/libm-2.15.so 7f8c47de7000-7f8c47de8000 rw-p 000fb000 08:05 130957 /lib/x86_64-linux-gnu/libm-2.15.so 7f8c47de8000-7f8c47eca000 r-xp 00000000 08:05 401337 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16 7f8c47eca000-7f8c480c9000 ---p 000e2000 08:05 401337 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16 7f8c480c9000-7f8c480d1000 r--p 000e1000 08:05 401337 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16 7f8c480d1000-7f8c480d3000 rw-p 000e9000 08:05 401337 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.16 7f8c480d3000-7f8c480e8000 rw-p 00000000 00:00 0 7f8c480e8000-7f8c480ea000 r-xp 00000000 08:05 130961 /lib/x86_64-linux-gnu/libdl-2.15.so 7f8c480ea000-7f8c482ea000 ---p 00002000 08:05 130961 /lib/x86_64-linux-gnu/libdl-2.15.so 7f8c482ea000-7f8c482eb000 r--p 00002000 08:05 130961 /lib/x86_64-linux-gnu/libdl-2.15.so 7f8c482eb000-7f8c482ec000 rw-p 00003000 08:05 130961 /lib/x86_64-linux-gnu/libdl-2.15.so 7f8c482ec000-7f8c48304000 r-xp 00000000 08:05 130955 /lib/x86_64-linux-gnu/libpthread-2.15.so 7f8c48304000-7f8c48503000 ---p 00018000 08:05 130955 /lib/x86_64-linux-gnu/libpthread-2.15.so 7f8c48503000-7f8c48504000 r--p 00017000 08:05 130955 /lib/x86_64-linux-gnu/libpthread-2.15.so 7f8c48504000-7f8c48505000 rw-p 00018000 08:05 130955 /lib/x86_64-linux-gnu/libpthread-2.15.so 7f8c48505000-7f8c48509000 rw-p 00000000 00:00 0 7f8c48509000-7f8c4852b000 r-xp 00000000 08:05 130958 /lib/x86_64-linux-gnu/ld-2.15.so 7f8c48658000-7f8c486d8000 rwxp 00000000 00:00 0 7f8c486d8000-7f8c486f9000 rw-p 00000000 00:00 0 7f8c48713000-7f8c48719000 rw-p 00000000 00:00 0 7f8c48727000-7f8c4872b000 rw-p 00000000 00:00 0 7f8c4872b000-7f8c4872c000 r--p 00022000 08:05 130958 /lib/x86_64-linux-gnu/ld-2.15.so 7f8c4872c000-7f8c4872e000 rw-p 00023000 08:05 130958 /lib/x86_64-linux-gnu/ld-2.15.so 7fffea404000-7fffea494000 rw-p 00000000 00:00 0 [stack] 7fffea5f8000-7fffea5f9000 r-xp 00000000 00:00 0 [vdso] ffffffffff600000-ffffffffff601000 r-xp 00000000 00:00 0 [vsyscall] 0 klee 0x0000000000d99fcf 1 klee 0x0000000000d9a4d9 2 libpthread.so.0 0x00007f8c482fbcb0 3 libc.so.6 0x00007f8c4754c425 gsignal + 53 4 libc.so.6 0x00007f8c4754fb8b abort + 379 5 libc.so.6 0x00007f8c4758a39e 6 libc.so.6 0x00007f8c47620f47 __fortify_fail + 55 7 libc.so.6 0x00007f8c4761fe40 8 libc.so.6 0x00007f8c4761f2a9 9 libc.so.6 0x00007f8c4759213d _IO_default_xsputn + 221 10 libc.so.6 0x00007f8c47560702 _IO_vfprintf + 7490 11 libc.so.6 0x00007f8c4761f344 __vsprintf_chk + 148 12 libc.so.6 0x00007f8c4761f28d __sprintf_chk + 125 13 klee 0x0000000000603741 klee::STPBuilder::getInitialArray(klee::Array const*) + 129 14 klee 0x0000000000603c15 klee::STPBuilder::getArrayForUpdate(klee::Array const*, klee::UpdateNode const*) + 341 15 klee 0x0000000000605552 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 6450 16 klee 0x0000000000603287 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 503 17 klee 0x00000000006034b3 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType) + 67 18 klee 0x00000000006051d2 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 5554 19 klee 0x0000000000603287 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 503 20 klee 0x00000000006034b3 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType) + 67 21 klee 0x00000000006051d2 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 5554 22 klee 0x0000000000603287 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 503 23 klee 0x00000000006034b3 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType) + 67 24 klee 0x00000000006051d2 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 5554 25 klee 0x0000000000603287 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 503 26 klee 0x00000000006034b3 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType) + 67 27 klee 0x0000000000604047 klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 1063 28 klee 0x0000000000603287 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType*) + 503 29 klee 0x00000000006034b3 klee::STPBuilder::construct(klee::ref<klee::Expr>, int*, klee::STPBuilder::STPExprType) + 67 30 klee 0x00000000005ff64c 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&) + 188 31 klee 0x00000000005ea0ce CexCachingSolver::getAssignment(klee::Query const&, klee::Assignment*&) + 254 32 klee 0x00000000005ea781 CexCachingSolver::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&) + 65 33 klee 0x00000000005fdef3 klee::Solver::getInitialValues(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> > > >&) + 19 34 klee 0x00000000005bcebc klee::TimingSolver::getInitialValues(klee::ExecutionState 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> > > >&) + 348 35 klee 0x000000000057a89c klee::Executor::getSymbolicSolution(klee::ExecutionState const&, std::vector<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > >, std::allocator<std::pair<std::string, std::vector<unsigned char, std::allocator<unsigned char> > > > >&) + 652 36 klee 0x00000000005a0e03 37 klee 0x000000000057d1fe klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 46 38 klee 0x000000000058cfa2 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 22578 39 klee 0x000000000058dd52 klee::Executor::run(klee::ExecutionState&) + 1906 40 klee 0x000000000058e7af klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1823 41 klee 0x0000000000568458 main + 5320 42 libc.so.6 0x00007f8c4753776d __libc_start_main + 237 43 klee 0x0000000000574a31 Aborted (core dumped) Regards, David
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
