Commit 6c65e7ee authored by Johannes Kanig's avatar Johannes Kanig

Q520-002 fix unsoundness related to exceptions

On N127-001, an optimisation of the fast WP was introduced, based on
marking states that contain variables that need to be refreshed when
merging them. However, this "marked" status was incorrectly reset to
false when merging states, even though some of those "unfresh" variables
could survive the merge. The consequence was that the WP was reusing
variables too aggressively, which would result in incorrect VCs.

We now compute the marked status of a merged state from the states to be
merged: if one of them is marked, the merged state is marked too.

mlw_wp.ml:
(merge): synthetize marked status from input states

Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995
parent c7432733
......@@ -1426,7 +1426,7 @@ end = struct
{ base with now =
{ subst_vars = vars;
subst_regions = regs };
marked = false;
marked = marked;
},
List.map2 t_and_simp fl1 fl2
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment