The Removal of Recoder #3120

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 ...

reactivate JPKeY...

class can now easier implemented w/o recoder

* origin/main: Fix lockspec test More spammy logging removed Replace nbsp in proof script Minor changes TacletAppIndex lazy delta updates Make builtin rule app index lazy another review change optimize logging statements code review for #3152 missed a line in spotless. spotless and documentation fixing an NPE bug in the error reporting of Recoder2KeY more test cases for exceptional jml cases applying spotless improving the fix for #3149 fixes #3149 fix jacoco for gradle 8 introducing exceptional JML tests add code coverage Bump org.sonarqube from 4.0.0.2929 to 4.1.0.3113 # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java

We have a circle problem, between parseSpecialClasses and type resolution.

* origin/main: adding test case for error messaging remove sonarqube Fix NPE while extracting recoder error position and use existing information better Fix #3156 Fix proof view filter not applied on load

# 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/PositionInfo.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/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/parser/ParserUtil.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.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/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java # key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java

fixed test case: de.uka.ilkd.key.rule.TestMatchTaclet#testPrefixMatching

…l/key-javaparser3

…round

* origin/main: (27 commits) Fix InvariantConfigurator repairs on the KeYParser Check for popup on all needed events Set location of all dialogs relative to parent reformatting remove performance measurments doing performance things and benchmarking Critical changes to KeY parser for more performance Ignore Javadoc warning on logger variables Switch to proof when opening context menu Adjust scroll into view behaviour slightly Add StringUtil.count for future use Scroll sequent view to active formula Fix taclet info for OSS nodes Fix missing highlight of rule app in OSS nodes Fix visual selection indicator in tree Allow selection of sub-nodes in OSS steps Fix slicing bug with weird dependency contracts Restore selection after context menu close config codecov ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.util/src/main/java/org/key_project/util/java/StringUtil.java

# By Arne Keller (15) and others # Via GitHub (14) and others * origin/main: (27 commits) Fix InvariantConfigurator repairs on the KeYParser Check for popup on all needed events Set location of all dialogs relative to parent reformatting remove performance measurments doing performance things and benchmarking Critical changes to KeY parser for more performance Ignore Javadoc warning on logger variables Switch to proof when opening context menu Adjust scroll into view behaviour slightly Add StringUtil.count for future use Scroll sequent view to active formula Fix taclet info for OSS nodes Fix missing highlight of rule app in OSS nodes Fix visual selection indicator in tree Allow selection of sub-nodes in OSS steps Fix slicing bug with weird dependency contracts Restore selection after context menu close config codecov ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.util/src/main/java/org/key_project/util/java/StringUtil.java

Complex cases are missing

# By Arne Keller (19) and others # Via GitHub (9) and others * weigl/sjrt: (36 commits) try to make a matcher translator regression test Remove unnecessary parentheses in JmlLexer Remove dead code Harmonize action and status bar labels All layout actions in one sub-menu Add shortcut key for last layout action Revert "Move layout controls to menu" Document 'minimize interactions' correctly Show SMT solver info in text area Consider divider width in layout Disable rearrangement of toolbar Fix extension panels not showing up sometimes Move layout controls to menu Make exploration extension experimental Spotless Fix broken test case for free conditions on block contracts Move action history button to main toolbar Spotless Don't add inv_free to callee postcondition unless necessary Use correct default for assignable_free in JMLSpecFactory ... # Conflicts: # key.core/build.gradle

