diff options
| author | Jordy Ruiz <jruiz@ic.ac.uk> | 2020-08-08 10:04:55 +0200 |
|---|---|---|
| committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-08-23 10:51:48 +0100 |
| commit | 729ecede246be700bd483ff47d5462814df08b82 (patch) | |
| tree | b9287894b6bbf2e58b417125c87a710601dc0d42 /runtime | |
| parent | 085c54b980a2f62c7c475d32b5d0ce9c6f97904f (diff) | |
| download | klee-729ecede246be700bd483ff47d5462814df08b82.tar.gz | |
klee-stats: check for a run.stats file in the klee-out directory, to prevent outputting wrong data.
When KLEE crashes, it produces an empty info file, so it is not enough to check for the existence of an info file. Previously, table columns would mismatch and return data labeled with the wrong directory names.
Diffstat (limited to 'runtime')
0 files changed, 0 insertions, 0 deletions