Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Overloaded Operators for KeY lang #3032

Draft
wants to merge 56 commits into
base: main
Choose a base branch
from
Draft

Conversation

wadoon
Copy link
Member

@wadoon wadoon commented Feb 7, 2023

This MR brings overloaded operators to KeY lang:

  1. On function and predicate definitions you can additional add prefix, infix, and postfix notations.

    \functions {
      int add(int, int) \infix(+);
    }
    

    These information are stored inside the Function object.

  2. These information also impacts the pretty printing.

  3. Operators are now a sequence of symbols [-+*/^<>=|]. Their first character determines the precedence. Following are legal expressions:

      a ++ b + c  = ( a ++ b ) + c
      a <|> b <= c 
      a +- b != a + -b
    

This trick avoids an "operator precedence parser", which would also be nice.

more operators are allowed
* do not use relational operator name map
* fix priorities in lexer (/** is not an operator)
* requests for prefix/postfix operators in LDT
* master:
  Move functionality for relevant Java files from NodeInfo to new class ProofJavaSourceCollection
  fix error in logging formatting strings
  fix the collection of JUnit tests on jenkins
  also show message of the chained cause of the exception in IssueDialog
  allowing [] after parameter names in JML model methods
  Fix potential stack overflow in ExplorationStepsList
  allow arrays and general types in JML. (KeYProject#1681)
  fixes KeYProject#1682
  Add Task runWithProfiler to execute key.ui with the  Java Flight Recoder
  Fix symbex test cases
  Attempt to fix KeYProject#1679

# Conflicts:
#	key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
* master:
  [floats] optimising float termination rules
  [floats] reconducting a proof
  [floats] missing rules for double assignments
  [floats] re-implementing a Z3FP solver.
  [floats] added missing unary minus
  repairing cast to integer in JML translation.
  [floats] repairing float-cast rules
  [floats] repairing cast to float
  [floats] nasty method call missing
  [floats] introducing overloaded operator handler
  [floats] missing functions in LDT lookup
  Set the interactive flag for builtin rule applications coming from BuiltInRuleMenuItem correctly
  [floats] adapted taclet option explanations
  fixes KeYProject#1627

# Conflicts:
#	key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
#	key/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java
#	key/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/JMLArithmeticHelper.java
* master: (37 commits)
  missing NPE check in MasterHandlerTest
  Fix KeYProject#1696 (wrong hash for heapAtPre)
  a two-state method needs the invariant also at pre-state (try to fix KeYProject#1689)
  Fix KeYProject#1690
  Fix failing test case
  Fixed rule "wellFormedStoreObjectEQ"
  [floats] repairing JML interpretation of equality on floats and doubles.
  add comment to find AutoSuite
  fix NPE
  remove test filter
  fix, swap argument in assertEquals
  only recoder uses junit4
  translate the remaining Junit4 parts
  fix merge issues
  hopefully fixing gradle test filters
  new category "owntest" for tests with an own gradle task
  falsely marked as test
  migrate TestTacletEquality
  fix gradle settings, remove autosuite
  try to fix RAP
  ...

# Conflicts:
#	key/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java
more operators are allowed
* do not use relational operator name map
* fix priorities in lexer (/** is not an operator)
* requests for prefix/postfix operators in LDT
@wadoon wadoon self-assigned this Feb 7, 2023
@mattulbrich
Copy link
Member

mattulbrich commented Feb 7, 2023

This MR brings overloaded operators to KeY lang:

Does this include overloading in the sense that several signatures can share the same symbol (+ for floats and for integers e.g.). That would really be important.

Update: Just browsed through the examples. It seems that: yes. Great!


functionMetaData
:
INFIX LPAREN op=(PLUS|STAR|SLASH|MINUS|EXP|PERCENT|LESS|LESSEQUAL|GREATER|GREATEREQUAL|LGUILLEMETS) RPAREN
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seams to deviate from the PR description

# By Julian Wiesler (149) and others
# Via Wolfram Pfeifer (25) and others
* origin/main: (338 commits)
  improving javadoc, removing old code.
  Throw exception with location information on invalid unicode escape sequence
  Move JavaCharStream to the correct folder on build
  Report location on error in constant evaluation
  applying spotless
  small fixes and improvements to proof scripts
  adding features to immutable lists
  Fix javadoc formatting
  Correctly handle unloading proofs
  Formatting and documentation
  ignore class output, add test case
  Javac issues extension: handle non-Java proofs
  Fix construction of Javac issue dialog
  fix typo
  Update tests.yml
  Fix javacc deprecation warning
  Fix branch name in Checkstyle script
  Update feature_request.md
  copy bug-report from gitlab to github
  Update dlsmt.sh
  ...

# Conflicts:
#	key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java
#	key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java
#	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java
#	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java
#	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCommons.java
#	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java
#	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
#	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java
#	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/SecurityLattice.java
#	key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java
#	key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java
#	key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java
#	key.core/src/main/java/de/uka/ilkd/key/api/ScriptApi.java
#	key.core/src/main/java/de/uka/ilkd/key/api/VariableAssignments.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/boollattice/BooleanLattice.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java
#	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java
#	key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
#	key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java
#	key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java
#	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java
#	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java
#	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/AuxiliaryComputationAutoPilotMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/ExhaustiveProofMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryBlockComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryLoopComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FullUseInformationFlowContractMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StateExpansionAndInfFlowContractApplicationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/UseInformationFlowContractMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.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/InfFlowProofSymbols.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/BasicBlockExecutionSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicDependsSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicFreeInvSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicFreePreSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopInvariantSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicMbyAtPreDefSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiesSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactoryImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPostconditionSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPreconditionSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfCreatedSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfExactTypeSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfNotNullSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BlockCallPredicateSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowInputOutputRelationSnippet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowPOSnippetFactoryImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/ReplaceAndRegisterMethod.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowCheckInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowContractAppTaclet.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.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/InfFlowMethodContractTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java
#	key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaProgramElement.java
#	key.core/src/main/java/de/uka/ilkd/key/java/JavaReduxFileCollection.java
#	key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/java/Label.java
#	key.core/src/main/java/de/uka/ilkd/key/java/PrettyPrinter.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/SchemaRecoder2KeY.java
#	key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.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/declaration/EnumClassDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/TypeDeclaration.java
#	key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java
#	key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java
#	key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/BinaryOperator.java
#	key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.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/Ccatch.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/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/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/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/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/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/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/KeYCrossReferenceNameInfo.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/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/Model.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/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/RecoderModelTransformer.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/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/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/SeqConcat.java
#	key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java
#	key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/EnhancedFor.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/For.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/JavaStatement.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java
#	key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ContainsStatementVisitor.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/FreeLabelFinder.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.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/ProgramContextAdder.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.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/LDT.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/BoundVarsVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/DefaultVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/GenericTermReplacer.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Namespace.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/PosInProgram.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/PosInTerm.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/SingleRenamingTable.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabelFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabelFactory.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/AbstractTermTransformer.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.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/MixFitInfo.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/ProgramMethod.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/AbstractPropositionalExpansionMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/FullPropositionalExpansionMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/PrepareInfFlowContractPreBranchesMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroListener.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/PropositionalExpansionMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/PropositionalExpansionWithSimplificationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/SMTPreparationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.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/JavascriptCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.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/RuleCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SMTCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveInstCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.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/BuilderHelpers.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.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/ExpressionBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java
#	key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
#	key.core/src/main/java/de/uka/ilkd/key/parser/KeYSemanticException.java
#	key.core/src/main/java/de/uka/ilkd/key/parser/Location.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/SelectPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/SequentViewLogicPrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/pp/StorePrinter.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/MultiThreadedTacletIndex.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/Node.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/NodeIterator.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/NullNewRuleListener.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/SingleThreadedTacletIndex.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollector.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/ApplicationCheck.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.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/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/InitConfig.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.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/init/ProofObligationVars.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/AutoSaver.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/GZipFileRuleSource.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/RuleSourceFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/AbstractFileRepo.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/DiskFileRepo.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/BranchNodeIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/BuiltInAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergeAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergePartnerAppIntermediate.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/AxiomJustification.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/AnyRuleSetTacletFilter.java
#	key.core/src/main/java/de/uka/ilkd/key/prover/impl/AbstractProverCore.java
#	key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
#	key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractContractRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.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/BlockContractExternalBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiationCache.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/RuleSet.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/TacletAttributes.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.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/conditions/ContainsAssignmentCondition.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/FreeLabelInVariableCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/AntecTacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/FindTacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/SuccTacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/TacletMatcherKit.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/TacletMatchProgram.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/TermNavigator.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/BindVariablesInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchElementaryUpdateInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSortDependingFunctionInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeProcedure.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRuleBuiltInRuleApp.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeTotalWeakening.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeWithLatticeAbstraction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayBaseInstanceOf.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayLength.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/ConstructorCall.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/CreateObject.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateWellformedCond.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DoBreak.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/EvaluateArgs.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ExpandMethodBody.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ForToWhile.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ForToWhileTransformation.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.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/PostWork.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SpecialConstructorCall.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/StaticInitialisation.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/Unpack.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilderSchemaVarCollector.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletPrefixBuilder.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/SmtLib2Translator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/communication/LegacyPipe.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/communication/SimplePipe.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/model/Model.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FloatHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/HandlerUtil.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/QuantifierHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExpr.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTHandlerServices.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.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/smt/newsmt2/TypeManager.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.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/BlockContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassAxiomImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassInvariantImpl.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/ContractFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/InitiallyClauseImpl.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/LoopWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/PartialInvAxiom.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedString.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.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/SLEnvInput.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/JMLSpecExtractor.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLUtils.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/TextualJMLLoopSpec.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/jml/translation/ProgramVariableCollection.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/DebugJmlLexer.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/LDTHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.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/SLExceptionFactory.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/SLResolverManager.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTypeResolver.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/FocussedBreakpointRuleApplicationManager.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/FocussedRuleApplicationManager.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/FormulaTermFeatures.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/IsInRangeProvable.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/NumberRuleAppCost.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/StaticFeatureCollection.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DependencyContractFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/IfThenElseMalusFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ImplicitCastNecessary.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MergeRuleFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/QueryExpandCost.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SetsSmallerThanFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ThrownExceptionFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ConstraintAwareSyntacticalReplaceVisitor.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ExistentiallyConnectedFormulasFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/MonomialColumnOp.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TriggerVariableInstantiationProjection.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/ConstantTermFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/ContainsExecutableCodeTermFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/assumptions/AssumptionGenerator.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/assumptions/GenericTranslator.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java
#	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletSoundnessPOLoader.java
#	key.core/src/main/java/de/uka/ilkd/key/util/Assert.java
#	key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java
#	key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java
#	key.core/src/main/java/de/uka/ilkd/key/util/InfFlowSpec.java
#	key.core/src/main/java/de/uka/ilkd/key/util/KeYResourceManager.java
#	key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
#	key.core/src/main/java/de/uka/ilkd/key/util/Pair.java
#	key.core/src/main/java/de/uka/ilkd/key/util/Position.java
#	key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionState.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.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/BuildingIssue.java
#	key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java
#	key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRules.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mapSize.key
#	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key
#	key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java
#	key.core/src/test/java/de/uka/ilkd/key/java/TestJavaCardDLJavaExtensions.java
#	key.core/src/test/java/de/uka/ilkd/key/java/TestJavaInfo.java
#	key.core/src/test/java/de/uka/ilkd/key/java/TestKeYRecoderMapping.java
#	key.core/src/test/java/de/uka/ilkd/key/java/recoderext/TestEnumClassDeclaration.java
#	key.core/src/test/java/de/uka/ilkd/key/java/visitor/TestDeclarationProgramVariableCollector.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInTerm.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestTermBuilder.java
#	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/ScriptLineParserTest.java
#	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/TestProofScriptCommand.java
#	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/meta/RewriteTest.java
#	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjectorTest.java
#	key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/AbstractTestTermParser.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestJMLParserAssociativity.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParserHeap.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParserSorts.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/messages/ParserMessageTest.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsFunctional.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java
#	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/loop/LoopScopeInvRuleTests.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/merge/MergeRuleTests.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/merge/PredicateAbstractionLatticeTests.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/metaconstruct/TestProgramMetaConstructs.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/communication/BufferedMessageReaderTest.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLAssertStatementTest.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/ContractLoadingTests.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/TextualTranslatorTest.java
#	key.core/src/test/java/de/uka/ilkd/key/util/DesignTests.java
#	key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java
#	key.core/src/test/java/de/uka/ilkd/key/util/TestProofStarter.java
#	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/GenericResolutionTransformation.java
#	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/Main.java
#	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveGenerics.java
#	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java
#	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveTypeDeclaration.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/ResolveGenericClass.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestComment.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMethodDeclaration.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMultipleBounds.java
#	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestTypeReference.java
#	key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
#	key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java
#	key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
#	key.ui/src/main/java/de/uka/ilkd/key/core/WebstartMain.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/AutoDismissDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/AuxiliaryContractConfigurator.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/AuxiliaryContractSelectionPanel.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/BlockContractExternalCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/BlockContractInternalCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ExceptionDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/InspectorForDecisionPredicates.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserBookmarkPanel.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopContractExternalCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopContractInternalCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopInvariantRuleCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/NodeInfoVisualizer.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/SearchBar.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoSave.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EnsureSourceConsistencyToggleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LicenseAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RightMouseClickToggleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowKnownTypesAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SystemInfoAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/DefaultContextMenuKind.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/HeatmapExt.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFontSwing.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/MaterialDesignRegular.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergePartnerSelectionDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleCompletion.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/predicateabstraction/AbstractionPredicatesChoiceDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InsertionTacletBrowserMenuItem.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/MenuItemForTwoModeRules.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/PosInSequentTransferable.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentHideWarningBorder.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewInputListener.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewMenu.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/ProofClosedNotification.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/GeneralFailureJTextPaneDisplay.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/GeneralInformationJTextPaneDisplay.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ProofClosedJTextPaneDisplay.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleTermOriginTrackingAction.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifferenceView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/DisableGoal.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIOneStepChildTreeNode.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/NewTranslationOptions.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceViewFrame.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/TextLineNumber.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/BracketMatchingTextArea.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java
#	key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java
#	key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java
#	key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java
#	key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java
#	key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java
#	key.ui/src/main/java/de/uka/ilkd/key/util/PreferenceSaver.java
#	key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java
#	key.ui/src/test/java/de/uka/ilkd/key/gui/KeyboardTacletTest.java
#	key.ui/src/test/java/de/uka/ilkd/key/gui/proofdiff/ProofDifferenceTest.java
#	key.util/src/main/java/org/key_proje…
@wadoon wadoon added this to the v2.14.0 milestone Jul 20, 2023
@github-actions
Copy link

github-actions bot commented Jul 24, 2023

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

wadoon and others added 17 commits July 30, 2023 20:44
* main: (109 commits)
  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)
  update beanshell version in recoder's dependencies
  Switch to Java 17 for KeY-2.14.0
  repair POM generation using afterEvaluate
  Adding license to KeY files
  Adding license to Java files
  add metadata for POM generation and update templates for license headers
  Bump ch.qos.logback:logback-classic from 1.4.8 to 1.4.11
  Fix bug in icon selection
  update samplesIndex.txt
  Repair example index
  better default keyboard shortcuts, corrected docs URL, cleanup
  removing the SmansEtAl example from first touch
  change docking frames dependencies to maven central versions
  ...
* origin/main: (181 commits)
  Use Amazon's Corretto
  add caching for gradle dependencies
  Update to Java 21 Runtime for testing
  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
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
* 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

# Conflicts:
#	key.core/src/main/antlr4/KeYLexer.g4
#	key.core/src/main/antlr4/KeYParser.g4
#	key.core/src/main/antlr4/gen/KeYLexer.java
# 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/nparser/builder/FunctionPredicateBuilder.java
* origin/main:
  Bump org.slf4j:slf4j-api from 2.0.11 to 2.0.12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants