Closed domainexpert closed 6 years ago
This fixes crashes with the following message when running with Coreutils (e.g., executing make dirname.tx in coreutils directory of klee-examples repository).
make dirname.tx
coreutils
klee-examples
klee: TxStore.cpp:161: bool klee::TxStore::isInLeftSubtree(uint64_t) const: Assertion `current->depth > targetDepth && "entry should have been defined in an ancestor node"' failed. 0 libLLVM-3.4.so.1 0x00007fa0b351e042 llvm::sys::PrintStackTrace(_IO_FILE*) + 34 1 libLLVM-3.4.so.1 0x00007fa0b351de34 2 libpthread.so.0 0x00007fa0b2423390 3 libc.so.6 0x00007fa0afbc2428 gsignal + 56 4 libc.so.6 0x00007fa0afbc402a abort + 362 5 libc.so.6 0x00007fa0afbbabd7 6 libc.so.6 0x00007fa0afbbac82 7 klee 0x00000000004f640b 8 klee 0x00000000004cc41f klee::TxStoreEntry::TxStoreEntry(klee::ref<klee::TxStateAddress>, klee::ref<klee::TxStateValue>, klee::ref<klee::TxStateValue>, klee::TxStore const*, unsigned long) + 863 9 klee 0x00000000004f77d3 klee::TxStore::MiddleStateStore::updateStore(klee::TxStore const*, klee::ref<klee::TxStateAddress>, klee::ref<klee::TxStateValue>, klee::ref<klee::TxStateValue>, unsigned long) + 227 10 klee 0x00000000004f84e8 klee::TxStore::updateStore(klee::ref<klee::TxStateAddress>, klee::ref<klee::TxStateValue>, klee::ref<klee::TxStateValue>) + 408 11 klee 0x00000000004dc13b klee::Dependency::execute(llvm::Instruction*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&, bool) + 4507 12 klee 0x00000000004dee97 klee::Dependency::executeMemoryOperation(llvm::Instruction*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&, std::vector<klee::ref<klee::Expr>, std::allocator<klee::ref<klee::Expr> > >&, bool, bool) + 71 13 klee 0x0000000000482b2e klee::TxTree::executeMemoryOperation(llvm::Instruction*, klee::ref<klee::Expr>, klee::ref<klee::Expr>, bool) + 206 14 klee 0x000000000047722e klee::Executor::executeMemoryOperation(klee::ExecutionState&, bool, klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::KInstruction*) + 4126 15 klee 0x0000000000478cab klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 2875 16 klee 0x000000000047eca9 klee::Executor::run(klee::ExecutionState&) + 1689 17 klee 0x000000000047f6c8 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1672 18 klee 0x00000000004581e0 main + 12688 19 libc.so.6 0x00007fa0afbad830 __libc_start_main + 240 20 klee 0x0000000000460759 _start + 41
With this patch, make check succeeded 100% and make in klee-examples basic did not result in change in subsumption and error counts.
make check
make
basic
This fixes crashes with the following message when running with Coreutils (e.g., executing
make dirname.tx
incoreutils
directory ofklee-examples
repository).With this patch,
make check
succeeded 100% andmake
inklee-examples
basic
did not result in change in subsumption and error counts.