diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java index 87deb6675f6..293a231f50f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/impl/ExecutionAuxiliaryContract.java @@ -175,10 +175,10 @@ protected void collectRemembranceVariables(Term term, if (SymbolicExecutionUtil.isHeap(eu.lhs(), getServices().getTypeConverter().getHeapLDT())) { remembranceHeaps.put((LocationVariable) term.sub(0).op(), - getServices().getTermBuilder().var(eu.lhs())); + getServices().getTermBuilder().varOfUpdateableOp(eu.lhs())); } else { remembranceLocalVariables.put((LocationVariable) term.sub(0).op(), - getServices().getTermBuilder().var(eu.lhs())); + getServices().getTermBuilder().varOfUpdateableOp(eu.lhs())); } } else { assert false : "Unsupported update term with operator '" + term.op() + "'."; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java index 87dac759a1b..726d64d25fa 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodPO.java @@ -157,8 +157,8 @@ protected ImmutableList buildOperationBlocks( * {@inheritDoc} */ @Override - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { return tb.tt(); } @@ -166,8 +166,8 @@ protected Term generateMbyAtPreDef(ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { if (precondition != null && !precondition.isEmpty()) { var context = Context.inMethod(getProgramMethod(), services.getTermBuilder()); @@ -184,9 +184,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { return tb.tt(); } @@ -196,7 +196,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, */ @Override protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { return tb.tt(); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java index 8dfc33c5a47..46547b4935b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/ProgramMethodSubsetPO.java @@ -224,10 +224,10 @@ protected boolean endsWithReturn(Statement[] statements) { * {@inheritDoc} */ @Override - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.getPre(modHeaps, selfVar, paramVarsList, atPreVars, services); } @@ -236,10 +236,10 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, * {@inheritDoc} */ @Override - protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, - ImmutableList paramVars, List heaps, + protected Term buildFreePre(LocationVariable selfVar, KeYJavaType selfKJT, + ImmutableList paramVars, List heaps, Services proofServices) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.buildFreePre(selfVar, selfKJT, paramVarsList, heaps, proofServices); } @@ -248,10 +248,10 @@ protected Term buildFreePre(ProgramVariable selfVar, KeYJavaType selfKJT, * {@inheritDoc} */ @Override - protected Term ensureUninterpretedPredicateExists(ImmutableList paramVars, - ImmutableList formalParamVars, ProgramVariable exceptionVar, + protected Term ensureUninterpretedPredicateExists(ImmutableList paramVars, + ImmutableList formalParamVars, LocationVariable exceptionVar, String name, Services proofServices) { - ImmutableList paramVarsList = + ImmutableList paramVarsList = convert(undeclaredVariableCollector.result()); return super.ensureUninterpretedPredicateExists(paramVarsList, formalParamVars, exceptionVar, name, proofServices); @@ -263,8 +263,8 @@ protected Term ensureUninterpretedPredicateExists(ImmutableList * @param c The {@link Collection} to convert. * @return The created {@link ImmutableList}. */ - protected static ImmutableList convert(Collection c) { - ImmutableList result = ImmutableSLList.nil(); + protected static ImmutableList convert(Collection c) { + ImmutableList result = ImmutableSLList.nil(); for (LocationVariable var : c) { result = result.append(var); } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java index 639365d2b37..c6084f2b8fb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/breakpoint/AbstractConditionalBreakpoint.java @@ -57,10 +57,10 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea private String conditionString; /** - * A list of {@link ProgramVariable}s containing all variables that were parsed and have to be + * A list of {@link LocationVariable}s containing all variables that were parsed and have to be * possibly replaced during runtime. */ - private ImmutableList varsForCondition; + private ImmutableList varsForCondition; /** * The KeYJavaType of the container of the element associated with the breakpoint. @@ -84,9 +84,9 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea private final Set paramVars; /** - * A {@link ProgramVariable} representing the instance the class KeY is working on + * A {@link LocationVariable} representing the instance the class KeY is working on */ - private ProgramVariable selfVar; + private LocationVariable selfVar; /** * The {@link IProgramMethod} this Breakpoint lies within @@ -291,14 +291,14 @@ private Term computeTermForCondition(String condition) { setSelfVar(new LocationVariable( new ProgramElementName(getProof().getServices().getTermBuilder().newName("self")), containerType, null, false, false)); - ImmutableList varsForCondition = ImmutableSLList.nil(); + ImmutableList varsForCondition = ImmutableSLList.nil(); if (getPm() != null) { // collect parameter variables for (ParameterDeclaration pd : getPm().getParameters()) { for (VariableSpecification vs : pd.getVariables()) { this.paramVars.add((LocationVariable) vs.getProgramVariable()); varsForCondition = - varsForCondition.append((ProgramVariable) vs.getProgramVariable()); + varsForCondition.append((LocationVariable) vs.getProgramVariable()); } } // Collect local variables @@ -313,7 +313,7 @@ private Term computeTermForCondition(String condition) { } JavaInfo info = getProof().getServices().getJavaInfo(); ImmutableList kjts = info.getAllSupertypes(containerType); - ImmutableList globalVars = ImmutableSLList.nil(); + ImmutableList globalVars = ImmutableSLList.nil(); for (KeYJavaType kjtloc : kjts) { if (kjtloc.getJavaType() instanceof TypeDeclaration) { ImmutableList fields = @@ -322,7 +322,7 @@ private Term computeTermForCondition(String condition) { if ((kjtloc.equals(containerType) || !field.isPrivate()) && !((LocationVariable) field.getProgramVariable()).isImplicit()) { globalVars = - globalVars.append((ProgramVariable) field.getProgramVariable()); + globalVars.append((LocationVariable) field.getProgramVariable()); } } } @@ -423,10 +423,10 @@ public boolean isBreakpointHit(SourceElement activeStatement, RuleApp ruleApp, P */ protected abstract boolean isInScopeForCondition(Node node); - private ImmutableList saveAddVariable(LocationVariable x, - ImmutableList varsForCondition) { + private ImmutableList saveAddVariable(LocationVariable x, + ImmutableList varsForCondition) { boolean contains = false; - for (ProgramVariable paramVar : varsForCondition) { + for (var paramVar : varsForCondition) { if (paramVar.toString().equals(x.toString())) { contains = true; break; @@ -512,28 +512,28 @@ public void setVariableNamingMap(Map variableNamingM /** * @return the selfVar */ - public ProgramVariable getSelfVar() { + public LocationVariable getSelfVar() { return selfVar; } /** * @param selfVar the selfVar to set */ - public void setSelfVar(ProgramVariable selfVar) { + public void setSelfVar(LocationVariable selfVar) { this.selfVar = selfVar; } /** * @return the varsForCondition */ - public ImmutableList getVarsForCondition() { + public ImmutableList getVarsForCondition() { return varsForCondition; } /** * @param varsForCondition the varsForCondition to set */ - public void setVarsForCondition(ImmutableList varsForCondition) { + public void setVarsForCondition(ImmutableList varsForCondition) { this.varsForCondition = varsForCondition; } diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index 26b8bcedd61..49a2d95a902 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.symbolic_execution.testcase.util; import java.io.File; +import java.util.HashMap; import java.util.Map; import de.uka.ilkd.key.control.KeYEnvironment; @@ -148,8 +149,12 @@ public void test2GetAndSetChoiceSetting() { // Make sure that all other settings are unchanged. Map changedSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices(); - defaultSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue); - Assertions.assertEquals(defaultSettings, changedSettings); + + Map expectedSettings = new HashMap<>(); + expectedSettings.putAll(defaultSettings); + expectedSettings.put(SymbolicExecutionUtil.CHOICE_SETTING_RUNTIME_EXCEPTIONS, newValue); + + Assertions.assertEquals(expectedSettings, changedSettings); } finally { if (originalValue != null) { SymbolicExecutionUtil.setChoiceSetting( diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java index 5482648451f..511292f6103 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java @@ -302,7 +302,7 @@ private Term addOrigin(Term term) { private ProgramElement parseRow(int irow) throws SVInstantiationParserException { String instantiation = (String) getValueAt(irow, 1); - SchemaVariable sv = (SchemaVariable) getValueAt(irow, 0); + ProgramSV sv = (ProgramSV) getValueAt(irow, 0); ContextInstantiationEntry contextInstantiation = originalApp.instantiations().getContextInstantiation(); @@ -353,7 +353,7 @@ public TacletApp createTacletAppFromVarInsts() throws SVInstantiationException { sort = idd.sort(); if (sort == null) { try { - sort = result.getRealSort(sv, services); + sort = result.getRealSort((OperatorSV) sv, services); } catch (SortException e) { throw new MissingSortException(String.valueOf(sv), createPosition(irow)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java index 61ce8ed878e..6c48fe9b0b6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java @@ -252,8 +252,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -262,9 +262,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -274,7 +274,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -282,8 +283,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java index bb3053c9aad..1b1dd411a00 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java @@ -244,8 +244,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -254,9 +254,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -266,7 +266,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -274,8 +275,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java index 4a587dc9311..d3fa706086b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java @@ -613,11 +613,13 @@ private void printSchemaVariables(StringBuilder result) { result.append("\\schemaVariables{\n"); for (final SchemaVariable sv : getSchemaVariables()) { - final String prefix = sv instanceof FormulaSV ? "\\formula " - : sv instanceof TermSV ? "\\term " : "\\variables "; + if (!(sv instanceof OperatorSV asv)) + continue; + final String prefix = asv instanceof FormulaSV ? "\\formula " + : asv instanceof TermSV ? "\\term " : "\\variables "; result.append(prefix); - result.append(sv.sort().name()).append(" "); - result.append(sv.name()); + result.append(asv.sort().name()).append(" "); + result.append(asv.name()); result.append(";\n"); } result.append("}\n\n"); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java index 0910cd04283..172c30a38af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java @@ -253,16 +253,16 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -270,9 +270,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -281,7 +281,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java index 44c0b766d42..d82be5eb93c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java @@ -256,8 +256,8 @@ protected ImmutableList buildOperationBlocks( @Override @Deprecated - protected Term getPre(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, + protected Term getPre(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -266,9 +266,9 @@ protected Term getPre(List modHeaps, ProgramVariable selfVar, @Override @Deprecated - protected Term getPost(List modHeaps, ProgramVariable selfVar, - ImmutableList paramVars, ProgramVariable resultVar, - ProgramVariable exceptionVar, Map atPreVars, + protected Term getPost(List modHeaps, LocationVariable selfVar, + ImmutableList paramVars, LocationVariable resultVar, + LocationVariable exceptionVar, Map atPreVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); @@ -278,7 +278,8 @@ protected Term getPost(List modHeaps, ProgramVariable selfVar, @Override @Deprecated protected Term buildFrameClause(List modHeaps, Map heapToAtPre, - ProgramVariable selfVar, ImmutableList paramVars, Services services) { + LocationVariable selfVar, ImmutableList paramVars, + Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } @@ -286,8 +287,8 @@ protected Term buildFrameClause(List modHeaps, Map @Override @Deprecated - protected Term generateMbyAtPreDef(ProgramVariable selfVar, - ImmutableList paramVars, Services services) { + protected Term generateMbyAtPreDef(LocationVariable selfVar, + ImmutableList paramVars, Services services) { throw new UnsupportedOperationException( "Not supported any more. " + "Please use the POSnippetFactory instead."); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java index 320f8b6aa96..e3198b3d8cb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java @@ -15,6 +15,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.IObserverFunction; +import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.Modality; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.speclang.*; @@ -162,9 +163,9 @@ public Class getType() { contractContents.put(Key.INF_FLOW_SPECS, modifedSpecs); final Term heap = tb.getBaseHeap(); - final ImmutableSet localInVariables = + final ImmutableSet localInVariables = MiscTools.getLocalIns(invariant.getLoop(), services); - final ImmutableSet localOutVariables = + final ImmutableSet localOutVariables = MiscTools.getLocalOuts(invariant.getLoop(), services); final ImmutableList localInTerms = toTermList(localInVariables); final ImmutableList localOutTerms = toTermList(localOutVariables); @@ -219,9 +220,9 @@ public Class getType() { final Term heap = tb.getBaseHeap(); BlockContract.Terms vars = contract.getVariablesAsTerms(services); - final ImmutableSet localInVariables = + final ImmutableSet localInVariables = MiscTools.getLocalIns(contract.getBlock(), services); - final ImmutableSet localOutVariables = + final ImmutableSet localOutVariables = MiscTools.getLocalOuts(contract.getBlock(), services); final ImmutableList localInTerms = toTermList(localInVariables); final ImmutableList localOutTerms = toTermList(localOutVariables); @@ -234,7 +235,7 @@ public Class getType() { } - private ImmutableList toTermList(ImmutableSet vars) { + private ImmutableList toTermList(ImmutableSet vars) { ImmutableList result = ImmutableSLList.nil(); for (ProgramVariable v : vars) { result = result.append(tb.var(v)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java index 8d04be250ce..474082a360b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.VariableSV; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.OpReplacer; @@ -234,7 +234,7 @@ private Taclet genInfFlowContractApplTaclet(Goal goal, ProofObligationVars appDa // collect quantifiable variables of the post term and replace them // by schema variables - Map quantifiableVarsToSchemaVars = + Map quantifiableVarsToSchemaVars = collectQuantifiableVariables(schemaFind, services); quantifiableVarsToSchemaVars.putAll(collectQuantifiableVariables(schemaAssumes, services)); quantifiableVarsToSchemaVars diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java index 81871f54679..0cce660df30 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java @@ -11,10 +11,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; -import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SchemaVariable; -import de.uka.ilkd.key.logic.op.SchemaVariableFactory; -import de.uka.ilkd.key.logic.op.TermSV; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.RewriteTaclet; import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilder; import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletBuilderSchemaVarCollector; @@ -72,7 +69,7 @@ Term createTermSV(Term t, String schemaPrefix, Services services) { } - SchemaVariable createVariableSV(QuantifiableVariable v, String schemaPrefix, + VariableSV createVariableSV(QuantifiableVariable v, String schemaPrefix, Services services) { if (v == null) { return null; @@ -86,7 +83,7 @@ SchemaVariable createVariableSV(QuantifiableVariable v, String schemaPrefix, void addVarconds(RewriteTacletBuilder tacletBuilder, - Iterable quantifiableSVs) throws IllegalArgumentException { + Iterable quantifiableSVs) throws IllegalArgumentException { RewriteTacletBuilderSchemaVarCollector svCollector = new RewriteTacletBuilderSchemaVarCollector(tacletBuilder); Set schemaVars = svCollector.collectSchemaVariables(); @@ -100,12 +97,12 @@ void addVarconds(RewriteTacletBuilder tacletBuilder, } - Map collectQuantifiableVariables(Term replaceWithTerm, + Map collectQuantifiableVariables(Term replaceWithTerm, Services services) { QuantifiableVariableVisitor qvVisitor = new QuantifiableVariableVisitor(); replaceWithTerm.execPreOrder(qvVisitor); LinkedList quantifiableVariables = qvVisitor.getResult(); - final Map quantifiableVarsToSchemaVars = + final Map quantifiableVarsToSchemaVars = new LinkedHashMap<>(); for (QuantifiableVariable qv : quantifiableVariables) { quantifiableVarsToSchemaVars.put(qv, createVariableSV(qv, "", services)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java index 4b7285e6f9c..821236d28a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java @@ -12,7 +12,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.QuantifiableVariable; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.VariableSV; import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.proof.init.ProofObligationVars; import de.uka.ilkd.key.rule.RewriteTaclet; @@ -82,7 +82,7 @@ public Taclet buildTaclet() { // collect quantifiable variables of the find term and replacewith term // and replace all quantifiable variables by schema variables - Map quantifiableVarsToSchemaVars = + Map quantifiableVarsToSchemaVars = collectQuantifiableVariables(schemaFind, services); quantifiableVarsToSchemaVars .putAll(collectQuantifiableVariables(schemaReplaceWith, services)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java index ca4ca1e0227..c1b8949fbc8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java @@ -260,7 +260,7 @@ public static ProgramVariable localVariable(String name, KeYJavaType kjt) { /** * create a local variable */ - public static ProgramVariable localVariable(ProgramElementName name, KeYJavaType kjt) { + public static LocationVariable localVariable(ProgramElementName name, KeYJavaType kjt) { return new LocationVariable(name, kjt); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java index f3f2c6aacb7..a88985df91e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java @@ -170,14 +170,18 @@ private Term translateOperator(de.uka.ilkd.key.java.expression.Operator op, private Term convertReferencePrefix(ReferencePrefix prefix, ExecutionContext ec) { if (prefix instanceof FieldReference) { return convertVariableReference((FieldReference) prefix, ec); - } else if (prefix instanceof MetaClassReference) { + } else if (prefix instanceof VariableReference vr) { + prefix = vr.getProgramVariable(); + } + if (prefix instanceof MetaClassReference) { LOGGER.warn("WARNING: metaclass references not supported yet"); throw new IllegalArgumentException("TypeConverter could not handle" + " this"); - } else if (prefix instanceof ProgramVariable) { + } else if (prefix instanceof ProgramConstant c) { + // the base case: the leftmost item is a local variable + return tb.var(c); + } else if (prefix instanceof LocationVariable lv) { // the base case: the leftmost item is a local variable - return tb.var((ProgramVariable) prefix); - } else if (prefix instanceof VariableReference) { - return tb.var(((VariableReference) prefix).getProgramVariable()); + return tb.var(lv); } else if (prefix instanceof ArrayReference) { return convertArrayReference((ArrayReference) prefix, ec); } else if (prefix instanceof ThisReference) { @@ -256,8 +260,8 @@ public Term convertMethodReference(MethodReference mr, ExecutionContext ec) { public Term convertVariableReference(VariableReference fr, ExecutionContext ec) { final ReferencePrefix prefix = fr.getReferencePrefix(); final ProgramVariable var = fr.getProgramVariable(); - if (var instanceof ProgramConstant) { - return tb.var(var); + if (var instanceof ProgramConstant pc) { + return tb.var(pc); } else if (var == services.getJavaInfo().getArrayLength()) { return tb.dotLength(convertReferencePrefix(prefix, ec)); } else if (var.isStatic()) { @@ -271,7 +275,7 @@ public Term convertVariableReference(VariableReference fr, ExecutionContext ec) return tb.dot(var.sort(), findThisForSort(var.getContainerType().getSort(), ec), fieldSymbol); } else { - return tb.var(var); + return tb.var((LocationVariable) var); } } else if (!(prefix instanceof PackageReference)) { final JFunction fieldSymbol = @@ -312,8 +316,10 @@ public Term convertToLogicElement(ProgramElement pe) { public Term convertToLogicElement(ProgramElement pe, ExecutionContext ec) { - if (pe instanceof ProgramVariable) { - return tb.var((ProgramVariable) pe); + if (pe instanceof ProgramConstant pc) { + return tb.var(pc); + } else if (pe instanceof LocationVariable lv) { + return tb.var(lv); } else if (pe instanceof FieldReference) { return convertVariableReference((FieldReference) pe, ec); } else if (pe instanceof MethodReference) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchSVWrapper.java index 9c796cf4923..cd5c920df7f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.Identifier; import recoder.java.ProgramElement; @@ -16,26 +16,17 @@ public class CatchSVWrapper extends Catch implements KeYRecoderExtension, SVWrap * */ private static final long serialVersionUID = 6288254708744002494L; - protected SchemaVariable sv; + protected final OperatorSV sv; - public CatchSVWrapper(SchemaVariable sv) { + public CatchSVWrapper(OperatorSV sv) { this.sv = sv; } - /** - * sets the schema variable of sort statement - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; - } - /** * returns a String name of this meta construct. */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchSVWrapper.java index 68450978928..3de85be5f17 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CcatchSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.Identifier; import recoder.java.ProgramElement; @@ -11,19 +11,9 @@ public class CcatchSVWrapper extends Ccatch implements KeYRecoderExtension, SVWrapper { private static final long serialVersionUID = -1; - protected SchemaVariable sv; + protected final OperatorSV sv; - public CcatchSVWrapper(SchemaVariable sv) { - this.sv = sv; - } - - /** - * sets the schema variable of sort statement - * - * @param sv the SchemaVariable - */ - @Override - public void setSV(SchemaVariable sv) { + public CcatchSVWrapper(OperatorSV sv) { this.sv = sv; } @@ -31,7 +21,7 @@ public void setSV(SchemaVariable sv) { * returns a String name of this meta construct. */ @Override - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java index 31b4797f03f..ee3687ff44c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.SourceVisitor; @@ -13,26 +13,17 @@ public class ExecCtxtSVWrapper extends ExecutionContext implements KeYRecoderExt * */ private static final long serialVersionUID = 2299515454738715766L; - SchemaVariable sv = null; + private final OperatorSV sv; - public ExecCtxtSVWrapper(SchemaVariable sv) { - this.sv = sv; - } - - /** - * sets the schema variable of sort label - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { + public ExecCtxtSVWrapper(OperatorSV sv) { this.sv = sv; } /** * returns the schema variable of this type sv wrapper */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java index 576e3d8d0dc..49396d336d7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.Expression; import recoder.java.LoopInitializer; @@ -20,7 +20,7 @@ public class ExpressionSVWrapper extends Literal * */ private static final long serialVersionUID = 7659491655661716390L; - protected SchemaVariable sv; + protected final OperatorSV sv; protected ReferenceSuffix suff; @@ -28,14 +28,11 @@ public class ExpressionSVWrapper extends Literal protected ExpressionSVWrapper(ExpressionSVWrapper proto) { super(proto); + sv = proto.getSV(); expressionParent = null; } - public ExpressionSVWrapper() { - expressionParent = null; - } - - public ExpressionSVWrapper(SchemaVariable sv) { + public ExpressionSVWrapper(OperatorSV sv) { this.sv = sv; expressionParent = null; } @@ -47,25 +44,18 @@ public void makeParentRoleValid() { } - /** - * sets the schema variable of sort statement - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; - } - - - public SchemaVariable getSV() { + @Override + public OperatorSV getSV() { return sv; } // don't think we need it + @Override public void accept(SourceVisitor v) { } + @Override public ExpressionSVWrapper deepClone() { return new ExpressionSVWrapper(sv); } @@ -75,6 +65,7 @@ public ExpressionSVWrapper deepClone() { * * @return the statement container. */ + @Override public StatementContainer getStatementContainer() { return statementParent; } @@ -84,11 +75,13 @@ public StatementContainer getStatementContainer() { * * @param c a statement container. */ + @Override public void setStatementContainer(StatementContainer c) { statementParent = c; } + @Override public ReferenceSuffix getReferenceSuffix() { return suff; } @@ -98,6 +91,7 @@ public ReferenceSuffix getReferenceSuffix() { * * @param path a reference suffix. */ + @Override public void setReferenceSuffix(ReferenceSuffix path) { suff = path; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JumpLabelSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JumpLabelSVWrapper.java index 52c2aced03c..ea53c160bb8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JumpLabelSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JumpLabelSVWrapper.java @@ -3,24 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; public class JumpLabelSVWrapper implements SVWrapper { - private SchemaVariable label; + private final OperatorSV label; - public JumpLabelSVWrapper(SchemaVariable l) { + public JumpLabelSVWrapper(OperatorSV l) { label = l; } - public SchemaVariable getSV() { + public OperatorSV getSV() { return label; } - public void setSV(SchemaVariable sv) { - label = sv; - } - public String toString() { return String.valueOf(label); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LabelSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LabelSVWrapper.java index aeba1e4aefc..de3ed1fa7f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LabelSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LabelSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.Identifier; @@ -13,30 +13,22 @@ public class LabelSVWrapper extends Identifier implements KeYRecoderExtension, S * */ private static final long serialVersionUID = 5338442155201858492L; - SchemaVariable sv = null; + private final OperatorSV sv; - public LabelSVWrapper(SchemaVariable sv) { + public LabelSVWrapper(OperatorSV sv) { this.sv = sv; } protected LabelSVWrapper(LabelSVWrapper proto) { super(proto); + sv = proto.getSV(); id = proto.id; } - /** - * sets the schema variable of sort label - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; - } - /** * returns the schema variable of this label sv wrapper */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodSignatureSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodSignatureSVWrapper.java index d995dc7cd8b..5d4164bbfdf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodSignatureSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodSignatureSVWrapper.java @@ -4,26 +4,22 @@ package de.uka.ilkd.key.java.recoderext; import de.uka.ilkd.key.java.recoderext.adt.MethodSignature; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; public class MethodSignatureSVWrapper extends MethodSignature implements SVWrapper { private static final long serialVersionUID = -4381850332826267659L; - private SchemaVariable method; + private final OperatorSV method; - public MethodSignatureSVWrapper(SchemaVariable l) { + public MethodSignatureSVWrapper(OperatorSV l) { super(null, null); method = l; } - public SchemaVariable getSV() { + public OperatorSV getSV() { return method; } - public void setSV(SchemaVariable sv) { - method = sv; - } - public String toString() { return String.valueOf(method); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProgramVariableSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProgramVariableSVWrapper.java index 9c11e1adb7e..3411f0cca43 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProgramVariableSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ProgramVariableSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.Identifier; @@ -13,29 +13,21 @@ public class ProgramVariableSVWrapper extends Identifier implements KeYRecoderEx * */ private static final long serialVersionUID = 8398356228769806560L; - SchemaVariable sv = null; + private final OperatorSV sv; - public ProgramVariableSVWrapper(SchemaVariable sv) { + public ProgramVariableSVWrapper(OperatorSV sv) { this.sv = sv; } protected ProgramVariableSVWrapper(ProgramVariableSVWrapper proto) { super(proto); - } - - /** - * sets the schema variable of sort label - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; + sv = proto.getSV(); } /** * returns the schema variable of this type sv wrapper */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SVWrapper.java index 8c0f0eac73f..88f023eee4a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SVWrapper.java @@ -3,21 +3,11 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; public interface SVWrapper { - - /** - * sets the schema variable of sort statement - * - * @param sv the SchemaVariable to wrap - */ - void setSV(SchemaVariable sv); - /** * returns a String name of this meta construct. */ - SchemaVariable getSV(); - - + OperatorSV getSV(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java index a66418df167..aaa3b8c582d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java @@ -8,6 +8,7 @@ import java.util.List; import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.op.OperatorSV; import de.uka.ilkd.key.logic.op.ProgramSV; import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.sort.ProgramSVSort; @@ -128,7 +129,7 @@ public PassiveExpression createPassiveExpression() { return new PassiveExpression(); } - public static void throwSortInvalid(SchemaVariable sv, String s) throws ParseException { + public static void throwSortInvalid(OperatorSV sv, String s) throws ParseException { throw new ParseException("Sort of declared schema variable " + sv.name().toString() + " " + sv.sort().name().toString() + " does not comply with expected type " + s + " in Java program."); @@ -140,18 +141,18 @@ public boolean lookupSchemaVariableType(String s, ProgramSVSort sort) { return false; } SchemaVariable n = svns.lookup(new Name(s)); - if (n instanceof SchemaVariable) { - return n.sort() == sort; + if (n instanceof OperatorSV asv) { + return asv.sort() == sort; } return false; } - public SchemaVariable lookupSchemaVariable(String s) throws ParseException { - SchemaVariable sv = null; + public OperatorSV lookupSchemaVariable(String s) throws ParseException { + OperatorSV sv; SchemaVariable n = svns.lookup(new Name(s)); - if (n instanceof SchemaVariable) { - sv = n; + if (n instanceof OperatorSV asv) { + sv = asv; } else { throw new ParseException("Schema variable not declared: " + s); } @@ -159,7 +160,7 @@ public SchemaVariable lookupSchemaVariable(String s) throws ParseException { } public StatementSVWrapper getStatementSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Statement"); } @@ -168,7 +169,7 @@ public StatementSVWrapper getStatementSV(String s) throws ParseException { } public ExpressionSVWrapper getExpressionSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Expression"); } @@ -177,7 +178,7 @@ public ExpressionSVWrapper getExpressionSV(String s) throws ParseException { public LabelSVWrapper getLabelSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Label"); } @@ -185,7 +186,7 @@ public LabelSVWrapper getLabelSV(String s) throws ParseException { } public MethodSignatureSVWrapper getMethodSignatureSVWrapper(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "MethodSignature"); } @@ -193,7 +194,7 @@ public MethodSignatureSVWrapper getMethodSignatureSVWrapper(String s) throws Par } public JumpLabelSVWrapper getJumpLabelSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV) || sv.sort() != ProgramSVSort.LABEL) { throwSortInvalid(sv, "Label"); } @@ -201,7 +202,7 @@ public JumpLabelSVWrapper getJumpLabelSV(String s) throws ParseException { } public TypeSVWrapper getTypeSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Type"); } @@ -209,7 +210,7 @@ public TypeSVWrapper getTypeSV(String s) throws ParseException { } public ExecCtxtSVWrapper getExecutionContextSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Type"); } @@ -217,7 +218,7 @@ public ExecCtxtSVWrapper getExecutionContextSV(String s) throws ParseException { } public ProgramVariableSVWrapper getProgramVariableSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Program Variable"); } @@ -225,7 +226,7 @@ public ProgramVariableSVWrapper getProgramVariableSV(String s) throws ParseExcep } public CatchSVWrapper getCatchSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Catch"); } @@ -233,7 +234,7 @@ public CatchSVWrapper getCatchSV(String s) throws ParseException { } public CcatchSVWrapper getCcatchSV(String s) throws ParseException { - SchemaVariable sv = lookupSchemaVariable(s); + var sv = lookupSchemaVariable(s); if (!(sv instanceof ProgramSV)) { throwSortInvalid(sv, "Ccatch"); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java index 68bde4ec34c..9ef36511a6f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.ProgramElement; import recoder.java.SourceVisitor; @@ -16,16 +16,14 @@ public class StatementSVWrapper extends JavaStatement implements KeYRecoderExten * */ private static final long serialVersionUID = -4062276649575988872L; - protected SchemaVariable sv; + protected final OperatorSV sv; protected StatementSVWrapper(StatementSVWrapper proto) { super(proto); + sv = proto.getSV(); } - public StatementSVWrapper() { - } - - public StatementSVWrapper(SchemaVariable sv) { + public StatementSVWrapper(OperatorSV sv) { this.sv = sv; } @@ -80,19 +78,10 @@ public boolean replaceChild(ProgramElement p, ProgramElement q) { } - /** - * sets the schema variable of sort statement - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; - } - /** * returns a String name of this meta construct. */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java index 5c6387eb84a..4113fd4e944 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/TypeSVWrapper.java @@ -3,7 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; -import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.logic.op.OperatorSV; import recoder.java.SourceElement; import recoder.java.reference.TypeReference; @@ -14,29 +14,21 @@ public class TypeSVWrapper extends TypeReference implements KeYRecoderExtension, * */ private static final long serialVersionUID = 2694567717981292433L; - SchemaVariable sv = null; + private final OperatorSV sv; - public TypeSVWrapper(SchemaVariable sv) { + public TypeSVWrapper(OperatorSV sv) { this.sv = sv; } protected TypeSVWrapper(TypeSVWrapper proto) { super(proto); - } - - /** - * sets the schema variable of sort label - * - * @param sv the SchemaVariable - */ - public void setSV(SchemaVariable sv) { - this.sv = sv; + sv = proto.getSV(); } /** * returns the schema variable of this type sv wrapper */ - public SchemaVariable getSV() { + public OperatorSV getSV() { return sv; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java index 344828299a4..a796487d7d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java @@ -26,11 +26,11 @@ public class OuterBreakContinueAndReturnReplacer extends JavaASTVisitor { protected static final Boolean CHANGED = Boolean.TRUE; private final Break breakOut; - private final Map breakFlags; - private final Map continueFlags; - private final ProgramVariable returnFlag; - private final ProgramVariable returnValue; - private final ProgramVariable exception; + private final Map breakFlags; + private final Map continueFlags; + private final LocationVariable returnFlag; + private final LocationVariable returnValue; + private final LocationVariable exception; private final ArrayDeque stack = new ArrayDeque<>(); private final ArrayDeque