Double Dave
2014-01-07 21:56:56 UTC
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
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