diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java index a688d5aa657..247e536fa3f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java @@ -1689,7 +1689,8 @@ public static int computeStackSize(RuleApp ruleApp) { JavaProgramElement element = block.program(); if (element instanceof StatementBlock) { StatementBlock b = (StatementBlock) block.program(); - ImmutableArray prefix = b.getPrefixElements(); + ImmutableArray prefix = + b.getPrefixElements(); result = CollectionUtil.count(prefix, element1 -> element1 instanceof MethodFrame); } @@ -4006,7 +4007,8 @@ public static Pair computeSecondStatement( blocks.addFirst((StatementBlock) firstStatement); } SourceElement lastStatement = null; - while (firstStatement instanceof ProgramPrefix && lastStatement != firstStatement) { + while (firstStatement instanceof PossibleProgramPrefix + && lastStatement != firstStatement) { lastStatement = firstStatement; firstStatement = firstStatement.getFirstElementIncludingBlocks(); if (lastStatement instanceof MethodFrame) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java index 52119071f24..e01a3a51920 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.statement.MethodFrame; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -166,12 +166,12 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { ExecutionContext lastExecutionContext = null; - final ProgramPrefix prefix; + final PossibleProgramPrefix prefix; int pos = -1; PosInProgram relPos = PosInProgram.TOP; - if (src instanceof ProgramPrefix) { - prefix = (ProgramPrefix) src; + if (src instanceof PossibleProgramPrefix) { + prefix = (PossibleProgramPrefix) src; final int srcPrefixLength = prefix.getPrefixLength(); if (patternPrefixLength > srcPrefixLength) { @@ -180,7 +180,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { pos = srcPrefixLength - patternPrefixLength; - ProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); + PossibleProgramPrefix firstActiveStatement = getPrefixElementAt(prefix, pos); relPos = firstActiveStatement.getFirstActiveChildPos(); @@ -199,8 +199,9 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { start = relPos.get(relPos.depth() - 1); if (relPos.depth() > 1) { - firstActiveStatement = (ProgramPrefix) PosInProgram.getProgramAt(relPos.up(), - firstActiveStatement); + firstActiveStatement = + (PossibleProgramPrefix) PosInProgram.getProgramAt(relPos.up(), + firstActiveStatement); } } newSource = new SourceData(firstActiveStatement, start, services); @@ -232,7 +233,7 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { * position */ private MatchConditions makeContextInfoComplete(MatchConditions matchCond, SourceData newSource, - ProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src, + PossibleProgramPrefix prefix, int pos, PosInProgram relPos, ProgramElement src, Services services) { final SVInstantiations instantiations = matchCond.getInstantiations(); @@ -264,7 +265,7 @@ private MatchConditions makeContextInfoComplete(MatchConditions matchCond, Sourc */ private MatchConditions matchInnerExecutionContext(MatchConditions matchCond, final Services services, ExecutionContext lastExecutionContext, - final ProgramPrefix prefix, int pos, final ProgramElement src) { + final PossibleProgramPrefix prefix, int pos, final ProgramElement src) { // partial context instantiation @@ -302,10 +303,11 @@ private MatchConditions matchInnerExecutionContext(MatchConditions matchCond, * prefix.getPrefixElementAt(pos); * @return the PosInProgram of the first element, which is not part of the prefix */ - private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInProgram relPos) { + private PosInProgram matchPrefixEnd(final PossibleProgramPrefix prefix, int pos, + PosInProgram relPos) { PosInProgram prefixEnd = PosInProgram.TOP; if (prefix != null) { - ProgramPrefix currentPrefix = prefix; + PossibleProgramPrefix currentPrefix = prefix; int i = 0; while (i <= pos) { final IntIterator it = currentPrefix.getFirstActiveChildPos().iterator(); @@ -328,8 +330,8 @@ private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInPr return prefixEnd; } - private static ProgramPrefix getPrefixElementAt(ProgramPrefix prefix, int i) { - ProgramPrefix current = prefix; + private static PossibleProgramPrefix getPrefixElementAt(PossibleProgramPrefix prefix, int i) { + PossibleProgramPrefix current = prefix; for (int pos = 0; pos < i; pos++) { current = current.getNextPrefixElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java index 26ffcb6a72e..757a5296451 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/JavaTools.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.java.visitor.CreatingASTVisitor; import de.uka.ilkd.key.java.visitor.JavaASTVisitor; import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; @@ -32,12 +32,15 @@ public static SourceElement getActiveStatement(JavaBlock jb) { assert jb.program() != null; SourceElement result = jb.program().getFirstElement(); - while ((result instanceof ProgramPrefix || result instanceof CatchAllStatement) - && !(result instanceof StatementBlock && ((StatementBlock) result).isEmpty())) { + while ((result instanceof PossibleProgramPrefix pre && pre.isPrefix()) + || result instanceof CatchAllStatement) { if (result instanceof LabeledStatement) { result = ((LabeledStatement) result).getChildAt(1); } else if (result instanceof CatchAllStatement) { result = ((CatchAllStatement) result).getBody(); + } else if (result == result.getFirstElement() + && ((PossibleProgramPrefix) result).isPrefix()) { + System.out.println(result); } else { result = result.getFirstElement(); } 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 8545b8cb1e3..e107aea8984 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 @@ -2313,7 +2313,7 @@ public static SuperReference superReference() { * @return a new {@link Switch} block that executes branches depending on the value * of expression */ - public static Switch switchBlock(final Expression expression, final Branch[] branches) { + public static Switch switchBlock(final Expression expression, final SwitchBranch[] branches) { final Switch block = new Switch(expression, branches); return block; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java b/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java index f409c13a8dd..056210e3817 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ProgramPrefixUtil.java @@ -4,7 +4,7 @@ package de.uka.ilkd.key.java; import de.uka.ilkd.key.java.statement.MethodFrame; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; public class ProgramPrefixUtil { @@ -26,7 +26,7 @@ public MethodFrame getInnerMostMethodFrame() { } } - public static ProgramPrefixInfo computeEssentials(ProgramPrefix prefix) { + public static ProgramPrefixInfo computeEssentials(PossibleProgramPrefix prefix) { int length = 1; MethodFrame mf = (MethodFrame) (prefix instanceof MethodFrame ? prefix : null); while (prefix.hasNextPrefixElement()) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 02cb218f130..d3050cad9a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -399,7 +399,7 @@ private ExtList collectChildrenAndComments(recoder.java.ProgramElement pe) { * @param se the sourcelement to extract from, not null * @return the newly created PositionInfo */ - private PositionInfo positionInfo(recoder.java.SourceElement se) { + protected PositionInfo positionInfo(recoder.java.SourceElement se) { var relPos = se.getRelativePosition(); var startPos = Position.fromSEPosition(se.getStartPosition()); var endPos = Position.fromSEPosition(se.getEndPosition()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index c97fa310414..3410fe8241e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -217,6 +217,11 @@ public MethodBodyStatement convert(RMethodBodyStatement l) { return new MethodBodyStatement(tr, resVar, convert(l.getMethodReference())); } + public ActiveCase convert(de.uka.ilkd.key.java.recoderext.ActiveCase ac) { + ExtList children = collectChildren(ac); + return new ActiveCase(children, positionInfo(ac)); + } + /** * translate Context statement blocks */ @@ -279,13 +284,17 @@ public SchemaVariable convert(CcatchSVWrapper svw) { return svw.getSV(); } - public SchemaVariable convert(ProgramVariableSVWrapper svw) { + public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.ProgramVariableSVWrapper svw) { + return svw.getSV(); + } + public SchemaVariable convert(de.uka.ilkd.key.java.recoderext.SwitchBranchSVWrapper svw) { return svw.getSV(); } /** - * for some reason the this and super references have to be treated differently here. + * for some reason the {@code this} and {@code super} references have to be treated differently + * here. */ @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java index 3aed53cad25..cb15a5da8dc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.java.statement.MethodFrame; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.util.Debug; import org.key_project.util.ExtList; @@ -21,7 +21,7 @@ * Statement block. taken from COMPOST and changed to achieve an immutable structure */ public class StatementBlock extends JavaStatement implements StatementContainer, - TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix { + TypeDeclarationContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Body. @@ -102,9 +102,9 @@ public boolean equals(Object o) { } /** computes the prefix elements for the given array of statment block */ - public static ImmutableArray computePrefixElements( - ImmutableArray b, ProgramPrefix current) { - final ArrayList prefix = new ArrayList<>(); + public static ImmutableArray computePrefixElements( + PossibleProgramPrefix current) { + final ArrayList prefix = new ArrayList<>(); prefix.add(current); while (current.hasNextPrefixElement()) { @@ -246,23 +246,29 @@ public SourceElement getFirstElementIncludingBlocks() { } } + @Override + public boolean isPrefix() { + return !isEmpty(); + } + @Override public boolean hasNextPrefixElement() { - return body.size() != 0 && (body.get(0) instanceof ProgramPrefix); + return body.size() != 0 && (body.get(0) instanceof PossibleProgramPrefix); } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.get(0); + return (PossibleProgramPrefix) body.get(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { - return hasNextPrefixElement() ? ((ProgramPrefix) body.get(0)).getLastPrefixElement() : this; + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? ((PossibleProgramPrefix) body.get(0)).getLastPrefixElement() + : this; } @Override @@ -276,8 +282,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return computePrefixElements(body, this); + public ImmutableArray getPrefixElements() { + return computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java new file mode 100644 index 00000000000..75510a8957a --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ActiveCase.java @@ -0,0 +1,209 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.recoderext; + +import recoder.java.*; +import recoder.java.statement.EmptyStatement; +import recoder.java.statement.SwitchBranch; +import recoder.list.generic.ASTList; + +public class ActiveCase extends SwitchBranch { + /** + * serialization id + */ + private static final long serialVersionID = /* TODO */ 0; + + /** + * Body. + */ + protected ASTList body; + + /** + * ActiveCase. + */ + public ActiveCase() { + super(); + } + + /** + * ActiveCase. + */ + public ActiveCase(ASTList body) { + setBody(body); + makeParentRoleValid(); + } + + /** + * Case. + * + * @param proto a case. + */ + + protected ActiveCase(ActiveCase proto) { + super(proto); + if (proto.body != null) { + body = proto.body.deepClone(); + } + makeParentRoleValid(); + } + + /** + * Deep clone. + * + * @return the object. + */ + + public ActiveCase deepClone() { + return new ActiveCase(this); + } + + /** + * Make parent role valid. + */ + + public void makeParentRoleValid() { + super.makeParentRoleValid(); + if (body != null) { + for (Statement statement : body) { + statement.setStatementContainer(this); + } + } + } + + /** + * Returns the number of children of this node. + * + * @return an int giving the number of children of this node + */ + + public int getChildCount() { + int result = 0; + if (body != null) { + result += body.size(); + } + return result; + } + + /** + * Returns the child at the specified index in this node's "virtual" child array + * + * @param index an index into this node's "virtual" child array + * @return the program element at the given position + * @throws ArrayIndexOutOfBoundsException if index is out of bounds + */ + + public ProgramElement getChildAt(int index) { + int len; + if (body != null) { + len = body.size(); + if (len > index) { + return body.get(index); + } + index -= len; + } + throw new ArrayIndexOutOfBoundsException(); + } + + public int getChildPositionCode(ProgramElement child) { + // role 0 (IDX): body + if (body != null) { + int index = body.indexOf(child); + if (index >= 0) { + return (index << 4); + } + } + return -1; + } + + /** + * Replace a single child in the current node. The child to replace is matched by identity and + * hence must be known exactly. The replacement element can be null - in that case, the child is + * effectively removed. The parent role of the new child is validated, while the parent link of + * the replaced child is left untouched. + * + * @param p the old child. + * @param q the new child. + * @return true if a replacement has occured, false otherwise. + * @throws ClassCastException if the new child cannot take over the role of the old one. + */ + + public boolean replaceChild(ProgramElement p, ProgramElement q) { + int count; + if (p == null) { + throw new NullPointerException(); + } + count = (body == null) ? 0 : body.size(); + for (int i = 0; i < count; i++) { + if (body.get(i) == p) { + if (q == null) { + body.remove(i); + } else { + Statement r = (Statement) q; + body.set(i, r); + r.setStatementContainer(this); + } + return true; + } + } + return false; + } + + /** + * Get the number of statements in this container. + * + * @return the number of statements. + */ + + public int getStatementCount() { + return (body != null) ? body.size() : 0; + } + + /* + * Return the statement at the specified index in this node's "virtual" statement array. @param + * index an index for a statement. @return the statement with the given index. @exception + * ArrayIndexOutOfBoundsException if index is out of bounds. + */ + + public Statement getStatementAt(int index) { + if (body != null) { + return body.get(index); + } + throw new ArrayIndexOutOfBoundsException(); + } + + /** + * The body may be empty (null), to define a fall-through. Attaching an + * {@link EmptyStatement}would create a single ";". + */ + + public ASTList getBody() { + return body; + } + + /** + * Set body. + * + * @param list a statement mutable list. + */ + + public void setBody(ASTList list) { + body = list; + } + + public void accept(SourceVisitor v) { + if (v instanceof SourceVisitorExtended e) { + e.visitActiveCase(this); + } else { + throw new IllegalStateException( + "Method 'accept' not implemented in " + "ActiveCase"); + } + } + + public SourceElement getLastElement() { + if (body == null || body.size() == 0) { + return this; + } + return body.get(body.size() - 1).getLastElement(); + } +} 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 87c056b5014..498409ae70b 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 @@ -122,6 +122,10 @@ public MergePointStatement createMergePointStatement(Expression e) { return new MergePointStatement(e); } + public ActiveCase createActiveCase() { + return new ActiveCase(); + } + /** * Create a {@link PassiveExpression}. */ @@ -241,6 +245,14 @@ public CcatchSVWrapper getCcatchSV(String s) throws ParseException { return new CcatchSVWrapper(sv); } + public SwitchBranchSVWrapper getSwitchBranchSV(String s) throws ParseException { + JOperatorSV sv = lookupSchemaVariable(s); + if (!(sv instanceof ProgramSV)) { + throwSortInvalid(sv, "SwitchCase"); + } + return new SwitchBranchSVWrapper((ProgramSV) sv); + } + /** * For internal reuse and synchronization. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java index 52f3c417cc9..a05e76ed200 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SourceVisitorExtended.java @@ -13,6 +13,10 @@ */ public class SourceVisitorExtended extends SourceVisitor { + public void visitActiveCase(ActiveCase x) { + // default do nothing + } + public void visitCatchAll(CatchAllStatement x) { // default do nothing } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..f24543204bd --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SwitchBranchSVWrapper.java @@ -0,0 +1,79 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.recoderext; + +import de.uka.ilkd.key.logic.op.ProgramSV; + +import org.key_project.logic.op.sv.SchemaVariable; + +import recoder.java.ProgramElement; +import recoder.java.SourceVisitor; +import recoder.java.Statement; +import recoder.java.statement.SwitchBranch; + +public class SwitchBranchSVWrapper extends SwitchBranch implements KeYRecoderExtension, SVWrapper { + private static final long serialVersionUID = -1; + protected ProgramSV sv; + + public SwitchBranchSVWrapper(ProgramSV sv) { + this.sv = sv; + } + + /** + * sets the schema variable of sort statement + * + * @param sv the SchemaVariable + */ + public void setSV(SchemaVariable sv) { + this.sv = (ProgramSV) sv; + } + + /** + * returns a String name of this meta construct. + */ + @Override + public ProgramSV getSV() { + return sv; + } + + @Override + public void accept(SourceVisitor v) { + + } + + public SwitchBranchSVWrapper deepClone() { + return new SwitchBranchSVWrapper(sv); + } + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public int getChildPositionCode(ProgramElement child) { + return 0; + } + + @Override + public boolean replaceChild(ProgramElement p, ProgramElement q) { + return false; + } + + @Override + public int getStatementCount() { + return 0; + } + + @Override + public Statement getStatementAt(int index) { + throw new IndexOutOfBoundsException(); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java new file mode 100644 index 00000000000..84a192fdbca --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ActiveCase.java @@ -0,0 +1,199 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; + +import org.key_project.util.ExtList; +import org.key_project.util.collection.ImmutableArray; + +public class ActiveCase extends SwitchBranch implements PossibleProgramPrefix { + /** + * Body. + */ + protected final ImmutableArray body; + + private final MethodFrame innerMostMethodFrame; + + private final int prefixLength; + + public ActiveCase() { + this.body = null; + prefixLength = 0; + innerMostMethodFrame = null; + } + + public ActiveCase(Statement[] body) { + this.body = new ImmutableArray<>(body); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public ActiveCase(ImmutableArray body) { + this.body = body; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Constructor for the transformation of COMPOST ASTs to KeY. + * + * @param children the children of this AST element as KeY classes. May contain: Comments, + * several of Statement (as the statements for Default) + */ + public ActiveCase(ExtList children) { + super(children); + this.body = new ImmutableArray<>(children.collect(Statement.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Constructor for the transformation of COMPOST ASTs to KeY. + * + * @param children the children of this AST element as KeY classes. May contain: Comments a + * Statement (as the statement following case) Must NOT contain: an Expression indicating + * the condition of the case as there are classes that are Expression and Statement, so + * they might get mixed up. Use the second parameter of this constructor for the + * expression. + */ + public ActiveCase(ExtList children, PositionInfo pos) { + super(children, pos); + this.body = new ImmutableArray<>(children.collect(Statement.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + /** + * Returns the number of children of this node. + * + * @return an int giving the number of children of this node + */ + public int getChildCount() { + int result = 0; + if (body != null) { + result += body.size(); + } + return result; + } + + /** + * Returns the child at the specified index in this node's "virtual" child array + * + * @param index an index into this node's "virtual" child array + * @return the program element at the given position + * @exception ArrayIndexOutOfBoundsException if index is out of bounds + */ + public ProgramElement getChildAt(int index) { + int len; + if (body != null) { + len = body.size(); + if (len > index) { + return body.get(index); + } + } + throw new ArrayIndexOutOfBoundsException(); + } + + @Override + public SourceElement getFirstElement() { + if (body.isEmpty()) + return this; + return body.get(0); + } + + /** + * Get the number of statements in this container. + * + * @return the number of statements. + */ + public int getStatementCount() { + return (body != null) ? body.size() : 0; + } + + /* + * Return the statement at the specified index in this node's "virtual" statement array. + * + * @param index an index for a statement. + * + * @return the statement with the given index. + * + * @exception ArrayIndexOutOfBoundsException if index is out of bounds. + */ + public Statement getStatementAt(int index) { + if (body != null) { + return body.get(index); + } + throw new ArrayIndexOutOfBoundsException(); + } + + /** + * The body may be empty (null), to define a fall-through. Attaching an {@link EmptyStatement} + * would create a single ";". + */ + public ImmutableArray getBody() { + return body; + } + + /** + * calls the corresponding method of a visitor in order to perform some action/transformation on + * this element + * + * @param v the Visitor + */ + public void visit(Visitor v) { + v.performActionOnActiveCase(this); + } + + @Override + public boolean isPrefix() { + return body != null && !body.isEmpty(); + } + + @Override + public boolean hasNextPrefixElement() { + return body != null && !body.isEmpty() && body.get(0) instanceof PossibleProgramPrefix; + } + + @Override + public PossibleProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (PossibleProgramPrefix) body.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; + } + + @Override + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return body.isEmpty() ? PosInProgram.TOP : PosInProgram.ZERO; + } + + @Override + public int getPrefixLength() { + return prefixLength; + } + + @Override + public MethodFrame getInnerMostMethodFrame() { + return innerMostMethodFrame; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java index c3c9cd54322..ce9e60953b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/BranchStatement.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.statement; +import de.uka.ilkd.key.java.PositionInfo; import org.key_project.util.ExtList; @@ -19,6 +20,11 @@ protected BranchStatement() { } + public BranchStatement(PositionInfo pos) { + super(pos); + } + + /** * Constructor for the transformation of COMPOST ASTs to KeY. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java index c1c9535b626..de361fb1c14 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Case.java @@ -13,7 +13,7 @@ * Case. * */ -public class Case extends BranchImp implements ExpressionContainer { +public class Case extends SwitchBranch implements ExpressionContainer { /** * Expression. diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java index 6536464ed76..ceb807cb9cf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Default.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.java.Statement; import de.uka.ilkd.key.java.visitor.Visitor; @@ -14,7 +15,7 @@ * Default. * */ -public class Default extends BranchImp { +public class Default extends SwitchBranch { /** * Body. @@ -62,6 +63,11 @@ public int getChildCount() { return result; } + @Override + public SourceElement getFirstElement() { + return body.get(0); + } + /** * Returns the child at the specified index in this node's "virtual" child array * diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java index 32774cb8f19..a10bd75928d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Exec.java @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -16,7 +16,7 @@ * * @author AutoDoc */ -public class Exec extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Exec extends BranchStatement implements StatementContainer, PossibleProgramPrefix { /** * Body. @@ -92,20 +92,20 @@ public Exec(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -120,8 +120,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java index 845af967733..514d619c291 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LabeledStatement.java @@ -6,8 +6,8 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.ProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -16,7 +16,7 @@ * Labeled statement. */ public class LabeledStatement extends JavaStatement - implements StatementContainer, NamedProgramElement, ProgramPrefix { + implements StatementContainer, NamedProgramElement, PossibleProgramPrefix { /** * Name. @@ -94,10 +94,11 @@ public LabeledStatement(Label id, Statement statement, PositionInfo pos) { @Override public boolean hasNextPrefixElement() { - if (body instanceof ProgramPrefix) { + if (body instanceof PossibleProgramPrefix) { if (body instanceof StatementBlock) { return !((StatementBlock) body).isEmpty() - && ((StatementBlock) body).getStatementAt(0) instanceof ProgramPrefix; + && ((StatementBlock) body) + .getStatementAt(0) instanceof PossibleProgramPrefix; } return true; } @@ -105,9 +106,9 @@ public boolean hasNextPrefixElement() { } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) (body instanceof StatementBlock + return (PossibleProgramPrefix) (body instanceof StatementBlock ? ((StatementBlock) body).getStatementAt(0) : body); } else { @@ -116,16 +117,16 @@ public ProgramPrefix getNextPrefixElement() { } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @Override - public ImmutableArray getPrefixElements() { + public ImmutableArray getPrefixElements() { if (body instanceof StatementBlock) { - return StatementBlock.computePrefixElements(((StatementBlock) body).getBody(), this); - } else if (body instanceof ProgramPrefix) { - return StatementBlock.computePrefixElements(new ImmutableArray<>(body), this); + return StatementBlock.computePrefixElements(this); + } else if (body instanceof PossibleProgramPrefix) { + return StatementBlock.computePrefixElements(this); } return new ImmutableArray<>(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java index 60d71b65f31..4e20d49c900 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/LoopScopeBlock.java @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; @@ -19,7 +19,7 @@ * @author Dominic Scheurer */ public class LoopScopeBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { protected final IProgramVariable indexPV; protected final StatementBlock body; @@ -72,20 +72,20 @@ public LoopScopeBlock(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -100,8 +100,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java index 69a6d5bf378..39a1f4307a8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/MethodFrame.java @@ -7,7 +7,7 @@ import de.uka.ilkd.key.java.reference.IExecutionContext; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.IProgramMethod; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.util.Debug; @@ -18,7 +18,7 @@ * The statement inserted by KeY if a method call is executed. */ public class MethodFrame extends JavaStatement - implements StatementContainer, ProgramPrefix { + implements StatementContainer, PossibleProgramPrefix { /** * result @@ -94,20 +94,20 @@ public MethodFrame(IProgramVariable resultVar, IExecutionContext execContext, @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -122,8 +122,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } public PosInProgram getFirstActiveChildPos() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java index 3816e6f9282..04eb64056c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Switch.java @@ -4,7 +4,13 @@ package de.uka.ilkd.key.java.statement; import de.uka.ilkd.key.java.*; +import de.uka.ilkd.key.java.expression.Literal; +import de.uka.ilkd.key.java.reference.ExecutionContext; +import de.uka.ilkd.key.java.reference.MetaClassReference; import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.PosInProgram; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; +import de.uka.ilkd.key.logic.op.ProgramVariable; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -14,7 +20,7 @@ */ public class Switch extends BranchStatement - implements ExpressionContainer, VariableScope, TypeScope { + implements ExpressionContainer, VariableScope, TypeScope, PossibleProgramPrefix { /** * Branches. @@ -28,7 +34,9 @@ public class Switch extends BranchStatement protected final Expression expression; + private final int prefixLength; + private final MethodFrame innerMostMethodFrame; /** * Switch. @@ -37,6 +45,8 @@ public class Switch extends BranchStatement public Switch() { this.branches = null; this.expression = null; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -48,6 +58,8 @@ public Switch() { public Switch(Expression e) { this.branches = null; this.expression = e; + prefixLength = 0; + innerMostMethodFrame = null; } /** @@ -60,6 +72,26 @@ public Switch(Expression e) { public Switch(Expression e, Branch[] branches) { this.branches = new ImmutableArray<>(branches); this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public Switch(Expression e, ImmutableArray branches) { + this.branches = branches; + this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); + } + + public Switch(PositionInfo pos, Expression e, Branch[] branches) { + super(pos); + this.branches = new ImmutableArray<>(branches); + this.expression = e; + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } /** @@ -70,8 +102,11 @@ public Switch(Expression e, Branch[] branches) { public Switch(ExtList children) { super(children); - this.expression = children.get(Expression.class); + this.expression = children.removeFirstOccurrence(Expression.class); this.branches = new ImmutableArray<>(children.collect(Branch.class)); + ProgramPrefixUtil.ProgramPrefixInfo info = ProgramPrefixUtil.computeEssentials(this); + prefixLength = info.getLength(); + innerMostMethodFrame = info.getInnerMostMethodFrame(); } @@ -188,6 +223,13 @@ public ImmutableArray getBranchList() { return branches; } + @Override + public SourceElement getFirstElement() { + if (branches.isEmpty()) + return this; + return branches.get(0); + } + /** * calls the corresponding method of a visitor in order to perform some action/transformation on * this element @@ -197,4 +239,65 @@ public ImmutableArray getBranchList() { public void visit(Visitor v) { v.performActionOnSwitch(this); } + + @Override + public boolean isPrefix() { + return !branches.isEmpty() && expressionWithoutSideffects(); + } + + @Override + public boolean hasNextPrefixElement() { + return !branches.isEmpty() && branches.get(0) instanceof PossibleProgramPrefix; + } + + @Override + public PossibleProgramPrefix getNextPrefixElement() { + if (hasNextPrefixElement()) { + return (PossibleProgramPrefix) branches.get(0); + } else { + throw new IndexOutOfBoundsException("No next prefix element " + this); + } + } + + @Override + public PossibleProgramPrefix getLastPrefixElement() { + return hasNextPrefixElement() + ? ((PossibleProgramPrefix) branches.get(0)).getLastPrefixElement() + : this; + } + + @Override + public int getPrefixLength() { + return prefixLength; + } + + @Override + public MethodFrame getInnerMostMethodFrame() { + return innerMostMethodFrame; + } + + @Override + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); + } + + /** + * The method checks whether the expression in the synchronized prefix is either a local + * variable or a meta class reference (as local variables of this type are not supported by KeY, + * see return value for {@link MetaClassReference#getKeYJavaType(Services, ExecutionContext)}. + * + * @return true iff the above stated condition holds. + */ + private boolean expressionWithoutSideffects() { + return (expression instanceof ProgramVariable && !((ProgramVariable) expression).isMember()) + || (expression instanceof MetaClassReference) || expression instanceof Literal; + } + + @Override + public PosInProgram getFirstActiveChildPos() { + return branches.isEmpty() ? PosInProgram.TOP + : (expressionWithoutSideffects() + ? PosInProgram.ONE + : PosInProgram.TOP); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java new file mode 100644 index 00000000000..71c9e3a538d --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranch.java @@ -0,0 +1,22 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.PositionInfo; + +import org.key_project.util.ExtList; + +public abstract class SwitchBranch extends BranchImp { + public SwitchBranch() { + super(); + } + + public SwitchBranch(ExtList children) { + super(children); + } + + public SwitchBranch(ExtList children, PositionInfo pos) { + super(children, pos); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java new file mode 100644 index 00000000000..5b2eaa28bf1 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SwitchBranchSVWrapper.java @@ -0,0 +1,59 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.java.statement; + +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.SourceData; +import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.visitor.Visitor; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.rule.MatchConditions; + +public class SwitchBranchSVWrapper extends SwitchBranch { + private final ProgramSV sv; + + public SwitchBranchSVWrapper(ProgramSV sv) { + this.sv = sv; + } + + public ProgramSV getSv() { + return sv; + } + + + @Override + public int getChildCount() { + return 0; + } + + @Override + public ProgramElement getChildAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public void visit(Visitor v) { + + } + + @Override + public int getStatementCount() { + return 0; + } + + @Override + public Statement getStatementAt(int index) { + throw new IndexOutOfBoundsException(); + } + + @Override + public String toString() { + return sv.toString(); + } + + @Override + public MatchConditions match(SourceData source, MatchConditions matchCond) { + return sv.match(source, matchCond); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java index 492cfc5b683..33fc58405b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/SynchronizedBlock.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.java.reference.MetaClassReference; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.ProgramVariable; import org.key_project.util.ExtList; @@ -19,7 +19,7 @@ */ public class SynchronizedBlock extends JavaStatement - implements StatementContainer, ExpressionContainer, ProgramPrefix { + implements StatementContainer, ExpressionContainer, PossibleProgramPrefix { /** * Expression. @@ -86,22 +86,27 @@ public SynchronizedBlock(ExtList children) { } + @Override + public boolean isPrefix() { + return expressionWithoutSideffects(); + } + @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -116,8 +121,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java index 02386a7c6e9..27a93342c8c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/statement/Try.java @@ -6,7 +6,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.PosInProgram; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -16,7 +16,7 @@ * * @author AutoDoc */ -public class Try extends BranchStatement implements StatementContainer, ProgramPrefix { +public class Try extends BranchStatement implements StatementContainer, PossibleProgramPrefix { /** * Body. @@ -98,20 +98,20 @@ public Try(ExtList children) { @Override public boolean hasNextPrefixElement() { - return !body.isEmpty() && body.getStatementAt(0) instanceof ProgramPrefix; + return !body.isEmpty() && body.getStatementAt(0) instanceof PossibleProgramPrefix; } @Override - public ProgramPrefix getNextPrefixElement() { + public PossibleProgramPrefix getNextPrefixElement() { if (hasNextPrefixElement()) { - return (ProgramPrefix) body.getStatementAt(0); + return (PossibleProgramPrefix) body.getStatementAt(0); } else { throw new IndexOutOfBoundsException("No next prefix element " + this); } } @Override - public ProgramPrefix getLastPrefixElement() { + public PossibleProgramPrefix getLastPrefixElement() { return hasNextPrefixElement() ? getNextPrefixElement().getLastPrefixElement() : this; } @@ -126,8 +126,8 @@ public MethodFrame getInnerMostMethodFrame() { } @Override - public ImmutableArray getPrefixElements() { - return StatementBlock.computePrefixElements(body.getBody(), this); + public ImmutableArray getPrefixElements() { + return StatementBlock.computePrefixElements(this); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java index 7a0e26f1fca..701196d8461 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java @@ -357,6 +357,22 @@ ProgramElement createNewElement(ExtList changeList) { def.doAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + ExtList changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + PositionInfo pi = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pi = PositionInfo.UNDEFINED; + } + addChild(new ActiveCase(changeList, pi)); + changed(); + } else { + doDefaultAction(x); + } + } + // eee @Override public void performActionOnCase(Case x) { @@ -1221,13 +1237,22 @@ ProgramElement createNewElement(ExtList changeList) { @Override public void performActionOnSwitch(Switch x) { - DefaultAction def = new DefaultAction(x) { - @Override - ProgramElement createNewElement(ExtList changeList) { - return new Switch(changeList); + var changeList = stack.peek(); + if (changeList.getFirst() == CHANGED) { + changeList.removeFirst(); + var pos = changeList.removeFirstOccurrence(PositionInfo.class); + if (!preservesPositionInfo) { + pos = PositionInfo.UNDEFINED; } - }; - def.doAction(x); + Expression expr = changeList.removeFirstOccurrence(Expression.class); + var branches = changeList.collect(SwitchBranch.class); + changeList.clear(); + var sw = new Switch(pos, expr, branches); + addChild(sw); + changed(); + } else { + doDefaultAction(x); + } } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java index b7855e66b08..297c6b30748 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java @@ -262,6 +262,11 @@ public void performActionOnCase(Case x) { doDefaultAction(x); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + doDefaultAction(x); + } + @Override public void performActionOnCatch(Catch x) { doDefaultAction(x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index 106d3bca3ed..0f4a74b34e6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java @@ -5,17 +5,9 @@ import java.rmi.UnexpectedException; -import de.uka.ilkd.key.java.JavaNonTerminalProgramElement; -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.Statement; -import de.uka.ilkd.key.java.StatementBlock; +import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration; -import de.uka.ilkd.key.java.statement.Exec; -import de.uka.ilkd.key.java.statement.LabeledStatement; -import de.uka.ilkd.key.java.statement.LoopScopeBlock; -import de.uka.ilkd.key.java.statement.MethodFrame; -import de.uka.ilkd.key.java.statement.SynchronizedBlock; -import de.uka.ilkd.key.java.statement.Try; +import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.PosInProgram; import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation; @@ -59,30 +51,36 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte if (!prefixPos.hasNext()) { body = createWrapperBody(context, putIn, suffix); - // special case labeled statement as a label must not be + // special case labeled statement as a label need not be // succeeded by a statement block if (context instanceof LabeledStatement) { body = createLabeledStatementWrapper((LabeledStatement) context, body); + } else if (context instanceof ActiveCase ac) { + body = createActiveCaseWrapper(ac, (StatementBlock) body); } return body; } else { body = wrap((JavaNonTerminalProgramElement) next, putIn, prefixPos, prefixDepth, prefix, suffix); - if (context instanceof StatementBlock) { - return createStatementBlockWrapper((StatementBlock) context, body); - } else if (context instanceof Try) { - return createTryStatementWrapper((StatementBlock) body, (Try) context); - } else if (context instanceof MethodFrame) { - return createMethodFrameWrapper((MethodFrame) context, (StatementBlock) body); - } else if (context instanceof LabeledStatement) { - return createLabeledStatementWrapper((LabeledStatement) context, body); - } else if (context instanceof LoopScopeBlock) { - return createLoopScopeBlockWrapper((LoopScopeBlock) context, (StatementBlock) body); - } else if (context instanceof SynchronizedBlock) { - return createSynchronizedBlockWrapper((SynchronizedBlock) context, + if (context instanceof StatementBlock block) { + return createStatementBlockWrapper(block, body); + } else if (context instanceof Try t) { + return createTryStatementWrapper(t, (StatementBlock) body); + } else if (context instanceof MethodFrame mf) { + return createMethodFrameWrapper(mf, (StatementBlock) body); + } else if (context instanceof LabeledStatement ls) { + return createLabeledStatementWrapper(ls, body); + } else if (context instanceof LoopScopeBlock lsb) { + return createLoopScopeBlockWrapper(lsb, (StatementBlock) body); + } else if (context instanceof SynchronizedBlock sb) { + return createSynchronizedBlockWrapper(sb, (StatementBlock) body); - } else if (context instanceof Exec) { - return createExecStatementWrapper((StatementBlock) body, (Exec) context); + } else if (context instanceof Exec e) { + return createExecStatementWrapper(e, (StatementBlock) body); + } else if (context instanceof Switch sw) { + return createSwitchWrapper(sw, (ActiveCase) body); + } else if (context instanceof ActiveCase ac) { + return createActiveCaseWrapper(ac, (Statement) body); } else { throw new RuntimeException( new UnexpectedException("Unexpected block type: " + context.getClass())); @@ -92,7 +90,7 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte /** * inserts the content of the statement block putIn and adds succeeding children of - * the innermost non terminal element (usually statement block) in the context. + * the innermost non-terminal element (usually statement block) in the context. * * @param wrapper the JavaNonTerminalProgramElement with the context that has to be wrapped * around the content of putIn @@ -144,7 +142,7 @@ private final StatementBlock createWrapperBody(JavaNonTerminalProgramElement wra /** * Replaces the first statement in the wrapper block. The replacement is optimized as it just * returns the replacement block if it is the only child of the statement block to be - * constructed and the chld is a statementblock too. + * constructed and the child is a statementblock too. * * @param wrapper the StatementBlock where to replace the first statement * @param replacement the StatementBlock that replaces the first statement of the block @@ -166,11 +164,31 @@ protected StatementBlock createStatementBlockWrapper(StatementBlock wrapper, } } - protected Try createTryStatementWrapper(StatementBlock body, Try old) { + protected Try createTryStatementWrapper(Try old, StatementBlock body) { return new Try(body, old.getBranchList()); } - protected Exec createExecStatementWrapper(StatementBlock body, Exec old) { + protected ActiveCase createActiveCaseWrapper(ActiveCase old, Statement body) { + var stmts = old.getBody().toArray(new Statement[0]); + if (body instanceof StatementBlock bodyBlock) { + if (stmts[0] instanceof StatementBlock sb && !sb.isEmpty()) { + stmts[0] = bodyBlock; + } else { + stmts = bodyBlock.getBody().toArray(new Statement[0]); + } + } else { + stmts[0] = body; + } + return new ActiveCase(stmts); + } + + protected Switch createSwitchWrapper(Switch old, ActiveCase body) { + var branches = old.getBranchList().toArray(new Branch[0]); + branches[0] = body; + return new Switch(old.getExpression(), branches); + } + + protected Exec createExecStatementWrapper(Exec old, StatementBlock body) { return new Exec(body, old.getBranchList()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java index 8f9eb8665c2..7b9b2e127b9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/Visitor.java @@ -304,6 +304,8 @@ public interface Visitor { void performActionOnCase(Case x); + void performActionOnActiveCase(ActiveCase x); + void performActionOnCatch(Catch x); void performActionOnDefault(Default x); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java index a2f0aa31ffc..382e118eaaf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java @@ -29,9 +29,9 @@ public MethodStackInfo(ProgramElement element) { */ public ImmutableList getMethodStack() { ImmutableList list = ImmutableSLList.nil(); - if (element instanceof ProgramPrefix) { - final ImmutableArray prefix = - ((ProgramPrefix) element).getPrefixElements(); + if (element instanceof PossibleProgramPrefix) { + final ImmutableArray prefix = + ((PossibleProgramPrefix) element).getPrefixElements(); for (int i = prefix.size() - 1; i >= 0; i--) { if (prefix.get(i) instanceof MethodFrame frame) { IProgramMethod method = frame.getProgramMethod(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java b/key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java similarity index 79% rename from key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java rename to key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java index c7881fa958e..dc6ed07fc0b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/PossibleProgramPrefix.java @@ -12,7 +12,9 @@ * this interface is implemented by program elements that may be matched by the inactive program * prefix */ -public interface ProgramPrefix extends NonTerminalProgramElement { +public interface PossibleProgramPrefix extends NonTerminalProgramElement { + + default boolean isPrefix() { return true; } /** return true if there is a next prefix element */ boolean hasNextPrefixElement(); @@ -21,15 +23,15 @@ public interface ProgramPrefix extends NonTerminalProgramElement { * return the next prefix element if no next prefix element is available an * IndexOutOfBoundsException is thrown */ - ProgramPrefix getNextPrefixElement(); + PossibleProgramPrefix getNextPrefixElement(); /** return the last prefix element */ - ProgramPrefix getLastPrefixElement(); + PossibleProgramPrefix getLastPrefixElement(); /** * returns an array with all prefix elements starting at this element */ - ImmutableArray getPrefixElements(); + ImmutableArray getPrefixElements(); /** returns the position of the first active child */ PosInProgram getFirstActiveChildPos(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java index c56513e2fb4..c1d41612582 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java @@ -31,14 +31,7 @@ import de.uka.ilkd.key.java.expression.operator.NewArray; import de.uka.ilkd.key.java.expression.operator.adt.*; import de.uka.ilkd.key.java.reference.*; -import de.uka.ilkd.key.java.statement.Catch; -import de.uka.ilkd.key.java.statement.Ccatch; -import de.uka.ilkd.key.java.statement.For; -import de.uka.ilkd.key.java.statement.ForUpdates; -import de.uka.ilkd.key.java.statement.Guard; -import de.uka.ilkd.key.java.statement.LoopInit; -import de.uka.ilkd.key.java.statement.MethodBodyStatement; -import de.uka.ilkd.key.java.statement.Switch; +import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.op.*; @@ -249,7 +242,7 @@ public abstract class ProgramSVSort extends SortImpl { public static final ProgramSVSort ARRAYPOSTDECL = new ArrayPostDeclarationSort(); - public static final ProgramSVSort SWITCH = new SwitchSVSort(); + public static final ProgramSVSort SWITCH_BRANCH = new SwitchBranchSVSort(); public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE = new ConstantProgramVariableSort(new Name("ConstantPrimitiveTypeVariable"), false); @@ -1219,15 +1212,12 @@ protected boolean canStandFor(ProgramElement check, Services services) { } } - private static final class SwitchSVSort extends ProgramSVSort { - - public SwitchSVSort() { - super(new Name("Switch")); - } + private static final class SwitchBranchSVSort extends ProgramSVSort { + public SwitchBranchSVSort() { super(new Name("SwitchBranch")); } @Override protected boolean canStandFor(ProgramElement pe, Services services) { - return (pe instanceof Switch); + return (pe instanceof Case) || (pe instanceof Default); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java index df7141b3eea..42521796c7d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/pp/PrettyPrinter.java @@ -32,8 +32,8 @@ import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.java.visitor.Visitor; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.ProgramElementName; -import de.uka.ilkd.key.logic.ProgramPrefix; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.AbstractProgramElement; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -856,7 +856,8 @@ public void performActionOnClassInitializer(ClassInitializer x) { protected void performActionOnStatement(SourceElement s) { layouter.beginRelativeC(0); - boolean validStatement = !(s instanceof CatchAllStatement || s instanceof ProgramPrefix); + boolean validStatement = !(s instanceof CatchAllStatement + || (s instanceof PossibleProgramPrefix pre && pre.isPrefix())); if (validStatement) { markStart(s); } @@ -1719,7 +1720,7 @@ public void performActionOnElse(Else x) { } } - private void printCaseBody(ImmutableArray body) { + private void printCaseBody(ImmutableArray body) { if (body != null && !body.isEmpty()) { for (int i = 0; i < body.size(); i++) { Statement statement = body.get(i); @@ -1773,6 +1774,16 @@ public void performActionOnDefault(Default x) { printCaseBody(x.getBody()); } + @Override + public void performActionOnActiveCase(ActiveCase x) { + if (!x.isPrefix()) + markStart(x); + layouter.keyWord("active-case").print(":"); + printCaseBody(x.getBody()); + if (!x.isPrefix()) + markEnd(x); + } + @Override public void performActionOnFinally(Finally x) { layouter.print(" "); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java index c6f08143795..706d96cdef4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.java.StatementBlock; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.TermLabelManager; import de.uka.ilkd.key.logic.op.LocationVariable; @@ -192,7 +192,7 @@ public static SourceElement computeActiveStatement(SourceElement firstStatement) // TODO: unify with MiscTools getActiveStatement if (firstStatement != null) { activeStatement = firstStatement; - while ((activeStatement instanceof ProgramPrefix) + while ((activeStatement instanceof PossibleProgramPrefix pre && pre.isPrefix()) && !(activeStatement instanceof StatementBlock)) { activeStatement = activeStatement.getFirstElement(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java index 21df139cf98..cee8e97327d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/TacletIndex.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.java.*; import de.uka.ilkd.key.java.statement.*; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.logic.sort.GenericSort; import de.uka.ilkd.key.rule.*; @@ -303,7 +303,7 @@ private ImmutableList getJavaTacletList( HashMap> map, ProgramElement pe, PrefixOccurrences prefixOccurrences) { ImmutableList res = ImmutableSLList.nil(); - if (pe instanceof ProgramPrefix nt) { + if (pe instanceof PossibleProgramPrefix nt) { int next = prefixOccurrences.occurred(pe); if (next < nt.getChildCount()) { return getJavaTacletList(map, nt.getChildAt(next), prefixOccurrences); @@ -555,7 +555,8 @@ private static class PrefixOccurrences { */ static final Class[] prefixClasses = new Class[] { StatementBlock.class, LabeledStatement.class, Try.class, - MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class }; + MethodFrame.class, SynchronizedBlock.class, LoopScopeBlock.class, Exec.class, + Switch.class, ActiveCase.class }; /** * number of prefix types @@ -571,7 +572,7 @@ private static class PrefixOccurrences { * fields to indicate the position of the next relevant child (the next possible prefix * element or real statement */ - static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0 }; + static final int[] nextChild = { 0, 1, 0, 1, 1, 1, 0, 1, 0 }; PrefixOccurrences() { reset(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java index c3b87a53c08..7ac65f39941 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java @@ -17,7 +17,7 @@ import de.uka.ilkd.key.java.statement.MethodFrame; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Goal; @@ -296,9 +296,8 @@ private static ExecutionContext extractExecutionContext(final MethodFrame frame) private JavaStatement getFirstStatementInPrefixWithAtLeastOneApplicableContract( final JModality modality, final Goal goal) { SourceElement element = modality.programBlock().program().getFirstElement(); - while ((element instanceof ProgramPrefix || element instanceof CatchAllStatement) - && !(element instanceof StatementBlock - && ((StatementBlock) element).isEmpty())) { + while ((element instanceof PossibleProgramPrefix pre && pre.isPrefix() + || element instanceof CatchAllStatement)) { if (element instanceof StatementBlock && hasApplicableContracts(services, (StatementBlock) element, modality.kind(), goal)) { return (StatementBlock) element; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java index f47cbf3f6b4..48c68afc1d2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/LoopScopeInvariantRule.java @@ -14,7 +14,7 @@ import de.uka.ilkd.key.java.visitor.ProgramElementReplacer; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.JavaBlock; -import de.uka.ilkd.key.logic.ProgramPrefix; +import de.uka.ilkd.key.logic.PossibleProgramPrefix; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.ParameterlessTermLabel; import de.uka.ilkd.key.logic.label.TermLabelManager; @@ -402,7 +402,7 @@ private Pair, Statement> findLoopLabel( Optional