Nullness Type System for key.core
#3470
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
wadoon
added
the
🛠 Maintenance
* refs/heads/main: reformat with spotless typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization fix error in the legacy compat part of the proof obligation loading revert some changes of Mattias in the Configuration fix compile error and reformat Configuration: correcting typos, making implementation consistent address reviewers comments reformat witn spotless add fallback and javadoc translate WD obligation loader fix Lemma Proof Obligations migration of existing \proofObligation to the new syntax migration script for \proofObligation spotless + compiler error Renovating PO loader # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
# By Florian Lanzinger (25) and others # Via GitHub (14) and others * main: (69 commits) typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object Test case Fix merge issues reformat files ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ParseExceptionInFile.java # key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Subtype.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptException.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/main/java/de/uka/ilkd/key/util/RecognitionException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/LocatableException.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.util/src/main/java/org/key_project/util/ExtList.java # key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # settings.gradle
# By Florian Lanzinger (25) and others # Via GitHub (14) and others * main: (69 commits) typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object Test case Fix merge issues reformat files ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ParseExceptionInFile.java # key.core/src/main/java/de/uka/ilkd/key/java/PosConvertException.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Subtype.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptException.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/main/java/de/uka/ilkd/key/util/RecognitionException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/LocatableException.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.util/src/main/java/org/key_project/util/ExtList.java # key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # settings.gradle
* refs/heads/main: (26 commits) Fix comment Fix checkstyle workflow Fix checkstyle workflow Fix merge conflicts & spotless Remove todo Spotless Fix? resolving error Move ParsableVariable to ncore Spotless Spotless Rename AbstractSV to OperatorSV Beautified code Fix settings test for SE Spotless fixes Fix taclet prefix check when parsing Fix taclet equality test Fix parsing of variable conditions Fix errors resulting from changing ParseableVar Delete Legacy Matcher and adapt VM matcher for new Modality operator Fix errors after changing ParsableVars ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
* also fix some encoding in recorder/src files
* 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 ...
* refs/heads/weigl/codequality: reenable sonarqube, disable the crappy things
|
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
More nullness type system checks. Now for
key.core.I want first to merge #3399 into KeY to avoid double work.