Fix regression reported by Michael Esser and Andrew Watson

(independently).

In our recently switch to llvm::raw_ostream (and friends) (I think this
is d934d983692c8952cdb887cbcd59f2df0001b9c0) we forgot to flush the
llvm::raw_string_ostream to the underlying string used for error report
files (e.g. test000001.overshift.err) so we would end up writing an
empty string to error report files.

Also added a test case to catch this.

1 files changed, 25 insertions, 0 deletions

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;
+}