From 6652625ce2b9f4f894932fa10066ef95275ca52b Mon Sep 17 00:00:00 2001 From: Lasagnenator <38394321+Lasagnenator@users.noreply.github.com> Date: Sat, 23 Nov 2024 16:21:21 +1100 Subject: [PATCH 1/2] Added more specific results --- benchexec/tools/svf-svc.py | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/benchexec/tools/svf-svc.py b/benchexec/tools/svf-svc.py index 9dfe46b28..43f5ed709 100644 --- a/benchexec/tools/svf-svc.py +++ b/benchexec/tools/svf-svc.py @@ -46,16 +46,19 @@ def cmdline(self, executable, options, task, rlimits): def determine_result(self, run): for line in run.output: - if line.startswith("Correct"): - return result.RESULT_TRUE_PROP - elif line.startswith("Incorrect"): + if line.startswith("REACH Incorrect"): + return result.RESULT_FALSE_REACH + elif line.startswith("MEMORY Incorrect"): + # SVF-SVC does not currently distinguish between memory safety types. + return result.RESULT_FALSE_PROP + elif line.startswith("OVERFLOW Incorrect"): + return result.RESULT_FALSE_OVERFLOW + elif "Incorrect" in line: return result.RESULT_FALSE_PROP - elif line.startswith("Error: "): - # The line should contain a short error message. - # The tool returns errors in the format Error: info. - error = line[line.index(":") + 2 :] - return result.RESULT_ERROR + "(" + error + ")" + elif "Correct" in line: + return result.RESULT_TRUE_PROP elif line.startswith("Unknown"): return result.RESULT_UNKNOWN + # Not matching the last three means something bad happened. return result.RESULT_ERROR From 573f76c6cd6659e462fd3f4c2c696f418b925baa Mon Sep 17 00:00:00 2001 From: Lasagnenator <38394321+Lasagnenator@users.noreply.github.com> Date: Sat, 23 Nov 2024 18:18:29 +1100 Subject: [PATCH 2/2] Added special errors --- benchexec/tools/svf-svc.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/benchexec/tools/svf-svc.py b/benchexec/tools/svf-svc.py index 43f5ed709..1ff5ef496 100644 --- a/benchexec/tools/svf-svc.py +++ b/benchexec/tools/svf-svc.py @@ -59,6 +59,9 @@ def determine_result(self, run): return result.RESULT_TRUE_PROP elif line.startswith("Unknown"): return result.RESULT_UNKNOWN + elif line.startswith("ERROR("): + # This will always be a single word error. + return line - # Not matching the last three means something bad happened. + # Not matching any means something bad happened. return result.RESULT_ERROR