diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 16 | ||||
| -rw-r--r-- | lib/Solver/CoreSolver.cpp | 19 | ||||
| -rw-r--r-- | test/regression/2017-02-21-pathOS-id.c | 19 |
3 files changed, 39 insertions, 15 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 48a4a32f..95812dd7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -976,14 +976,18 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { falseState->ptreeNode = res.first; trueState->ptreeNode = res.second; - if (!isInternal) { - if (pathWriter) { - falseState->pathOS = pathWriter->open(current.pathOS); + if (pathWriter) { + // Need to update the pathOS.id field of falseState, otherwise the same id + // is used for both falseState and trueState. + falseState->pathOS = pathWriter->open(current.pathOS); + if (!isInternal) { trueState->pathOS << "1"; falseState->pathOS << "0"; - } - if (symPathWriter) { - falseState->symPathOS = symPathWriter->open(current.symPathOS); + } + } + if (symPathWriter) { + falseState->symPathOS = symPathWriter->open(current.symPathOS); + if (!isInternal) { trueState->symPathOS << "1"; falseState->symPathOS << "0"; } diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 783047f8..d36a3219 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -8,6 +8,7 @@ //===----------------------------------------------------------------------===// #include "klee/CommandLine.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" @@ -51,10 +52,10 @@ static klee::Solver *handleMetaSMT() { UseForkedCoreSolver, CoreSolverOptimizeDivides); break; default: - llvm_unreachable("Unrecognised metasmt backend"); + llvm_unreachable("Unrecognised MetaSMT backend"); break; }; - llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n"; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); return coreSolver; } #endif /* ENABLE_METASMT */ @@ -65,32 +66,32 @@ Solver *createCoreSolver(CoreSolverType cst) { switch (cst) { case STP_SOLVER: #ifdef ENABLE_STP - llvm::errs() << "Using STP solver backend\n"; + klee_message("Using STP solver backend"); return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); #else - llvm::errs() << "Not compiled with STP support\n"; + klee_message("Not compiled with STP support"); return NULL; #endif case METASMT_SOLVER: #ifdef ENABLE_METASMT - llvm::errs() << "Using MetaSMT solver backend\n"; + klee_message("Using MetaSMT solver backend"); return handleMetaSMT(); #else - llvm::errs() << "Not compiled with MetaSMT support\n"; + klee_message("Not compiled with MetaSMT support"); return NULL; #endif case DUMMY_SOLVER: return createDummySolver(); case Z3_SOLVER: #ifdef ENABLE_Z3 - llvm::errs() << "Using Z3 solver backend\n"; + klee_message("Using Z3 solver backend"); return new Z3Solver(); #else - llvm::errs() << "Not compiled with Z3 support\n"; + klee_message("Not compiled with Z3 support"); return NULL; #endif case NO_SOLVER: - llvm::errs() << "Invalid solver\n"; + klee_message("Invalid solver"); return NULL; default: llvm_unreachable("Unsupported CoreSolverType"); diff --git a/test/regression/2017-02-21-pathOS-id.c b/test/regression/2017-02-21-pathOS-id.c new file mode 100644 index 00000000..d3bffbe0 --- /dev/null +++ b/test/regression/2017-02-21-pathOS-id.c @@ -0,0 +1,19 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out -write-paths %t.bc 2> %t.log +// RUN: cat %t.klee-out/test000001.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000002.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000003.path | wc -l | grep -q 1 +// RUN: cat %t.klee-out/test000004.path | wc -l | grep -q 1 +int main(){ + int a, b; + klee_make_symbolic (&a, sizeof(int), "a"); + klee_make_symbolic (&b, sizeof(int), "b"); + klee_assume(a<2); + klee_assume(a>=0); + malloc(a); + if(b){ + b++;//do something + } + return b; +} |