Skip to content

Commit 3ffa09d

Browse files
wadoonwadoon
authored
Merge branch 'main' into weigl/pckgreworked
2 parents b54fa5b + 27f5bed commit 3ffa09d

89 files changed

Lines changed: 1585 additions & 515 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎build.gradle‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,8 @@ plugins {
2424
id "com.diffplug.spotless" version "6.25.0"
2525

2626
// EISOP Checker Framework
27-
id "org.checkerframework" version "0.6.39"
27+
28+
id "org.checkerframework" version "0.6.41"
2829

2930
id("org.sonarqube") version "5.0.0.4638"
3031
}
@@ -104,11 +105,11 @@ subprojects {
104105
checkerFramework "io.github.eisop:checker:$eisop_version"
105106

106107
testImplementation("ch.qos.logback:logback-classic:1.5.6")
107-
testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2'
108-
testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2'
108+
testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3'
109+
testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3'
109110
testImplementation project(':key.util')
110111

111-
testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2'
112+
testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3'
112113
}
113114

114115
tasks.withType(JavaCompile) {

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@
7676
import org.slf4j.LoggerFactory;
7777

7878
import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY;
79-
import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
79+
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
8080

8181
/**
8282
* Provides utility methods for symbolic execution with KeY.
@@ -2686,7 +2686,7 @@ private static boolean checkReplaceTerm(Term toCheck, PosInOccurrence posInOccur
26862686
Term replaceTerm) {
26872687
Term termAtPio = followPosInOccurrence(posInOccurrence, toCheck);
26882688
if (termAtPio != null) {
2689-
return termAtPio.equalsModProperty(replaceTerm, RENAMING_PROPERTY);
2689+
return termAtPio.equalsModProperty(replaceTerm, RENAMING_TERM_PROPERTY);
26902690
} else {
26912691
return false;
26922692
}

‎key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@
2424

2525
import org.key_project.util.collection.ImmutableList;
2626

27-
import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
27+
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
2828

2929

3030
/**
@@ -80,7 +80,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
8080
final Term selfComposedExec =
8181
f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_BLOCK_WITH_PRE_RELATION);
8282

83-
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
83+
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
8484
}
8585

8686
@Override

‎key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@
2525

2626
import org.key_project.util.collection.ImmutableList;
2727

28-
import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
28+
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
2929

3030
public class StartAuxiliaryLoopComputationMacro extends AbstractProofMacro
3131
implements StartSideProofMacro {
@@ -77,7 +77,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
7777
final Term selfComposedExec =
7878
f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_LOOP_WITH_INV_RELATION);
7979

80-
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
80+
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
8181
}
8282

8383
@Override

‎key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222

2323
import org.key_project.util.collection.ImmutableList;
2424

25-
import static de.uka.ilkd.key.logic.equality.RenamingProperty.RENAMING_PROPERTY;
25+
import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY;
2626

2727
/**
2828
*
@@ -69,7 +69,7 @@ public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrenc
6969
final Term selfComposedExec =
7070
f.create(InfFlowPOSnippetFactory.Snippet.SELFCOMPOSED_EXECUTION_WITH_PRE_RELATION);
7171

72-
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_PROPERTY);
72+
return posInOcc.subTerm().equalsModProperty(selfComposedExec, RENAMING_TERM_PROPERTY);
7373
}
7474

7575
@Override

‎key.core/src/main/java/de/uka/ilkd/key/java/Comment.java‎

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -45,25 +45,19 @@ public String getText() {
4545
return text;
4646
}
4747

48-
48+
@Override
4949
public String toString() {
5050
return getText();
5151
}
5252

53-
54-
/**
55-
* comments can be ignored
56-
*/
57-
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
58-
return true;
59-
}
60-
53+
@Override
6154
public int hashCode() {
6255
int result = 17;
6356
result = 37 * result + getText().hashCode();
6457
return result;
6558
}
6659

