Skip to content

Commit

Permalink
Merge pull request sosy-lab#1107 from ultimate-pa/ultimate-dataraces
Browse files Browse the repository at this point in the history
Ultimate: fix output for data race violations
  • Loading branch information
PhilippWendler authored Nov 13, 2024
2 parents d8b67f1 + 5bd103a commit fc8c83c
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions benchexec/tools/ultimate.py
Original file line number Diff line number Diff line change
Expand Up @@ -363,6 +363,7 @@ def _determine_result_without_property_file(self, run):
ltl_false_string = "execution that violates the LTL property"
ltl_true_string = "Buchi Automizer proved that the LTL property"
overflow_false_string = "overflow possible"
datarace_false_string = "DataRaceFoundResult"

for line in run.output:
if unsupported_syntax_errorstring in line:
Expand All @@ -385,6 +386,8 @@ def _determine_result_without_property_file(self, run):
return "FALSE(valid-ltl)"
if ltl_true_string in line:
return result.RESULT_TRUE_PROP
if datarace_false_string in line:
return result.RESULT_FALSE_DATARACE
if unsafety_string in line:
return result.RESULT_FALSE_REACH
if mem_deref_false_string in line:
Expand Down Expand Up @@ -441,6 +444,8 @@ def _determine_result_with_property_file(run):
return result.RESULT_FALSE_TERMINATION
elif line.startswith("FALSE(OVERFLOW)"):
return result.RESULT_FALSE_OVERFLOW
elif line.startswith("FALSE(DATA-RACE)"):
return result.RESULT_FALSE_DATARACE
elif line.startswith("FALSE"):
return result.RESULT_FALSE_REACH
elif line.startswith("TRUE"):
Expand Down

0 comments on commit fc8c83c

Please sign in to comment.