KeYProject / key

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

Generalizing Logic Data Structures #3357

Closed Drodt closed 6 months ago

Drodt commented 9 months ago

Intended Change

This PR is the first step towards modularization of KeY to support target languages other than Java. We extract common data structures to ncore and took Feedback from the KaDa meetings into consideration. It does not break existing functionality and should be merged as otherwise maintaining a parallel version becomes difficult.

Type of pull request

Ensuring quality

Additional information and contact(s)

Current developers not involved in modularization can continue as usual with the following restrictions:

  1. Changes in ncore must be discussed with the core developers and inparticular @Drodt.
  2. PRs with changes to de.uka.ilkd.logic.* should always add @Drodt as an additional reviewer.
  3. Feedback is always welcome!

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 9 months ago

Codecov Report

Attention: Patch coverage is 55.43807% with 295 lines in your changes are missing coverage. Please review.

Project coverage is 37.85%. Comparing base (573c82c) to head (1256e74).

Files Patch % Lines
...c/main/java/de/uka/ilkd/key/logic/TermBuilder.java 48.21% 26 Missing and 3 partials :warning:
...rc/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java 51.16% 17 Missing and 4 partials :warning:
...java/de/uka/ilkd/key/logic/op/ModalOperatorSV.java 12.50% 21 Missing :warning:
...c/main/java/de/uka/ilkd/key/logic/op/Modality.java 66.66% 5 Missing and 10 partials :warning:
...ilkd/key/proof/init/FunctionalBlockContractPO.java 0.00% 13 Missing :warning:
.../ilkd/key/proof/init/FunctionalLoopContractPO.java 0.00% 12 Missing :warning:
.../src/main/java/de/uka/ilkd/key/logic/TermImpl.java 73.80% 1 Missing and 10 partials :warning:
.../main/java/de/uka/ilkd/key/java/TypeConverter.java 23.07% 10 Missing :warning:
...kd/key/informationflow/po/InfFlowProofSymbols.java 0.00% 7 Missing :warning:
...ilkd/key/informationflow/proof/init/StateVars.java 0.00% 7 Missing :warning:
... and 63 more
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3357 +/- ## ============================================ - Coverage 37.91% 37.85% -0.07% + Complexity 17069 17042 -27 ============================================ Files 2076 2082 +6 Lines 127020 127290 +270 Branches 21388 21441 +53 ============================================ + Hits 48165 48183 +18 - Misses 72949 73194 +245 - Partials 5906 5913 +7 ```

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