Open Drodt opened 5 months ago
All modified and coverable lines are covered by tests :white_check_mark:
Project coverage is 37.77%. Comparing base (
1fb0c10
) to head (7472e4a
). Report is 114 commits behind head on main.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Related Issue
This pull request fixes #29.
Intended Change
A non-trivial (i.e, neither
true
norfalse
) diverges clause results in two contracts to be verified. Previously, there was one where the value of the clause (herediv
) is not true and the method therefore terminates, and one where the method does not terminate.E.g., the two POs would look like
pre & !div -> <m()>post
andpre -> [m()] post
. This resulted in more complex proofs, because the case wherediv
is false had to be considered as well for the second PO.This PR changes the POs to
pre & !div -> <m()>post
andpre & div -> [m()] post
Hence, we have a proper cut.
Type of pull request
Ensuring quality
Additional information and contact(s)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.