Merge pull request #589 from gladtbx/klee_fix_pathOS

Fix internal fork without new pathOS.id

2 files changed, 29 insertions, 6 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index c5d294fb..f5b46fc0 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -976,14 +976,18 @@ Executor::fork(ExecutionState &current, 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/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;
+}