-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Generalize ParsableVariable and Schemavariables #3436
Conversation
Codecov ReportAttention: Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #3436 +/- ##
============================================
+ Coverage 37.86% 37.96% +0.10%
+ Complexity 17079 17058 -21
============================================
Files 2092 2081 -11
Lines 127596 126912 -684
Branches 21478 21332 -146
============================================
- Hits 48316 48186 -130
+ Misses 73355 72819 -536
+ Partials 5925 5907 -18 ☔ View full report in Codecov by Sentry. |
…casting TermSV to ProgramVariable not applicable
* refs/heads/main: Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test repair soundness of assignment2UpdateRules with checked overflows spotless Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design throw an error if choices used in a taclet are not declared correct inRange(..) predicates for overflow check semantics fix creating of branches for overflow checking
* refs/heads/main: Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test repair soundness of assignment2UpdateRules with checked overflows spotless Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design throw an error if choices used in a taclet are not declared correct inRange(..) predicates for overflow check semantics fix creating of branches for overflow checking
* main: (77 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR KeYProject#3436 made casting TermSV to ProgramVariable not applicable spotlessing ... making RuleCommand work if already fully instantiated RuleCommand can now deal with rules that have schema variables for logical variables. Fix loading of taclet proof obligations (issue KeYProject#3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation Code clean up (remove unused method) Fix loading of closed proofs (GUI threw error) Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method ...
* main: (77 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable spotlessing ... making RuleCommand work if already fully instantiated RuleCommand can now deal with rules that have schema variables for logical variables. Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation Code clean up (remove unused method) Fix loading of closed proofs (GUI threw error) Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method ...
* main: (33 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version ...
Related Issue
Intended Change
This PR moves the
ParsableVariable
interface toncore
, makes it no longer anOperator
and renamesAbstractSV
toOperatorSV
as this interface now handles all schema variables that may be operators.It also handles the refactorings necessary to adapt to this change. I.e., changing types where necessary, changing how modality schema vars are matched, and some changes to the term builder.
Also fixes the Github workflow.
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.