diff --git a/benchexec/tools/svf-svc.py b/benchexec/tools/svf-svc.py index 9dfe46b28..1ff5ef496 100644 --- a/benchexec/tools/svf-svc.py +++ b/benchexec/tools/svf-svc.py @@ -46,16 +46,22 @@ 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 + elif line.startswith("ERROR("): + # This will always be a single word error. + return line + # Not matching any means something bad happened. return result.RESULT_ERROR