Closed Drodt closed 5 months ago
Attention: Patch coverage is 94.36620%
with 4 lines
in your changes are missing coverage. Please review.
Project coverage is 37.90%. Comparing base (
1fb0c10
) to head (9f72a2d
).
Files | Patch % | Lines |
---|---|---|
.../key/nparser/builder/FunctionPredicateBuilder.java | 71.42% | 3 Missing and 1 partial :warning: |
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
Intended Change
This PR adds deconstructors for ADTs defined in KeY files. Let's say you have a file like
Previously, a sort
List
and two functionsList Nil
andList Cons(any, List)
were generated. Now, we also define two additional functions:any head(List)
andList tail(List)
, with the additional ruleshead(Cons(h, t)) = h
andtail(Cons(h, t)) = t
.Additionally, we now raise exceptions, when ADT definitions overwrite functions defined elsewhere. If two deconstructors should be defined, an exception is also raised. But, two deconstructors with the same name and return type are permitted.
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.