# Conflicts: # .github/workflows/tests.yml # build.gradle # key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/KeYRecoderExcHandler.java # key.core/build.gradle # key.core/src/main/java/de/uka/ilkd/key/java/CcatchNonstandardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ConstantExpressionEvaluator.java # key.core/src/main/java/de/uka/ilkd/key/java/Context.java # key.core/src/main/java/de/uka/ilkd/key/java/Dimension.java # key.core/src/main/java/de/uka/ilkd/key/java/Expression.java # key.core/src/main/java/de/uka/ilkd/key/java/JavaReader.java # key.core/src/main/java/de/uka/ilkd/key/java/KeYRecoderMapping.java # key.core/src/main/java/de/uka/ilkd/key/java/LoopInitializer.java # key.core/src/main/java/de/uka/ilkd/key/java/ModelElement.java # 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/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/SchemaJavaReader.java # key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeY.java # key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/Statement.java # key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java # key.core/src/main/java/de/uka/ilkd/key/java/TypeNameTranslator.java # key.core/src/main/java/de/uka/ilkd/key/java/TypeScope.java # key.core/src/main/java/de/uka/ilkd/key/java/abstraction/ProgramModelElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/Comment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/CompilationUnit.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/Declaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ExpressionContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/Import.java # 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/JavaSourceElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/Label.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/NamedModelElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/NamedProgramElement.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/PackageSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ParameterContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ParentIsInterfaceDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/PositionInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramVariableName.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/Reference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ScopeDefiningElement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/SingleLineComment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/SourceData.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/SourceElement.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/StatementContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/VariableScope.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/ClassType.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/ClassTypeContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Constructor.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/DefaultConstructor.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Field.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/abstraction/Member.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Method.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/NullType.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Package.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/PrimitiveType.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Type.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/abstraction/Variable.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchBreakLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchBreakParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchBreakWildcardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchContinueLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchContinueParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchContinueWildcardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchReturnParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/ccatch/CcatchReturnValParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ArrayDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassInitializer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/EnumClassDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Extends.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/FieldDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/FieldSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Implements.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InheritanceSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/LocalVariableDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MemberDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.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/ParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/SuperArrayDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/Throws.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclarationContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/VariableDeclaration.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/declaration/modifier/AnnotationUseSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/Private.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/Protected.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/Public.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/Synchronized.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/VisibilityModifier.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/modifier/Volatile.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/ArrayInitializer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Assignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/ExpressionStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Literal.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/Operator.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/ParenthesizedExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/PassiveExpression.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/CharLiteral.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/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/IntLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/LongLiteral.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/expression/operator/BinaryAnd.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryAndAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryNot.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOperator.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOr.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryOrAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryXOr.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/BinaryXOrAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ComparativeOperator.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Conditional.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/CopyAssignment.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/ast/expression/operator/Divide.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/DivideAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Equals.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ExactInstanceof.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/GreaterOrEquals.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/GreaterThan.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Instanceof.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LessOrEquals.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LessThan.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicalAnd.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicalNot.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/LogicalOr.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Minus.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/MinusAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Modulo.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ModuloAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Negative.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/New.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NewArray.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/NotEquals.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Plus.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/PlusAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Positive.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/PostDecrement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/PostIncrement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/PreDecrement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/PreIncrement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ShiftLeft.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ShiftLeftAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ShiftRight.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/ShiftRightAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/Times.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TimesAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeCast.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/TypeOperator.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnsignedShiftRight.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/operator/UnsignedShiftRightAssignment.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ArrayLengthReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ArrayReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ExecutionContext.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/FieldReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/IExecutionContext.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MetaClassReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodOrConstructorReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/MethodReference.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/reference/PackageReferenceContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchemaTypeReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SpecialConstructorReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SuperConstructorReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SuperReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ThisConstructorReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/ThisReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeRef.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceContainer.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/TypeReferenceImp.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/VariableReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Assert.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchImp.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/BranchStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Break.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Case.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Catch.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/CatchAllStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Ccatch.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Continue.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Default.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Else.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EmptyStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Exec.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ExpressionJumpStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Finally.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/For.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/ForUpdates.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Guard.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/If.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/JavaStatement.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/JumpStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LabelJumpStatement.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/LoopInit.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopScopeBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/LoopStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MergePointStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodBodyStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/MethodFrame.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Return.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Switch.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/SynchronizedBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Then.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Throw.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/ast/statement/Try.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/While.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/ImplicitFieldSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Abstract.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Final.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Ghost.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Model.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Native.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/NoState.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/StrictFp.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Transient.java # key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/TwoState.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/expression/literal/StringLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/Intersect.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/AllFields.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/AllObjects.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqConcat.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqGet.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqIndexOf.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqLength.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqReverse.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqSingleton.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SeqSub.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SetMinus.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/SetUnion.java # key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/adt/Singleton.java # key.core/src/main/java/de/uka/ilkd/key/java/loader/CreateArrayMethodBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaReduxFileCollection.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Bigint.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchAllStatement.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/Ccatch.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakWildcardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueWildcardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchNonstandardParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.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/ClassFileDeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassInitializeMethodBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassPreparationMethodBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstantStringExpressionEvaluator.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ContextStatementBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CreateBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CreateObjectBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/DLEmbeddedExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EnumClassBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EnumClassDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EscapeExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Exec.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/ExecutionContext.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/ExtendedIdentifier.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ghost.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ImplicitFieldAdder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ImplicitIdentifier.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/InstanceAllocationMethodBuilder.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/recoderext/JumpLabelSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYAnnotationUseSpecification.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceNameInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceServiceConfiguration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceSourceFileRepository.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYRecoderExtension.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/LocalClassTransformation.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LoopScopeBlock.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MergePointStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodCallStatement.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/Model.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/NewArrayWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/NewWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/NoState.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ObjectTypeIdentifier.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/PassiveExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/PrepareObjectBuilder.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/ProofCrossReferenceServiceConfiguration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProofJavaProgramFactory.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstruct.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstructExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstructType.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RMethodBodyStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RMethodCallStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Real.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RegisteredEscapeExpression.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/SchemaCrossReferenceServiceConfiguration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaCrossReferenceSourceInfo.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/SourceVisitorExtended.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.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/TransactionStatement.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TwoState.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/URLDataLocation.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/ADTPrefixConstruct.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/AllFields.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/AllObjects.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/EmptyMapLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/EmptySeqLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/EmptySetLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/MethodSignature.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/RangeExpression.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqConcat.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqGet.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqIndexOf.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqLength.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqReverse.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqSingleton.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqSub.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SetMinus.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SetUnion.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Singleton.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/expression/literal/RealLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/ConstructorReference.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/MemberReference.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/MethodName.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/NameReference.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/ReferencePrefix.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/ReferenceSuffix.java # key.core/src/main/java/de/uka/ilkd/key/java/reference/TypeReferenceInfix.java # key.core/src/main/java/de/uka/ilkd/key/java/statement/Branch.java # key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java # key.core/src/main/java/de/uka/ilkd/key/java/statement/IGuard.java # key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java # key.core/src/main/java/de/uka/ilkd/key/parser/ParserUtil.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/TrivialFileRepo.java # key.core/src/main/java/de/uka/ilkd/key/smt/RuleAppSMT.java # key.core/src/main/java/de/uka/ilkd/key/util/ReferenceLister.java # key.core/src/main/java/de/uka/ilkd/key/util/SpecDataLocation.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java # key.core/src/test/java/de/uka/ilkd/key/java/TestKeYRecoderMapping.java # key.core/src/test/java/de/uka/ilkd/key/java/TestPositions.java # key.core/src/test/java/de/uka/ilkd/key/java/TestRecoder2KeY.java # key.core/src/test/java/de/uka/ilkd/key/java/recoderext/TestEnumClassDeclaration.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestParallelParsing.java # key.core/src/test/java/de/uka/ilkd/key/parser/proofjava/TestProofJavaParser.java # key.core/src/test/resources/logback.xml # key.ui/build.gradle # key.ui/src/main/java/de/uka/ilkd/key/core/Main.java # key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java # key.ui/src/test/resources/logback.xml # key.util/src/main/java/org/key_project/util/java/SwingUtil.java # recoder/src/main/java/recoder/AbstractService.java # recoder/src/main/java/recoder/CrossReferenceServiceConfiguration.java # recoder/src/main/java/recoder/DefaultServiceConfiguration.java # recoder/src/main/java/recoder/ModelElement.java # recoder/src/main/java/recoder/ModelException.java # recoder/src/main/java/recoder/NamedModelElement.java # recoder/src/main/java/recoder/ParserException.java # recoder/src/main/java/recoder/ProgramFactory.java # recoder/src/main/java/recoder/Service.java # recoder/src/main/java/recoder/ServiceConfiguration.java # recoder/src/main/java/recoder/abstraction/ArrayType.java # recoder/src/main/java/recoder/abstraction/ClassType.java # recoder/src/main/java/recoder/abstraction/ClassTypeContainer.java # recoder/src/main/java/recoder/abstraction/Constructor.java # recoder/src/main/java/recoder/abstraction/DefaultConstructor.java # recoder/src/main/java/recoder/abstraction/Field.java # recoder/src/main/java/recoder/abstraction/Member.java # recoder/src/main/java/recoder/abstraction/Method.java # recoder/src/main/java/recoder/abstraction/NullType.java # recoder/src/main/java/recoder/abstraction/Package.java # recoder/src/main/java/recoder/abstraction/PrimitiveType.java # recoder/src/main/java/recoder/abstraction/ProgramModelElement.java # recoder/src/main/java/recoder/abstraction/Type.java # recoder/src/main/java/recoder/abstraction/Variable.java # recoder/src/main/java/recoder/bytecode/AccessFlags.java # recoder/src/main/java/recoder/bytecode/ByteCodeElement.java # recoder/src/main/java/recoder/bytecode/ByteCodeFormatException.java # recoder/src/main/java/recoder/bytecode/ByteCodeParser.java # recoder/src/main/java/recoder/bytecode/ClassFile.java # recoder/src/main/java/recoder/bytecode/ConstructorInfo.java # recoder/src/main/java/recoder/bytecode/FieldInfo.java # recoder/src/main/java/recoder/bytecode/MemberInfo.java # recoder/src/main/java/recoder/bytecode/MethodInfo.java # recoder/src/main/java/recoder/convenience/ASTIterator.java # recoder/src/main/java/recoder/convenience/ASTIteratorAdapter.java # recoder/src/main/java/recoder/convenience/ASTIteratorListener.java # recoder/src/main/java/recoder/convenience/AbstractTreeWalker.java # recoder/src/main/java/recoder/convenience/CustomTreeWalker.java # recoder/src/main/java/recoder/convenience/ForestWalker.java # recoder/src/main/java/recoder/convenience/Format.java # recoder/src/main/java/recoder/convenience/Formats.java # recoder/src/main/java/recoder/convenience/ModelElementFilter.java # recoder/src/main/java/recoder/convenience/NameGenerator.java # recoder/src/main/java/recoder/convenience/NamedModelElementFilter.java # recoder/src/main/java/recoder/convenience/Naming.java # recoder/src/main/java/recoder/convenience/ProgramElementWalker.java # recoder/src/main/java/recoder/convenience/TaggedComment.java # recoder/src/main/java/recoder/convenience/TreeWalker.java # recoder/src/main/java/recoder/io/ArchiveDataLocation.java # recoder/src/main/java/recoder/io/ClassFileRepository.java # recoder/src/main/java/recoder/io/DataFileLocation.java # recoder/src/main/java/recoder/io/DataLocation.java # recoder/src/main/java/recoder/io/DefaultClassFileRepository.java # recoder/src/main/java/recoder/io/DefaultProjectFileIO.java # recoder/src/main/java/recoder/io/DefaultSourceFileRepository.java # recoder/src/main/java/recoder/io/PathList.java # recoder/src/main/java/recoder/io/ProjectFileIO.java # recoder/src/main/java/recoder/io/ProjectSettings.java # recoder/src/main/java/recoder/io/PropertyNames.java # recoder/src/main/java/recoder/io/SourceFileRepository.java # recoder/src/main/java/recoder/java/Comment.java # recoder/src/main/java/recoder/java/CompilationUnit.java # recoder/src/main/java/recoder/java/Declaration.java # recoder/src/main/java/recoder/java/DocComment.java # recoder/src/main/java/recoder/java/Expression.java # recoder/src/main/java/recoder/java/ExpressionContainer.java # recoder/src/main/java/recoder/java/Identifier.java # recoder/src/main/java/recoder/java/Import.java # recoder/src/main/java/recoder/java/JavaNonTerminalProgramElement.java # recoder/src/main/java/recoder/java/JavaProgramElement.java # recoder/src/main/java/recoder/java/JavaProgramFactory.java # recoder/src/main/java/recoder/java/JavaSourceElement.java # recoder/src/main/java/recoder/java/LoopInitializer.java # recoder/src/main/java/recoder/java/NamedProgramElement.java # recoder/src/main/java/recoder/java/NonTerminalProgramElement.java # recoder/src/main/java/recoder/java/PackageSpecification.java # recoder/src/main/java/recoder/java/ParameterContainer.java # recoder/src/main/java/recoder/java/PrettyPrinter.java # recoder/src/main/java/recoder/java/PrettyPrintingException.java # recoder/src/main/java/recoder/java/ProgramElement.java # recoder/src/main/java/recoder/java/Reference.java # recoder/src/main/java/recoder/java/ScopeDefiningElement.java # recoder/src/main/java/recoder/java/SingleLineComment.java # recoder/src/main/java/recoder/java/SourceElement.java # recoder/src/main/java/recoder/java/SourceVisitor.java # recoder/src/main/java/recoder/java/Statement.java # recoder/src/main/java/recoder/java/StatementBlock.java # recoder/src/main/java/recoder/java/StatementContainer.java # recoder/src/main/java/recoder/java/TerminalProgramElement.java # recoder/src/main/java/recoder/java/TypeScope.java # recoder/src/main/java/recoder/java/VariableScope.java # recoder/src/main/java/recoder/java/declaration/ClassDeclaration.java # recoder/src/main/java/recoder/java/declaration/ClassInitializer.java # recoder/src/main/java/recoder/java/declaration/ConstructorDeclaration.java # recoder/src/main/java/recoder/java/declaration/Extends.java # recoder/src/main/java/recoder/java/declaration/FieldDeclaration.java # recoder/src/main/java/recoder/java/declaration/FieldSpecification.java # recoder/src/main/java/recoder/java/declaration/Implements.java # recoder/src/main/java/recoder/java/declaration/InheritanceSpecification.java # recoder/src/main/java/recoder/java/declaration/InterfaceDeclaration.java # recoder/src/main/java/recoder/java/declaration/JavaDeclaration.java # recoder/src/main/java/recoder/java/declaration/LocalVariableDeclaration.java # recoder/src/main/java/recoder/java/declaration/MemberDeclaration.java # recoder/src/main/java/recoder/java/declaration/MethodDeclaration.java # recoder/src/main/java/recoder/java/declaration/Modifier.java # recoder/src/main/java/recoder/java/declaration/ParameterDeclaration.java # recoder/src/main/java/recoder/java/declaration/Throws.java # recoder/src/main/java/recoder/java/declaration/TypeDeclaration.java # recoder/src/main/java/recoder/java/declaration/TypeDeclarationContainer.java # recoder/src/main/java/recoder/java/declaration/VariableDeclaration.java # recoder/src/main/java/recoder/java/declaration/VariableSpecification.java # recoder/src/main/java/recoder/java/declaration/modifier/Abstract.java # recoder/src/main/java/recoder/java/declaration/modifier/Final.java # recoder/src/main/java/recoder/java/declaration/modifier/Native.java # recoder/src/main/java/recoder/java/declaration/modifier/Private.java # recoder/src/main/java/recoder/java/declaration/modifier/Protected.java # recoder/src/main/java/recoder/java/declaration/modifier/Public.java # recoder/src/main/java/recoder/java/declaration/modifier/Static.java # recoder/src/main/java/recoder/java/declaration/modifier/StrictFp.java # recoder/src/main/java/recoder/java/declaration/modifier/Synchronized.java # recoder/src/main/java/recoder/java/declaration/modifier/Transient.java # recoder/src/main/java/recoder/java/declaration/modifier/VisibilityModifier.java # recoder/src/main/java/recoder/java/declaration/modifier/Volatile.java # recoder/src/main/java/recoder/java/expression/ArrayInitializer.java # recoder/src/main/java/recoder/java/expression/Assignment.java # recoder/src/main/java/recoder/java/expression/ExpressionStatement.java # recoder/src/main/java/recoder/java/expression/Literal.java # recoder/src/main/java/recoder/java/expression/Operator.java # recoder/src/main/java/recoder/java/expression/ParenthesizedExpression.java # recoder/src/main/java/recoder/java/expression/literal/BooleanLiteral.java # recoder/src/main/java/recoder/java/expression/literal/CharLiteral.java # recoder/src/main/java/recoder/java/expression/literal/DoubleLiteral.java # recoder/src/main/java/recoder/java/expression/literal/FloatLiteral.java # recoder/src/main/java/recoder/java/expression/literal/IntLiteral.java # recoder/src/main/java/recoder/java/expression/literal/LongLiteral.java # recoder/src/main/java/recoder/java/expression/literal/NullLiteral.java # recoder/src/main/java/recoder/java/expression/literal/StringLiteral.java # recoder/src/main/java/recoder/java/expression/operator/BinaryAnd.java # recoder/src/main/java/recoder/java/expression/operator/BinaryAndAssignment.java # recoder/src/main/java/recoder/java/expression/operator/BinaryNot.java # recoder/src/main/java/recoder/java/expression/operator/BinaryOr.java # recoder/src/main/java/recoder/java/expression/operator/BinaryOrAssignment.java # recoder/src/main/java/recoder/java/expression/operator/BinaryXOr.java # recoder/src/main/java/recoder/java/expression/operator/BinaryXOrAssignment.java # recoder/src/main/java/recoder/java/expression/operator/ComparativeOperator.java # recoder/src/main/java/recoder/java/expression/operator/Conditional.java # recoder/src/main/java/recoder/java/expression/operator/CopyAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Divide.java # recoder/src/main/java/recoder/java/expression/operator/DivideAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Equals.java # recoder/src/main/java/recoder/java/expression/operator/GreaterOrEquals.java # recoder/src/main/java/recoder/java/expression/operator/GreaterThan.java # recoder/src/main/java/recoder/java/expression/operator/Instanceof.java # recoder/src/main/java/recoder/java/expression/operator/LessOrEquals.java # recoder/src/main/java/recoder/java/expression/operator/LessThan.java # recoder/src/main/java/recoder/java/expression/operator/LogicalAnd.java # recoder/src/main/java/recoder/java/expression/operator/LogicalNot.java # recoder/src/main/java/recoder/java/expression/operator/LogicalOr.java # recoder/src/main/java/recoder/java/expression/operator/Minus.java # recoder/src/main/java/recoder/java/expression/operator/MinusAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Modulo.java # recoder/src/main/java/recoder/java/expression/operator/ModuloAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Negative.java # recoder/src/main/java/recoder/java/expression/operator/New.java # recoder/src/main/java/recoder/java/expression/operator/NewArray.java # recoder/src/main/java/recoder/java/expression/operator/NotEquals.java # recoder/src/main/java/recoder/java/expression/operator/Plus.java # recoder/src/main/java/recoder/java/expression/operator/PlusAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Positive.java # recoder/src/main/java/recoder/java/expression/operator/PostDecrement.java # recoder/src/main/java/recoder/java/expression/operator/PostIncrement.java # recoder/src/main/java/recoder/java/expression/operator/PreDecrement.java # recoder/src/main/java/recoder/java/expression/operator/PreIncrement.java # recoder/src/main/java/recoder/java/expression/operator/ShiftLeft.java # recoder/src/main/java/recoder/java/expression/operator/ShiftLeftAssignment.java # recoder/src/main/java/recoder/java/expression/operator/ShiftRight.java # recoder/src/main/java/recoder/java/expression/operator/ShiftRightAssignment.java # recoder/src/main/java/recoder/java/expression/operator/Times.java # recoder/src/main/java/recoder/java/expression/operator/TimesAssignment.java # recoder/src/main/java/recoder/java/expression/operator/TypeCast.java # recoder/src/main/java/recoder/java/expression/operator/TypeOperator.java # recoder/src/main/java/recoder/java/expression/operator/UnsignedShiftRight.java # recoder/src/main/java/recoder/java/expression/operator/UnsignedShiftRightAssignment.java # recoder/src/main/java/recoder/java/reference/ArrayLengthReference.java # recoder/src/main/java/recoder/java/reference/ArrayReference.java # recoder/src/main/java/recoder/java/reference/ConstructorReference.java # recoder/src/main/java/recoder/java/reference/FieldReference.java # recoder/src/main/java/recoder/java/reference/MemberReference.java # recoder/src/main/java/recoder/java/reference/MetaClassReference.java # recoder/src/main/java/recoder/java/reference/MethodReference.java # recoder/src/main/java/recoder/java/reference/NameReference.java # recoder/src/main/java/recoder/java/reference/PackageReference.java # recoder/src/main/java/recoder/java/reference/PackageReferenceContainer.java # recoder/src/main/java/recoder/java/reference/ReferencePrefix.java # recoder/src/main/java/recoder/java/reference/ReferenceSuffix.java # recoder/src/main/java/recoder/java/reference/SpecialConstructorReference.java # recoder/src/main/java/recoder/java/reference/SuperConstructorReference.java # recoder/src/main/java/recoder/java/reference/SuperReference.java # recoder/src/main/java/recoder/java/reference/ThisConstructorReference.java # recoder/src/main/java/recoder/java/reference/ThisReference.java # recoder/src/main/java/recoder/java/reference/TypeReference.java # recoder/src/main/java/recoder/java/reference/TypeReferenceContainer.java # recoder/src/main/java/recoder/java/reference/TypeReferenceInfix.java # recoder/src/main/java/recoder/java/reference/UncollatedReferenceQualifier.java # recoder/src/main/java/recoder/java/reference/VariableReference.java # recoder/src/main/java/recoder/java/statement/Assert.java # recoder/src/main/java/recoder/java/statement/Branch.java # recoder/src/main/java/recoder/java/statement/BranchStatement.java # recoder/src/main/java/recoder/java/statement/Break.java # recoder/src/main/java/recoder/java/statement/Case.java # recoder/src/main/java/recoder/java/statement/Catch.java # recoder/src/main/java/recoder/java/statement/Continue.java # recoder/src/main/java/recoder/java/statement/Default.java # recoder/src/main/java/recoder/java/statement/Do.java # recoder/src/main/java/recoder/java/statement/Else.java # recoder/src/main/java/recoder/java/statement/EmptyStatement.java # recoder/src/main/java/recoder/java/statement/ExpressionJumpStatement.java # recoder/src/main/java/recoder/java/statement/Finally.java # recoder/src/main/java/recoder/java/statement/For.java # recoder/src/main/java/recoder/java/statement/If.java # recoder/src/main/java/recoder/java/statement/JavaStatement.java # recoder/src/main/java/recoder/java/statement/JumpStatement.java # recoder/src/main/java/recoder/java/statement/LabelJumpStatement.java # recoder/src/main/java/recoder/java/statement/LabeledStatement.java # recoder/src/main/java/recoder/java/statement/LoopStatement.java # recoder/src/main/java/recoder/java/statement/Return.java # recoder/src/main/java/recoder/java/statement/Switch.java # recoder/src/main/java/recoder/java/statement/SynchronizedBlock.java # recoder/src/main/java/recoder/java/statement/Then.java # recoder/src/main/java/recoder/java/statement/Throw.java # recoder/src/main/java/recoder/java/statement/Try.java # recoder/src/main/java/recoder/java/statement/While.java # recoder/src/main/java/recoder/kit/CommentKit.java # recoder/src/main/java/recoder/kit/Conflict.java # recoder/src/main/java/recoder/kit/DifferentReturnTypeOverwrite.java # recoder/src/main/java/recoder/kit/Equivalence.java # recoder/src/main/java/recoder/kit/ExpressionKit.java # recoder/src/main/java/recoder/kit/FinalOverwrite.java # recoder/src/main/java/recoder/kit/Identity.java # recoder/src/main/java/recoder/kit/IllegalInterfaceMember.java # recoder/src/main/java/recoder/kit/IllegalName.java # recoder/src/main/java/recoder/kit/MethodKit.java # recoder/src/main/java/recoder/kit/MiscKit.java # recoder/src/main/java/recoder/kit/MissingSources.java # recoder/src/main/java/recoder/kit/MissingTypeDeclarations.java # recoder/src/main/java/recoder/kit/ModifierKit.java # recoder/src/main/java/recoder/kit/MorePrivateOverwrite.java # recoder/src/main/java/recoder/kit/NameClashException.java # recoder/src/main/java/recoder/kit/NameConflict.java # recoder/src/main/java/recoder/kit/NameGenerator.java # recoder/src/main/java/recoder/kit/NoProblem.java # recoder/src/main/java/recoder/kit/NonStaticOverwrite.java # recoder/src/main/java/recoder/kit/PackageKit.java # recoder/src/main/java/recoder/kit/Problem.java # recoder/src/main/java/recoder/kit/ProblemReport.java # recoder/src/main/java/recoder/kit/StatementKit.java # recoder/src/main/java/recoder/kit/Transformation.java # recoder/src/main/java/recoder/kit/TwoPassTransformation.java # recoder/src/main/java/recoder/kit/TypeKit.java # recoder/src/main/java/recoder/kit/UncoveredExceptionsOverwrite.java # recoder/src/main/java/recoder/kit/UnitKit.java # recoder/src/main/java/recoder/kit/VariableKit.java # recoder/src/main/java/recoder/kit/pattern/DesignPattern.java # recoder/src/main/java/recoder/kit/pattern/Factory.java # recoder/src/main/java/recoder/kit/pattern/FactoryMethod.java # recoder/src/main/java/recoder/kit/pattern/InconsistentPatternException.java # recoder/src/main/java/recoder/kit/pattern/Property.java # recoder/src/main/java/recoder/kit/transformation/AppendMember.java # recoder/src/main/java/recoder/kit/transformation/Modify.java # recoder/src/main/java/recoder/kit/transformation/PrepareStatementList.java # recoder/src/main/java/recoder/kit/transformation/PrependExpressionWithStatements.java # recoder/src/main/java/recoder/kit/transformation/RenameMethod.java # recoder/src/main/java/recoder/kit/transformation/RenamePackage.java # recoder/src/main/java/recoder/kit/transformation/RenameType.java # recoder/src/main/java/recoder/kit/transformation/RenameVariable.java # recoder/src/main/java/recoder/kit/transformation/ShiftPreceedingStatementExpressions.java # recoder/src/main/java/recoder/parser/ASCII_UCodeESC_CharStream.java # recoder/src/main/java/recoder/service/AmbiguousDeclarationException.java # recoder/src/main/java/recoder/service/AmbiguousImportException.java # recoder/src/main/java/recoder/service/AmbiguousReferenceException.java # recoder/src/main/java/recoder/service/AmbiguousStaticFieldImportException.java # recoder/src/main/java/recoder/service/AttachChange.java # recoder/src/main/java/recoder/service/ByteCodeInfo.java # recoder/src/main/java/recoder/service/ChangeHistory.java # recoder/src/main/java/recoder/service/ChangeHistoryEvent.java # recoder/src/main/java/recoder/service/ChangeHistoryListener.java # recoder/src/main/java/recoder/service/ClassTypeTopSort.java # recoder/src/main/java/recoder/service/ConstantEvaluator.java # recoder/src/main/java/recoder/service/CrossReferenceSourceInfo.java # recoder/src/main/java/recoder/service/CyclicInheritanceException.java # recoder/src/main/java/recoder/service/DefaultByteCodeInfo.java # recoder/src/main/java/recoder/service/DefaultConstantEvaluator.java # recoder/src/main/java/recoder/service/DefaultCrossReferenceSourceInfo.java # recoder/src/main/java/recoder/service/DefaultImplicitElementInfo.java # recoder/src/main/java/recoder/service/DefaultNameInfo.java # recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java # recoder/src/main/java/recoder/service/DefaultSourceInfo.java # recoder/src/main/java/recoder/service/DetachChange.java # recoder/src/main/java/recoder/service/ErrorHandler.java # recoder/src/main/java/recoder/service/IllegalChangeReportException.java # recoder/src/main/java/recoder/service/ImplicitElementInfo.java # recoder/src/main/java/recoder/service/MissingClassFileException.java # recoder/src/main/java/recoder/service/ModelUpdateListener.java # recoder/src/main/java/recoder/service/NameInfo.java # recoder/src/main/java/recoder/service/NoSuchTransformationException.java # recoder/src/main/java/recoder/service/ProgramModelInfo.java # recoder/src/main/java/recoder/service/SourceInfo.java # recoder/src/main/java/recoder/service/TreeChange.java # recoder/src/main/java/recoder/service/TypeImportException.java # recoder/src/main/java/recoder/service/TypingException.java # recoder/src/main/java/recoder/service/UnresolvedReferenceException.java # recoder/src/main/java/recoder/util/AbstractIndex.java # recoder/src/main/java/recoder/util/CommandLineProgram.java # recoder/src/main/java/recoder/util/Debug.java # recoder/src/main/java/recoder/util/Equality.java # recoder/src/main/java/recoder/util/FileCollector.java # recoder/src/main/java/recoder/util/FileUtils.java # recoder/src/main/java/recoder/util/HashCode.java # recoder/src/main/java/recoder/util/IdentityIndex.java # recoder/src/main/java/recoder/util/IllegalOptionValueException.java # recoder/src/main/java/recoder/util/Index.java # recoder/src/main/java/recoder/util/Marker.java # recoder/src/main/java/recoder/util/MissingArgumentException.java # recoder/src/main/java/recoder/util/MissingOptionValueException.java # recoder/src/main/java/recoder/util/NaturalIndex.java # recoder/src/main/java/recoder/util/ObjectIDAssignment.java # recoder/src/main/java/recoder/util/OptionException.java # recoder/src/main/java/recoder/util/OptionManager.java # recoder/src/main/java/recoder/util/OptionMultiplicityException.java # recoder/src/main/java/recoder/util/Order.java # recoder/src/main/java/recoder/util/Queue.java # recoder/src/main/java/recoder/util/Sorting.java # recoder/src/main/java/recoder/util/StringUtils.java # recoder/src/main/java/recoder/util/UnknownOptionException.java # recoder/src/main/java/recoder/util/Worklist.java # recoder/src/test/java/recoder/testsuite/basic/BasicTestsSuite.java # settings.gradle

