Closed flo2702 closed 1 month ago
Attention: Patch coverage is 60.52632%
with 15 lines
in your changes missing coverage. Please review.
Project coverage is 37.77%. Comparing base (
1b48b9e
) to head (04cc9ed
). Report is 56 commits behind head on main.:exclamation: Current head 04cc9ed differs from pull request most recent head 028663e
Please upload reports for the commit 028663e to get more accurate results.
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Related Issue
This pull request addresses #1663
Intended Change
When using a library method without an explicit contract, instead of getting stuck in the proof, KeY now assumes the following default contract
In addition, there is a proof setting
soundDefaultContracts
which can be turned off. In this case, the following default contract is used instead, which may be useful for exploratory proofsType of pull request
Ensuring quality
Additional information and contact(s)
This was done during HacKeYThon 2 by @JonasKlamroth and @flo2702
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.