The Removal of Recoder #3120
Draft
The Removal of Recoder #3120
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
and further fixes, established old work * origin: (793 commits) Add rule that handles casts of compound statements Improve position extraction and try to extract file name from recoder error message Fix failure on empty file Format Slice all taclet proofs Proof slicing: recursive and save files seqPermCountsInt, seqPermForall, seqPermExists Keep auto mode time Re add sorting of ChoiceSettings lost in merge Bump com.miglayout:miglayout-swing from 11.0 to 11.1 Fix exception in proof slicing caused by non sanitized file name Fix error forwarding in TacletProofObligationInput Enable test on windows Fix two tests on Windows degrades optional-tests Fix author name an action for deploying a nightly build fix issue of reviewer Fix comment author and nicer message fix typo in filename ...
|
@jwiesler Sources of key-javaparser are now available via maven. |
* main: Reduce proof dependencies on specific rules (like mergerule) and other high level concepts Use Amazon's Corretto add caching for gradle dependencies Update to Java 21 Runtime for testing Add HelpInfo to more extensions Add help buttons to extension settings # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
wadoon
requested review from
unp1 and
jwiesler
and removed request for
jwiesler
* origin/main: (58 commits) Bump com.diffplug.spotless from 6.23.0 to 6.23.3 Bump ch.qos.logback:logback-classic from 1.4.12 to 1.4.14 Bump com.diffplug.spotless from 6.22.0 to 6.23.0 Bump ch.qos.logback:logback-classic from 1.4.11 to 1.4.12 prepare config using dedicated labels Add a configuration for automatic generation of changelogs by Github Prevent second reading of declarations in KeYUserProblemFile Re-enable check for non-unique taclet names and remove two taclet duplicates Bump org.junit.vintage:junit-vintage-engine from 5.10.0 to 5.10.1 Improve selection consistency in task tree view Undo unrelated change that got checked in. Use selection in task tree view to change chosen problem not mouse events Slight alternative in who selects the first node after loading (should be safer) Remove further unnecessary proof change events Fix (for issue #3347) that node selection gets forgotten when switching between proofs Merge errors CI: make codecov checks non-failing Update .github/pull_request_template.md Update .github/pull_request_template.md Update .github/pull_request_template.md ... # Conflicts: # gradle/wrapper/gradle-wrapper.jar # gradlew
* origin/main: (25 commits) bug fix applying spotless Configurable enabled keys for JML condition evaluation Spotless cleanups Fix selection highlight for OSS node child Remove unnecessary checks for correct change as listener is now registered correctly only for changes of interest Make usage of PropertyChangeListeners working (addendum to previous commit) Reduce number of sequentview updates Remove duplicate update of sequentview USe refactorings from #3369 but preserve non-local filter semantics for proof tree view MainWindow updates sequent view after settings change for pretty printing Minor clean up to slightly simplify complexity of path selection in ProofTreeView Fix problem with closed subtree filter Fix node filter selection display in popup dialoh and some refactoring Restore correct node selection and remove unused fields from GUIProofTreeModel Store ProofTreeViewSettings per proof outside model and restore all settings upon switching Fix update of proof tree in case of filter changes (fixes #3367) applying spotless Bump com.miglayout:miglayout-swing from 11.2 to 11.3 Configurable enabled keys for JML condition evaluation ... # Conflicts: # key.ui/build.gradle
* origin/main: spotless after discussion: all datatypes are free ignore files in */antlr4/gen/* adding example file for natural numbers as ADTs spotless fix merge errors no spaces in displaynames of taclets fix spaces in origin label manually + spotless add an example for case distinction add list example with two proofs solve double declaration of sorts, functions and taclets solve that taclets are unknown better printing revival of ADTs grammar and taclet generation
# By Alexander Weigl (4) and others # Via GitHub * main: Bump com.diffplug.spotless from 6.24.0 to 6.25.0 Bump com.diffplug.spotless from 6.23.3 to 6.24.0 Bump org.slf4j:slf4j-api from 2.0.10 to 2.0.11 Bump org.slf4j:slf4j-api from 2.0.9 to 2.0.10 spotless reformat automatical translate package.html to package-info.java Treat duplicate predicate declarations as error. Fix TestTermParser to avoid multiple parsing of declarations implement the discussion of KaKeY fix passing of warnings # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/package.html # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/package.html # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/package.html # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/package.html # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/package.html # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/package-info.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/package.html # key.core/src/main/java/de/uka/ilkd/key/java/package.html
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java # key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java # settings.gradle
# By Drodt (57) and others # Via GitHub (9) and others * main: (103 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes #1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div Document ncore Fix merge import errors Fix merge errors ... # Conflicts: # key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java # key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleInvariantTranslator.java # key.core/build.gradle # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/TwoStateMethodPredicateSnippet.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Services.java # key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/KeYJavaType.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/Literal.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DLEmbeddedExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/EmptyMapLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/FreeLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java # key.core/src/main/java/de/uka/ilkd/key/ldt/BooleanLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/CharListLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/FreeLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/MapLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/PermissionLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/RealLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java # key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/IProgramVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ArraySort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java # key.core/src/main/java/de/uka/ilkd/key/pp/SelectPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java # key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java # key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRuleBuiltInRuleApp.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstantValue.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MultipleVarDecl.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ObserverEqualityMetaConstruct.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SpecialConstructorCall.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java # key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java # key.core/src/main/java/de/uka/ilkd/key/smt/hierarchy/TypeHierarchy.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ClassAxiomImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ContractAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExpression.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLParameters.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java # key.core/src/test/java/de/uka/ilkd/key/java/visitor/TestDeclarationProgramVariableCollector.java # key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java # key.core/src/test/java/de/uka/ilkd/key/logic/TestTermFactory.java # key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ClasslevelTranslatorTest.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ExpressionTranslatorTest.java # key.ui/build.gradle # key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java
* refs/heads/main: (63 commits) unified naming of operator to "seq_upd". Bump org.ow2.asm:asm from 9.6 to 9.7 reformat after merge fix hashing of set statements and assert statements Typo in message in dlsmt.sh More logging in run all proofs Infrastructure for selection of proof groups Update pull_request_template.md fix check for cvc5 exit in error in dlsmt.sh fix cvc5 fix smt solver downloader script for z3 added references to hard-coded rulesets applying spotless replacing "\seq_length(x)" by "x.length" in set statements in examples fix rap for SetStatmentRule fix rap for JmlAssertRule repair unit tests Update broken link in README.md different highlighting for JML statements ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java # key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/adt/SeqPut.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JmlAssert.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SetStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JmlAssert.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java # key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.java # key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java # key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java # key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java # key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java # key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java # key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java # key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ProofCollection.java # key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java
wadoon
force-pushed
the
weigl/key-javaparser3
branch
from
b60c3e7
to
4e3b31b
Compare
* refs/heads/main: (26 commits) applying spotless Boyer Moore Majority Vote Added test case for the bugfix Fixes a StackOverflow when pretty printing a taclet updating test case descriptions for error reporting cleaning up the test cases enabling KeY test cases common functionality in new superclass improving the feedback of the parsers in KeY Fix keyword for message matching for ParseExceptionTest better error reporting or JML parsing Fix error handling for unknown sorts + test Add error message location for faulty equality exprs Handle null named program variable as error Formatting Disable debugging facility Fix expected error in delayed_error.key Handle InputMismatchExceptions better Formatting Re-instantiate LL fallback ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/JMLParserExceptionTest.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
* refs/heads/main: (40 commits) Fix comment Fix checkstyle workflow reformat with spotless Fix checkstyle workflow Fix merge conflicts & spotless 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 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 ... # Conflicts: # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java # key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java # key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JumpLabelSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LabelSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodSignatureSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProgramVariableSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java # key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ModalOperatorSV.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/IPersistablePO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java # key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java # key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java # key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/TermInstantiation.java # key.core/src/main/java/de/uka/ilkd/key/rule/match/legacy/ElementMatcher.java # key.core/src/main/java/de/uka/ilkd/key/rule/match/legacy/LegacyTacletMatcher.java # key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchModalOperatorSVInstruction.java # key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java # key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/Context.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLResolverManager.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/DefaultLemmaGenerator.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java # key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java # key.core/src/test/java/de/uka/ilkd/key/rule/match/legacy/TestLegacyTacletMatch.java # key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java # keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java
* refs/heads/main: fixing double artifact upload, forbidden in new version Bump the github-actions-deps group with 11 updates update recoder test cases to JUnit 5 removal of JUnit4 deps
* refs/heads/main: (40 commits) 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) Spotless fixes Fixed small typo in merge fixes. fix \locset() with empty args adding test cases for empty seq and locset. allow "\seq()" and "\locset()" in JML Bump the gradle-deps group with 6 updates Bump the github-actions-deps group with 4 updates Code formatting Adapted those qodana suggestions that are not false positives. Removed eclipse project file Also fixes for testcases Applied spotless Towards desired renaming on JML level Again spotless ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/DependencyContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java # key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java # key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractApp.java # key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateHeapAnonUpdate.java # key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java # key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java # key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContract.java # key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/InformationFlowContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContract.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java # key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java # key.core/src/main/java/de/uka/ilkd/key/speclang/OperationContract.java # key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java # key.core/src/main/java/de/uka/ilkd/key/speclang/dl/translation/DLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLInfoExtractor.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassAxiom.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassInv.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLFieldDecl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLInitially.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLRepresents.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSetStatement.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java # key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLMethodResolver.java # key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java # key.core/src/test/resources/testcase/proofBundle/complexBundleGeneration/a/lang/String.key # key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaNonTerminalProgramElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/JavaProgramElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/NonTerminalProgramElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/StatementBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Modifier.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/AbstractIntegerLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/BooleanLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/DoubleLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptyMapLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySeqLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/EmptySetLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/FloatLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/NullLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/RealLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/PackageReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/IForUpdates.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ILoopInit.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabeledStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/TransactionStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/FreeLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/literal/StringLiteral.java # key.core/src/main/java/de/uka/ilkd/key/logic/BoundVariableTools.java # key.core/src/main/java/de/uka/ilkd/key/logic/ProgramElementName.java # key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermEqualsModProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermProperty.java # key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabel.java # key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabel.java # key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java # key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java # key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java # key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java # key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EnumTypeCondition.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeComparisonCondition.java # key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java # key.core/src/main/java/de/uka/ilkd/key/rule/inst/ProgramList.java # key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SeqDefHandler.java # key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java # key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java # key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java # key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java # key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java # key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java # key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java # key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java
# By Mattias Ulbrich (15) and others # Via GitHub (22) and others * origin/main: (37 commits) Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 5 updates formatting Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 8 updates spotless generating ProofTree tooltips lazily, options to disable them completely fix for visual bug with overlapping/unreadable text in color settings Fox copyright year Bump the gradle-deps group with 6 updates improving code for heatmap activation applied spotless Missed nonnullness of map keys. type annotations for test cases repairing a nullness type error some more NonNull annotations Adding a test case for immutable maps. extending the nonnull type system to the immutable maps repairing type annotations in key.util ... it compiles again. repairing heatmap updates for inner nodes ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java # key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java # key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java # key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java # key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java # key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java # key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java
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.
This PR replaces recoder by javaparser, or more precisely by key-javaparser.
The special version has support for
ProofJava,SchemaJavaand Java 17+, all in one grammar.Notes on the grammar can be found in the key-docs
This MR requires a complete overhaul of the KeY-Infrastructure.
Status:
JavaInfofor unused methods and delete themTestProofJavaParserandTestSchemaJavaParser?TestKeYRecoderMapping