* main: increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting Spotless and fix rebase Some additional minor fixes and spotlessApply Update `collect(Collectors.toList())` to `toList()` Introduction of record classes where it seems useful. Refactor: Introduce a pattern variable were possible. Translate large string concatenations into raw string literal (text blocks)

and some bug fixes # By Alexander Weigl (5) and Wolfram Pfeifer (2) # Via GitHub (1) and Wolfram Pfeifer (1) * main: increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting Spotless and fix rebase Some additional minor fixes and spotlessApply Update `collect(Collectors.toList())` to `toList()` Introduction of record classes where it seems useful. Refactor: Introduce a pattern variable were possible. Translate large string concatenations into raw string literal (text blocks) # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.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/Recoder2KeYTypeConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassInitializeMethodBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassPreparationMethodBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EnumClassBuilder.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/PrepareObjectBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProofJavaProgramFactory.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/URLDataLocation.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java # key.core/src/main/java/de/uka/ilkd/key/util/ReferenceLister.java # key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java # key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java # key.core/src/test/java/de/uka/ilkd/key/java/TestPositions.java # key.core/src/test/java/de/uka/ilkd/key/java/TestRecoder2KeY.java # key.core/src/test/java/de/uka/ilkd/key/logic/TestClashFreeSubst.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java # key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java # keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java # keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/dependency/ContractAppCollector.java

