Glad to hear you solved your problem. Although klee-fp is not actively maintained KLEE is. Would you mind seeing if this an issue in the upstream KLEE[1] and...
* Provide a patch to fix the issue along with a test case (the better option :) ) OR * Report the issue along with a test case on our issue tracker [2] ? [1] https://github.com/ccadar/klee [2] https://github.com/ccadar/klee/issues?state=open Thanks, Dan Liew. On 22 January 2014 20:41, Double Dave <[email protected]> wrote: > ok, i got a solution. Problem was that the name of a symbolic variable was > just to long. > Although i wouldn't consider 24 letters as too long, shortening these > variable names got my klee finally running. > > Regards, > David > > > On Tuesday, January 7, 2014 4:56 PM, Double Dave <[email protected]> > wrote: > 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_11STP > ExprTypeE+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_IhSa > IhEEESaIS8_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
