From bebc77433b86a2e9a38847c3189d63ca84f90e99 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 4 Jul 2014 15:46:57 +0100 Subject: 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. --- .../regression/2014-07-04-unflushed-error-report.c | 25 ++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 test/regression/2014-07-04-unflushed-error-report.c (limited to 'test') 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; +} -- cgit 1.4.1