* origin/main: Bump com.miglayout:miglayout-swing from 11.1 to 11.2 renaming of some fields/methods, since problems can not only contain terms Bump org.ow2.asm:asm from 9.5 to 9.6 Bump com.diffplug.spotless from 6.21.0 to 6.22.0 updating README.md fix bug allow problems to be sequents Update gradle build action to most recent ones v2 reformat further refactorings further refactorings further code refactorings updating GenerateUnitTests to Java 17+ Bump org.antlr:antlr4 from 4.13.0 to 4.13.1 Fix dependency issue in SMT translation Bump com.diffplug.spotless from 6.20.0 to 6.21.0 Bump org.slf4j:slf4j-api from 2.0.7 to 2.0.9 Optimize SMT apply performance Stop automode or exit on SIGINT # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/expression/literal/CharLiteral.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.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/RecoderModelTransformer.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/Intersect.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/DeclarationProgramVariableCollector.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ProblemFinder.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/KeYUserProblemFile.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java # key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java # key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java

* main: (41 commits) Update .github/workflows/nightlydeploy.yml Update nightlydeploy.yml spotless warning Fix wrong quicksave failed warning Update build.gradle Remove AutoClosable on KeYEnvironment Fix proof tree behaviour when toggling goals Fix branch selection in caching Fix rare edge case in dependency analyzer Fix gradle detection of git branch Kill SMT solvers properly on timeout Fix unit test Fix environments not disposed in tests Keep strategy info visible after applying Disable stop button once it is used Fully disable origin tracking if it is disabled Proof macro: record statistics correctly Statistics constructor from node list spotless: adding a space bugfix: KeY files with errors cannot be edited. ... # Conflicts: # key.core.symbolic_execution/src/test/resources/testcase/set/allNodeTypesTest/test/AllNodeTypesTest_VerificationProfile.proof # key.core/src/main/java/de/uka/ilkd/key/java/Services.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java # key.ui/examples/standard_key/pred_log/count.key.proof # key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java # key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java

