KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Configurable enabled keys for JML condition evaluation #3373

Closed wadoon closed 8 months ago

wadoon commented 9 months ago

This PR allows you to configure the enabled keys in the processing of the JML conditions within the JML conditional annotation texts. Currently, the set is hard coded and only contains key as the only enabled key. This means, that KeY accepts the following JML annotation texts:

but ignores

Intended Change

Currently, there is no GUI element to configure this element.

The need for this raises from case study where you want to have the same source code as the foundation, but you have different verification runs: e.g, functional behavior under overflow absence, and a second run to prove overflow absence. Now you can differentiate the specificaton between the runs. For example:

//+first@ assert x>0;
//+second@ assume x>0;

Question to the reviewer

Type of pull request

codecov[bot] commented 9 months ago

Codecov Report

Attention: 16 lines in your changes are missing coverage. Please review.

Comparison is base (abbe1f8) 37.98% compared to head (a8a10a8) 37.98%. Report is 15 commits behind head on main.

Files Patch % Lines
...java/de/uka/ilkd/key/settings/GeneralSettings.java 23.80% 16 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3373 +/- ## ========================================= Coverage 37.98% 37.98% - Complexity 17024 17027 +3 ========================================= Files 2059 2059 Lines 126029 126051 +22 Branches 21282 21285 +3 ========================================= + Hits 47874 47883 +9 - Misses 72272 72285 +13 Partials 5883 5883 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.