Mentions légales du service

Skip to content
  • Johannes Kanig's avatar
    Q520-002 fix unsoundness related to exceptions · 6c65e7ee
    Johannes Kanig authored
    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
    6c65e7ee