* main: (30 commits) Revert lazy term index updates Push gradle version and update build.gradle for future compatibility to the upcoming gradle 9.x series Simplify string formatting following a suggestion Alexander Weigl Add some more test cases for Strings#isJMLComment Replaced some additional string concatenations Provide additional String formating utility method to reduce code duplication Add missing setRunOnlyOn(...) method to enable running only defined groups of test proofs spotless checks Improve readability of emptyness checks Fix some equals/hashCode issues Fix erroneous instanceof which checked for an incompatible type Remove unused imports Avoid potential NPEs and replace usage of deprecated method Minor clean up Avoid potential NullPointerExceptions Fix calls to StringBuilder equals method which only checks for object identity not for content equality Fix errorneous equals implementation - equals compared this.getClass with this.getClass and not with other.getClass - equals on incompatible types Simplify empty String checks (semi automatic) Remove unused code Stricter enforcement of Java AST immutability ... # Conflicts: # gradle/wrapper/gradle-wrapper.properties # key.core/src/main/java/de/uka/ilkd/key/java/Services.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/FieldReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/reference/SchematicFieldReference.java # key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Ccatch.java # key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelOperationsInterpreter.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/LDTInput.java # key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt

* main: fix compile error which occurs on auto rebasing Small cleanup Slightl increase of required number of steps Fix Nullpointer exception if all proofs are closed Remove any dependencies from proof object to origin labels and to SourceView related initialization Comment Services method related to OriginTermLabel factory Make TermLabelManager independent of specific TermLabel instances Update toggle action for origin tracking Pass correct OriginTermLabelFactory to copies of services Fix an accidental committed debug hack Change to per environment. spotless fixes Make origin activation proof specific Allow origin labels to be switched off completely # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/java/Services.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java

