Skip to content

Commit 16907d7

Browse files
committed
removal of TextualJMLConstruct
# Conflicts: # key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java
1 parent b6d4c72 commit 16907d7

48 files changed

Lines changed: 175 additions & 2143 deletions

Some content is hidden

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

key.core/src/main/java/de/uka/ilkd/key/java/ast/ProgramElement.java

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

66

7+
import com.github.javaparser.ast.jml.clauses.JmlContract;
78
import de.uka.ilkd.key.rule.MatchConditions;
8-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
99

1010
import org.key_project.util.collection.ImmutableList;
1111
import org.key_project.util.collection.ImmutableSLList;
@@ -27,7 +27,7 @@ public interface ProgramElement extends SourceElement, ModelElement {
2727
Comment[] getComments();
2828

2929
///
30-
default ImmutableList<TextualJMLConstruct> getAttachedJml() {
30+
default ImmutableList<JmlContract> getAttachedJml() {
3131
return ImmutableSLList.nil();
3232
}
3333

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@
1616
import de.uka.ilkd.key.java.visitor.Visitor;
1717
import de.uka.ilkd.key.logic.PosInProgram;
1818
import de.uka.ilkd.key.logic.ProgramPrefix;
19-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
2019
import de.uka.ilkd.key.util.Debug;
2120

2221
import org.key_project.util.ExtList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ClassDeclaration.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@
1212
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
1313
import de.uka.ilkd.key.java.visitor.Visitor;
1414
import de.uka.ilkd.key.logic.ProgramElementName;
15-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1615

1716
import org.key_project.util.ExtList;
1817
import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/ConstructorDeclaration.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,14 @@
55

66
import java.util.List;
77

8+
import com.github.javaparser.ast.jml.clauses.JmlContract;
89
import de.uka.ilkd.key.java.ast.Comment;
910
import de.uka.ilkd.key.java.ast.PositionInfo;
1011
import de.uka.ilkd.key.java.ast.StatementBlock;
1112
import de.uka.ilkd.key.java.ast.abstraction.Constructor;
1213
import de.uka.ilkd.key.java.ast.reference.TypeReference;
1314
import de.uka.ilkd.key.java.visitor.Visitor;
1415
import de.uka.ilkd.key.logic.ProgramElementName;
15-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1616

1717
import org.key_project.util.ExtList;
1818
import org.key_project.util.collection.ImmutableArray;
@@ -63,7 +63,7 @@ public ConstructorDeclaration(PositionInfo pi, List<Comment> c, ImmutableArray<M
6363
TypeReference o, Comment[] comments, ProgramElementName name,
6464
ImmutableArray<ParameterDeclaration> map1,
6565
Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration,
66-
List<TextualJMLConstruct> specs) {
66+
List<JmlContract> specs) {
6767
super(pi, c, map, o, comments, name, map1, exceptions, body, parentIsInterfaceDeclaration,
6868
ImmutableList.fromList(specs));
6969
}

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/InterfaceDeclaration.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@
2424
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
2525
import de.uka.ilkd.key.java.visitor.Visitor;
2626
import de.uka.ilkd.key.logic.ProgramElementName;
27-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
2827

2928
import org.key_project.util.ExtList;
3029
import org.key_project.util.collection.ImmutableArray;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/JavaDeclaration.java

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,12 +18,12 @@
1818

1919
import java.util.List;
2020

21+
import com.github.javaparser.ast.jml.clauses.JmlContract;
2122
import de.uka.ilkd.key.java.ast.Comment;
2223
import de.uka.ilkd.key.java.ast.Declaration;
2324
import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement;
2425
import de.uka.ilkd.key.java.ast.PositionInfo;
2526
import de.uka.ilkd.key.java.ast.declaration.modifier.*;
26-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
2727

2828
import org.key_project.util.ExtList;
2929
import org.key_project.util.collection.ImmutableArray;
@@ -39,7 +39,7 @@
3939

4040
public abstract class JavaDeclaration extends JavaNonTerminalProgramElement implements Declaration {
4141

42-
protected final ImmutableList<TextualJMLConstruct> attachedJml;
42+
protected final ImmutableList<JmlContract> attachedJml;
4343

4444

4545
/**
@@ -53,7 +53,7 @@ public abstract class JavaDeclaration extends JavaNonTerminalProgramElement impl
5353

5454
public JavaDeclaration(PositionInfo pi, List<Comment> comments,
5555
@NonNull ImmutableArray<Modifier> modArray,
56-
ImmutableList<TextualJMLConstruct> attachedJml) {
56+
ImmutableList<JmlContract> attachedJml) {
5757
super(pi, comments);
5858
this.modArray = modArray;
5959
this.attachedJml = attachedJml;
@@ -89,7 +89,7 @@ public JavaDeclaration(ExtList children) {
8989
super(children);
9090
modArray = new ImmutableArray<>(children.collect(Modifier.class));
9191
this.attachedJml =
92-
ImmutableList.fromList(List.of(children.collect(TextualJMLConstruct.class)));
92+
ImmutableList.fromList(List.of(children.collect(JmlContract.class)));
9393
}
9494

9595

@@ -115,7 +115,7 @@ public VisibilityModifier getVisibilityModifier() {
115115

116116

117117
@Override
118-
public ImmutableList<TextualJMLConstruct> getAttachedJml() {
118+
public ImmutableList<JmlContract> getAttachedJml() {
119119
return attachedJml;
120120
}
121121

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/MethodDeclaration.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55

66
import java.util.List;
77

8+
import com.github.javaparser.ast.jml.clauses.JmlContract;
89
import de.uka.ilkd.key.java.ast.*;
910
import de.uka.ilkd.key.java.ast.abstraction.KeYJavaType;
1011
import de.uka.ilkd.key.java.ast.abstraction.Method;
@@ -13,7 +14,6 @@
1314
import de.uka.ilkd.key.java.visitor.Visitor;
1415
import de.uka.ilkd.key.logic.ProgramElementName;
1516
import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
16-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1717
import de.uka.ilkd.key.speclang.njml.SpecMathMode;
1818

1919
import org.key_project.util.ExtList;
@@ -94,7 +94,7 @@ public MethodDeclaration(
9494
Comment[] voidComments, ProgramElementName name,
9595
ImmutableArray<ParameterDeclaration> parameters, Throws exceptions,
9696
StatementBlock body, boolean parentIsInterfaceDeclaration,
97-
ImmutableList<TextualJMLConstruct> attachedJml) {
97+
ImmutableList<JmlContract> attachedJml) {
9898
super(pi, comments, modArray, attachedJml);
9999
this.returnType = returnType;
100100
this.voidComments = voidComments;

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/TypeDeclaration.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@
1212
import de.uka.ilkd.key.java.ast.expression.literal.NullLiteral;
1313
import de.uka.ilkd.key.logic.ProgramElementName;
1414
import de.uka.ilkd.key.speclang.jml.JMLInfoExtractor;
15-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1615
import de.uka.ilkd.key.speclang.njml.SpecMathMode;
1716

1817
import org.key_project.util.ExtList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/Do.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@
88
import de.uka.ilkd.key.java.ast.*;
99
import de.uka.ilkd.key.java.ast.expression.Expression;
1010
import de.uka.ilkd.key.java.visitor.Visitor;
11-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1211

1312
import org.key_project.util.ExtList;
1413
import org.key_project.util.collection.ImmutableList;

key.core/src/main/java/de/uka/ilkd/key/java/ast/statement/EnhancedFor.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@
99
import de.uka.ilkd.key.java.ast.declaration.LocalVariableDeclaration;
1010
import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
1111
import de.uka.ilkd.key.java.visitor.Visitor;
12-
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1312

1413
import org.key_project.util.ExtList;
1514
import org.key_project.util.collection.ImmutableList;

0 commit comments

Comments
 (0)