60+
@Override
6761
public boolean equals(Object o) {
6862
if (o == this) {
6963
return true;

‎key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java‎

Lines changed: 7 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -55,37 +55,28 @@ protected int getArrayPos(ImmutableArray<ProgramElement> arr, ProgramElement el)
5555
return -1;
5656
}
5757

58-
59-
/**
60-
* commented in interface SourceElement. Overwrites the default method implementation in
61-
* ProgramElement by descending down to the children.
62-
*/
63-
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
64-
65-
if (se == this) {
58+
@Override
59+
public boolean equals(Object o) {
60+
if (o == this) {
6661
return true;
67-
} else if (se == null || this.getClass() != se.getClass()) {
62+
}
63+
if (o == null || o.getClass() != this.getClass()) {
6864
return false;
6965
}
7066

71-
final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) se;
67+
final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) o;
7268
if (jnte.getChildCount() != getChildCount()) {
7369
return false;
7470
}
7571

7672
for (int i = 0, cc = getChildCount(); i < cc; i++) {
77-
if (!getChildAt(i).equalsModRenaming(jnte.getChildAt(i), nat)) {
73+
if (!getChildAt(i).equals(jnte.getChildAt(i))) {
7874
return false;
7975
}
8076
}
8177
return true;
8278
}
8379

84-
@Override
85-
public boolean equals(Object o) {
86-
return super.equals(o);
87-
}
88-
8980
@Override
9081
protected int computeHashCode() {
9182
int localHash = 17 * super.computeHashCode();

‎key.core/src/main/java/de/uka/ilkd/key/java/JavaProgramElement.java‎

Lines changed: 2 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -78,16 +78,6 @@ public Comment[] getComments() {
7878
return comments;
7979
}
8080

81-
82-
/**
83-
* commented in interface SourceElement. The default equals method compares two elements by
84-
* testing if they have the same type and calling the default equals method.
85-
*/
86-
@Override
87-
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
88-
return (this.getClass() == se.getClass());
89-
}
90-
9181
protected int computeHashCode() {
9282
int result = 17 * this.getClass().hashCode();
9383
return result;
@@ -114,11 +104,10 @@ public boolean equals(Object o) {
114104
if (o == this) {
115105
return true;
116106
}
117-
if (o == null || o.getClass() != this.getClass()) {
107+
if (o == null) {
118108
return false;
119109
}
120-
121-
return equalsModRenaming((JavaProgramElement) o, NameAbstractionTableDisabled.INSTANCE);
110+
return (this.getClass() == o.getClass());
122111
}
123112

124113

‎key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@
44
package de.uka.ilkd.key.java;
55

66
import de.uka.ilkd.key.java.visitor.Visitor;
7+
import de.uka.ilkd.key.logic.equality.EqualsModProperty;
8+
import de.uka.ilkd.key.logic.equality.Property;
79

810
import org.key_project.logic.SyntaxElement;
911

@@ -13,7 +15,7 @@
1315
* to achieve an immutable structure
1416
*/
1517

16-
public interface SourceElement extends SyntaxElement {
18+
public interface SourceElement extends SyntaxElement, EqualsModProperty<SourceElement> {
1719

1820

1921
/**
@@ -93,8 +95,16 @@ public interface SourceElement extends SyntaxElement {
9395
* seen as {int decl_1; decl_1=0;} for the first one but {int decl_1; i=0;} for the second one.
9496
* These are not syntactical equal, therefore false is returned.
9597
*/
96-
boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat);
97-
98-
99-
98+
@Override
99+
default <V> boolean equalsModProperty(Object o, Property<SourceElement> property, V... v) {
100+
if (!(o instanceof SourceElement)) {
101+
return false;
102+
}
103+
return property.equalsModThisProperty(this, (SourceElement) o, v);
104+
}
105+
106+
@Override
107+
default int hashCodeModProperty(Property<SourceElement> property) {
108+
return property.hashCodeModThisProperty(this);
109+
}
100110
}

‎key.core/src/main/java/de/uka/ilkd/key/java/StatementBlock.java‎

Lines changed: 28 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@
2020
/**
2121
* Statement block. taken from COMPOST and changed to achieve an immutable structure
2222
*/
23-
2423
public class StatementBlock extends JavaStatement implements StatementContainer,
2524
TypeDeclarationContainer, VariableScope, TypeScope, ProgramPrefix {
2625

@@ -46,7 +45,6 @@ public StatementBlock() {
4645
*
4746
* @param children an ExtList that contains the children
4847
*/
49-
5048
public StatementBlock(ExtList children) {
5149
super(children);
5250
body = new ImmutableArray<>(children.collect(Statement.class));
@@ -75,13 +73,32 @@ public StatementBlock(Statement... body) {
7573
}
7674

7775
@Override
78-
public boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat) {
79-
return super.equalsModRenaming(se, nat)
80-
&& (this.getStartPosition().equals(Position.UNDEFINED) || // why do we care here
81-
// about position info and
82-
// nowhere else?
83-
se.getStartPosition().equals(Position.UNDEFINED)
84-
|| this.getStartPosition().line() == se.getStartPosition().line());
76+
public boolean equals(Object o) {
77+
if (o == this) {
78+
return true;
79+
}
80+
if (o == null || o.getClass() != this.getClass()) {
81+
return false;
82+
}
83+
84+
final JavaNonTerminalProgramElement jnte = (JavaNonTerminalProgramElement) o;
85+
if (jnte.getChildCount() != getChildCount()) {
86+
return false;
87+
}
88+
89+
for (int i = 0, cc = getChildCount(); i < cc; i++) {
90+
if (!getChildAt(i).equals(jnte.getChildAt(i))) {
91+
return false;
92+
}
93+
}
94+
95+
return (this.getStartPosition().equals(Position.UNDEFINED) || // why do we care here
96+
// about position info and
97+
// nowhere else?
98+
// We also care in
99+
// LoopStatement
100+
jnte.getStartPosition().equals(Position.UNDEFINED)
101+
|| this.getStartPosition().line() == jnte.getStartPosition().line());
85102
}
86103

87104
/** computes the prefix elements for the given array of statment block */
@@ -98,14 +115,11 @@ public static ImmutableArray<ProgramPrefix> computePrefixElements(
98115
return new ImmutableArray<>(prefix);
99116
}
100117

101-
102-
103118
/**
104119
* Get body.
105120
*
106121
* @return the statement array wrapper.
107122
*/
108-
109123
public ImmutableArray<? extends Statement> getBody() {
110124
return body;
111125
}
@@ -114,13 +128,11 @@ public final boolean isEmpty() {
114128
return body.isEmpty();
115129
}
116130

117-
118131
/**
119132
* Returns the number of children of this node.
120133
*
121134
* @return an int giving the number of children of this node
122135
*/
123-
124136
public int getChildCount() {
125137
return body.size();
126138
}
@@ -132,7 +144,6 @@ public int getChildCount() {
132144
* @return the program element at the given position
133145
* @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds
134146
*/
135-
136147
public ProgramElement getChildAt(int index) {
137148
if (body != null) {
138149
return body.get(index);
@@ -145,12 +156,11 @@ public ProgramElement getChildAt(int index) {
145156
*
146157
* @return the number of statements.
147158
*/
148-
149159
public int getStatementCount() {
150160
return body.size();
151161
}
152162

153-
/*
163+
/**
154164
* Return the statement at the specified index in this node's "virtual" statement array.
155165
*
156166
* @param index an index for a statement.
@@ -159,7 +169,6 @@ public int getStatementCount() {
159169
*
160170
* @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds.
161171
*/
162-
163172
public Statement getStatementAt(int index) {
164173
if (body != null) {
165174
return body.get(index);
@@ -172,7 +181,6 @@ public Statement getStatementAt(int index) {
172181
*
173182
* @return the number of type declarations.
174183
*/
175-
176184
public int getTypeDeclarationCount() {
177185
int count = 0;
178186
if (body != null) {
@@ -185,7 +193,7 @@ public int getTypeDeclarationCount() {
185193
return count;
186194
}
187195

188-
/*
196+
/**
189197
* Return the type declaration at the specified index in this node's "virtual" type declaration
190198
* array.
191199
*
@@ -195,7 +203,6 @@ public int getTypeDeclarationCount() {
195203
*
196204
* @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds.
197205
*/
198-
199206
public TypeDeclaration getTypeDeclarationAt(int index) {
200207
if (body != null) {
201208
int s = body.size();
@@ -222,7 +229,6 @@ public void visit(Visitor v) {
222229
v.performActionOnStatementBlock(this);
223230
}
224231

225-
226232
public SourceElement getFirstElement() {
227233
if (isEmpty()) {
228234
return this;
@@ -240,7 +246,6 @@ public SourceElement getFirstElementIncludingBlocks() {
240246
}
241247
}
242248

243-
244249
@Override
245250
public boolean hasNextPrefixElement() {
246251
return body.size() != 0 && (body.get(0) instanceof ProgramPrefix);

0 commit comments

Comments
 (0)