* main: replace JSR305 annotations with JSpecify Added forgotten test for getFirst Remaned methods to better reflect their intention Fix bug in refectoring retrieval Add comments and test for LabelCollection Clean up spotless changes and some typo corrections clean up Some additional optimisations Optimized TermLabel processing using a linked hash set for common operations instead of a list Refactorings container can use mutable linked sets Optimize offline dependency tracker and add tests IdentityHashSet collection class Contract creation should use correct OriginLabel settings Minor polishing Simplify TermLabelManager API Always bounds check formula nr in sequent Fix tracking of dynamically added rules Proof Slicing: make dependency tracking optional Codestyle # 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/PositionInfo.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java # key.core/src/main/java/de/uka/ilkd/key/ldt/IntegerLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/LocSetLDT.java # key.core/src/main/java/de/uka/ilkd/key/ldt/SeqLDT.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/parser/ParserException.java # key.core/src/main/java/de/uka/ilkd/key/proof/SVInstantiationExceptionWithPosition.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/FileRuleSource.java # key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java # key.core/src/main/java/de/uka/ilkd/key/rule/ObserverToUpdateRule.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/translation/Context.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/SLTranslationException.java # key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.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/HasLocation.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/LocatableException.java # key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParserHeap.java # key.ui/src/main/java/de/uka/ilkd/key/gui/PositionedIssueString.java

