| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Otherwise optimizations done in klee won't have any effect.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
even if there were many divide by zero bugs.
The fix basically inlines all function calls to klee_div_zero_check()
so that each call to klee_report_error() is a unique instruction
for each instrumentation of a divide operation.
It also seems that inlining the call "magically" fixed the debug information
(file and line number) of the instruction so that the debug information on the
inlined instructions matches that of the instrumented division instruction.
Note that the command line option -emit-all-errors could be used to
workaround the bug fixed in this commit.
|
