about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2014-07-04 23:10:50 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2014-07-04 23:10:50 +0100
commit75f71cf58f8bea99a22228925e44fd2b330e4007 (patch)
treecd119f23e5577fbbb6b8abaf888273616f5c88e0
parent6ae1a8a7d100019a97b96ad9bd0dcba273c6f7e8 (diff)
parentbebc77433b86a2e9a38847c3189d63ca84f90e99 (diff)
downloadklee-75f71cf58f8bea99a22228925e44fd2b330e4007.tar.gz
Merge pull request #133 from delcypher/fix_empty_error_report
Fix regression reported by Michael Esser and Andrew Watson
-rw-r--r--lib/Core/Executor.cpp3
-rw-r--r--test/regression/2014-07-04-unflushed-error-report.c25
2 files changed, 27 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index fcdf8a6d..f31d6aeb 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2808,7 +2808,8 @@ void Executor::terminateStateOnError(ExecutionState &state,
     std::string info_str = info.str();
     if (info_str != "")
       msg << "Info: \n" << info_str;
-    interpreterHandler->processTestCase(state, MsgString.c_str(), suffix);
+
+    interpreterHandler->processTestCase(state, msg.str().c_str(), suffix);
   }
     
   terminateState(state);
diff --git a/test/regression/2014-07-04-unflushed-error-report.c b/test/regression/2014-07-04-unflushed-error-report.c
new file mode 100644
index 00000000..63431370
--- /dev/null
+++ b/test/regression/2014-07-04-unflushed-error-report.c
@@ -0,0 +1,25 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: %klee -check-overshift %t.bc 2> %t.log
+// RUN: FileCheck -input-file=%T/klee-last/test000001.overshift.err %s
+
+/* This test checks that the error file isn't empty and contains the
+ * right content.
+ */
+int main()
+{
+  unsigned int x=15;
+  unsigned int y;
+  unsigned int z;
+  volatile unsigned int result;
+
+  /* Overshift if y>= sizeof(x) */
+  klee_make_symbolic(&y,sizeof(y),"shift_amount1");
+  // CHECK: Error: overshift error
+  // CHECK-NEXT: 2014-07-04-unflushed-error-report.c
+  // FIXME: Need newer FileCheck for to do ``Line: [[@LINE+1]]``
+  // Just hardcode line number for now
+  // CHECK-NEXT: Line: 22
+  result = x << y;
+
+  return 0;
+}