* remove JSR305 types

* origin/main: (73 commits) Use pattern matching to avoid cast Change default notification setting to unfocused Renaming from reviewer suggestion (got lost when splitting the PR) Minor cleanup Prevent possible NullPointerException. Cleanup. Remove last usage of the legacy matcher. Check only new terms for well-typedness Move static metavariable cache to service caches Minor cleanup incl. spotless changes Use array of assumes instantiations Preparation for parallel prover engine - make Strategies stateless by introducing a specific explicit state object for TermBuffers and the Backtracking Manager This will allow strategies to execute in parallel Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java Some cleanup and proper switching to automode Avoid access of non-private field in synchronized context Pruning a closed proof (and reopening it) did not update the proof status in the task tree and also did not select any node/goal. Minor clean up Ensure correct enabling and disabling of SequentView updates Proper use of automode when realizing cached branches Ensure GUI update during problem loading to be done in the EventQueue ... # Conflicts: # build.gradle # key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java # key.core/src/main/java/de/uka/ilkd/key/control/UserInterfaceControl.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/recoderext/Ccatch.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchBreakLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchContinueLabelParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchReturnValParameterDeclaration.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java # key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Exec.java # key.core/src/main/java/de/uka/ilkd/key/java/visitor/ContainsStatementVisitor.java # key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java # key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java # key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java

