diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-08-30 16:43:30 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-09-02 16:45:06 +0100 |
| commit | f8301282120cc3cc58d641ddc99f92b14d894692 (patch) | |
| tree | 0c0f0a308496ee1abb050ceac3a1b95727a1390f /tools | |
| parent | 8cc2105aeb16e081a2ddd1128b6455cbdcb2ed3d (diff) | |
| download | klee-f8301282120cc3cc58d641ddc99f92b14d894692.tar.gz | |
Fixed bug where divide by zero bugs would only be detected once in a program
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.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions