Skip to content

Commit 75d8e56

Browse files
committed
Fix CPROVER counterexample translation
In some versions of CBMC, the full array is printed to the counterexample every time an assignment to the array is performed. We use the line number information to detect this and avoid printing the whole thing.
1 parent 443436f commit 75d8e56

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

cex.py

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ def fmt(match, store_name, tid):
8181
s[1] for s in states
8282
if s[0]["function"] == "init" and not(LTSTAMP.match(s[1][0])))
8383
others = [
84-
(s[0]["function"], *s[1]) for s in states
84+
(s[0]["function"], s[0]["line"], *s[1]) for s in states
8585
if s[0]["function"] not in ("init", "__CPROVER_initialize")]
8686
yield "<initialization>"
8787
for i in inits:
@@ -92,7 +92,8 @@ def fmt(match, store_name, tid):
9292

9393
agent = ""
9494
system = None
95-
for i, (func, var, value) in enumerate(others):
95+
last_line = None
96+
for i, (func, line, var, value) in enumerate(others):
9697
if var == "__LABS_step":
9798
if system:
9899
yield f"\n<end {system}>"
@@ -102,12 +103,11 @@ def fmt(match, store_name, tid):
102103
yield f"\n<{pprint_agent(info, agent)}: {func} '{info.lstig[int(value)].name}'>" # noqa: E501
103104
elif var in ("firstAgent", "guessedcomp"):
104105
agent = value
105-
else:
106-
if (len(others) > i + 1 and LSTIG.match(var) and
107-
LTSTAMP.match(others[i + 1][0])):
108-
pprint = pprint_assign(var, value, agent, endline=" ")
109-
else:
110-
pprint = pprint_assign(var, value, agent)
106+
# If multiple assignments correspond to the same line, it's because
107+
# we assigned to an array and CBMC is printing out the whole thing
108+
elif last_line != line:
109+
pprint = pprint_assign(var, value, agent)
110+
last_line = line
111111
if pprint:
112112
yield pprint
113113

0 commit comments

Comments
 (0)