* 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

* 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

* 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

Commits on Apr 17, 2023

test all redux classes for parsability

wadoon committed Apr 17, 2023

Configuration menu

View commit details

Copy full SHA for b1f53db

Browse repository at this point

Copy the full SHA

b1f53db View commit details

Browse the repository at this point in the history

Commits on May 4, 2023

Pretty printing of compilation units

jwiesler committed May 4, 2023

Configuration menu

View commit details

Copy full SHA for 385bbee

Browse repository at this point

Copy the full SHA

385bbee View commit details

Browse the repository at this point in the history

Commits on May 10, 2023

Unused code

jwiesler committed May 10, 2023

Configuration menu

View commit details

Copy full SHA for 87c2185

Browse repository at this point

Copy the full SHA

87c2185 View commit details

Browse the repository at this point in the history

Commits on May 15, 2023

Fix some references

jwiesler committed May 15, 2023

Configuration menu

View commit details

Copy full SHA for 42c5f75

Browse repository at this point

Copy the full SHA

42c5f75 View commit details

Browse the repository at this point in the history

Commits on May 16, 2023

Replace File with Path

jwiesler committed May 16, 2023

Configuration menu

View commit details

Copy full SHA for 77f3e02

Browse repository at this point

Copy the full SHA

77f3e02 View commit details

Browse the repository at this point in the history

Commits on May 20, 2023

make key compilable again

wadoon committed May 20, 2023

Configuration menu

View commit details

Copy full SHA for 3266e0b

Browse repository at this point

Copy the full SHA

3266e0b View commit details

Browse the repository at this point in the history

Commits on May 26, 2023

Comment out test rules

jwiesler committed May 26, 2023

Configuration menu

View commit details

Copy full SHA for d76652c

Browse repository at this point

Copy the full SHA

d76652c View commit details

Browse the repository at this point in the history

Commits on May 27, 2023

Fix some schema variable usages

jwiesler committed May 27, 2023

Configuration menu

View commit details

Copy full SHA for 2e368d7

Browse repository at this point

Copy the full SHA

2e368d7 View commit details

Browse the repository at this point in the history

Commits on Jul 18, 2023

Field access

jwiesler committed Jul 18, 2023

Configuration menu

View commit details

Copy full SHA for 150a51c

Browse repository at this point

Copy the full SHA

150a51c View commit details

Browse the repository at this point in the history

Commits on Aug 22, 2023

fix merge compilation errors

wadoon committed Aug 22, 2023

Configuration menu

View commit details

Copy full SHA for d0ffa83

Browse repository at this point

Copy the full SHA

d0ffa83 View commit details

Browse the repository at this point in the history

Commits on Apr 7, 2024

fix merge errors

wadoon committed Apr 7, 2024

Configuration menu

View commit details

Copy full SHA for 39684ce

Browse repository at this point

Copy the full SHA

39684ce View commit details

Browse the repository at this point in the history

Commits on Jul 20, 2024

Remove Ctrl+C handling, see #3456

wadoon committed Jul 20, 2024

Configuration menu

View commit details

Copy full SHA for 37255eb

Browse repository at this point

Copy the full SHA

37255eb View commit details

Browse the repository at this point in the history

The Removal of Recoder #3120

Are you sure you want to change the base?

The Removal of Recoder #3120

Commits on Apr 15, 2023

Commits on Apr 16, 2023

Commits on Apr 17, 2023

Commits on Apr 18, 2023

Commits on Apr 20, 2023

Commits on Apr 27, 2023

Commits on May 2, 2023

Commits on May 3, 2023

Commits on May 4, 2023

Commits on May 9, 2023

Commits on May 10, 2023

Commits on May 11, 2023

Commits on May 15, 2023

Commits on May 16, 2023

Commits on May 19, 2023

Commits on May 20, 2023

Commits on May 22, 2023

Commits on May 23, 2023

Commits on May 24, 2023

Commits on May 26, 2023

Commits on May 27, 2023

Commits on May 28, 2023

Commits on Jun 2, 2023

Commits on Jun 3, 2023

Commits on Jun 7, 2023

Commits on Jun 9, 2023

Commits on Jun 10, 2023

Commits on Jun 12, 2023

Commits on Jun 13, 2023

Commits on Jun 14, 2023

Commits on Jun 15, 2023

Commits on Jun 16, 2023

Commits on Jun 19, 2023

Commits on Jun 20, 2023

Commits on Jun 21, 2023

Commits on Jun 23, 2023

Commits on Jun 26, 2023

Commits on Jun 27, 2023

Commits on Jun 28, 2023

Commits on Jun 29, 2023

Commits on Jun 30, 2023

Commits on Jul 3, 2023

Commits on Jul 5, 2023

Commits on Jul 10, 2023

Commits on Jul 12, 2023

Commits on Jul 13, 2023

Commits on Jul 17, 2023

Commits on Jul 18, 2023

Commits on Jul 22, 2023

Commits on Aug 13, 2023

Commits on Aug 14, 2023

Commits on Aug 21, 2023

Commits on Aug 22, 2023

Commits on Aug 27, 2023

Commits on Oct 13, 2023

Commits on Oct 17, 2023

Commits on Oct 23, 2023

Commits on Oct 24, 2023

Commits on Oct 28, 2023

Commits on Nov 18, 2023

Commits on Nov 19, 2023

Commits on Dec 7, 2023

Commits on Dec 16, 2023

Commits on Dec 29, 2023

Commits on Feb 3, 2024

Commits on Feb 22, 2024

Commits on Mar 17, 2024

Commits on Apr 5, 2024

Commits on Apr 7, 2024

Commits on Apr 20, 2024

Commits on Apr 21, 2024

Commits on May 9, 2024

Commits on May 23, 2024

Commits on May 26, 2024

Commits on Jun 21, 2024

Commits on Jul 20, 2024

Commits on Aug 3, 2024