Overloaded Operators for KeY lang #3032
Draft
Commits on Feb 4, 2022
Commits on Feb 8, 2022
-
* do not use relational operator name map * fix priorities in lexer (/** is not an operator) * requests for prefix/postfix operators in LDT
-
Merge branch 'master' into weigl/overop
* 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
Commits on Feb 13, 2022
-
-
Merge branch 'master' into weigl/overop
* 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
-
-
Commits on Feb 16, 2022
-
Merge branch 'master' into weigl/overop
* 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
Commits on Apr 17, 2022
-
-
-
-
-
-
-
-
* do not use relational operator name map * fix priorities in lexer (/** is not an operator) * requests for prefix/postfix operators in LDT
-
-
-
-
Merge remote-tracking branch 'origin/weigl/overop' into weigl/overop
* origin/weigl/overop: fix tests, add whitepsaces add prefix at negDouble remove prefix from neglit fixes failing tests minors fix clash with <-> NotationInfo recognizes MixFitInfos remove old lookup and add metadata remove seq +, use annotation change the loopup functions add MixFitInfo to capture information add metadata information to functions and predicates allow multi-char operators # 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
-
Commits on Jun 24, 2022
-
Merge remote-tracking branch 'origin/master' into weigl/overop
* origin/master: (112 commits) Use generic method correctly avoid creating proof obligations in ProofManagementDialog It is unnecessary to create proof obligations in most cases there and creating some proof obligations changes state shared with a large part of KeY (see KeYProject#1715). JavaDoc for changed methods + Doubles for timeout Checkstyle/SonarQube Avoid reopening popup menu when selection button is pressed Bug fixes from the IdentityHashMap case study Solve missing plugin in shadowJar by adding `mergeServiceFiles()` SonarQube Checkstyle mark JSpinner backgrounds correctly when an error occurs Deactivate SMT button when no proof is loaded Check formatting with Spotless Add JavaDoc Modify problems using solver sockets Minor changes checkstyle Write comments Delete solvers.txt (automatically created during build) Load solvers.txt from everywhere on classpath Fix failing legacy solver test cases by setting different SMT logic ...
Commits on Feb 7, 2023
Commits on Feb 8, 2023
-
Merge remote-tracking branch 'origin/main' into weigl/overop
# 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…
Commits on Jul 23, 2023
Commits on Jul 30, 2023
Commits on Aug 2, 2023
Commits on Aug 27, 2023
-
Merge branch 'main' into weigl/overop
* 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 ...
Commits on Oct 12, 2023
Commits on Nov 19, 2023
-
Merge remote-tracking branch 'origin/main' into weigl/overop
* 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
-
Commits on Nov 27, 2023
Commits on Dec 16, 2023
Commits on Dec 29, 2023
-
-
-
Merge remote-tracking branch 'origin/main' into weigl/overop
* 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
-
Commits on Feb 3, 2024
-
Merge branch 'main' into weigl/overop
# 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
Commits on Feb 11, 2024
Commits on Feb 18, 2024
-
Merge remote-tracking branch 'origin/main' into weigl/overop
* origin/main: Bump org.slf4j:slf4j-api from 2.0.11 to 2.0.12
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.