diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2014-07-04 23:10:50 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2014-07-04 23:10:50 +0100 |
commit | 75f71cf58f8bea99a22228925e44fd2b330e4007 (patch) | |
tree | cd119f23e5577fbbb6b8abaf888273616f5c88e0 | |
parent | 6ae1a8a7d100019a97b96ad9bd0dcba273c6f7e8 (diff) | |
parent | bebc77433b86a2e9a38847c3189d63ca84f90e99 (diff) | |
download | klee-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.cpp | 3 | ||||
-rw-r--r-- | test/regression/2014-07-04-unflushed-error-report.c | 25 |
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; +} |