Skip to content

Commit 9ffe9d9

Browse files
committed
Move Annotation Position from RefinedVariable to PlacementInCode
Also remove `isParameter` field.
1 parent da035a8 commit 9ffe9d9

File tree

5 files changed

+17
-27
lines changed

5 files changed

+17
-27
lines changed

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ public void addVarToContext(RefinedVariable var) {
106106

107107
public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> type, Predicate c, CtElement element) {
108108
RefinedVariable vi = new Variable(simpleName, type, c);
109-
vi.addPlacementInCode(element);
109+
vi.setPlacementInCode(element);
110110
vi.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces());
111111
addVarToContext(vi);
112112
return vi;
@@ -115,7 +115,7 @@ public RefinedVariable addVarToContext(String simpleName, CtTypeReference<?> typ
115115
public RefinedVariable addInstanceToContext(String simpleName, CtTypeReference<?> type, Predicate c,
116116
CtElement element) {
117117
RefinedVariable vi = new VariableInstance(simpleName, type, c);
118-
vi.addPlacementInCode(element);
118+
vi.setPlacementInCode(element);
119119
if (!ctxInstanceVars.contains(vi))
120120
addInstanceVariable(vi);
121121
return vi;
@@ -126,7 +126,7 @@ public void addRefinementToVariableInContext(String name, CtTypeReference<?> typ
126126
if (hasVariable(name)) {
127127
RefinedVariable vi = getVariableByName(name);
128128
vi.setRefinement(et);
129-
vi.addPlacementInCode(element);
129+
vi.setPlacementInCode(element);
130130
} else {
131131
addVarToContext(name, type, et, element);
132132
}

liquidjava-verifier/src/main/java/liquidjava/processor/context/PlacementInCode.java

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
package liquidjava.processor.context;
22

33
import java.lang.annotation.Annotation;
4+
5+
import liquidjava.utils.Utils;
46
import spoon.reflect.code.CtComment;
57
import spoon.reflect.cu.SourcePosition;
68
import spoon.reflect.declaration.CtAnnotation;
@@ -9,10 +11,12 @@
911
public class PlacementInCode {
1012
private final String text;
1113
private final SourcePosition position;
14+
private final SourcePosition annotationPosition;
1215

13-
private PlacementInCode(String text, SourcePosition pos) {
16+
private PlacementInCode(String text, SourcePosition pos, SourcePosition annotationPosition) {
1417
this.text = text;
1518
this.position = pos;
19+
this.annotationPosition = annotationPosition;
1620
}
1721

1822
public String getText() {
@@ -23,6 +27,10 @@ public SourcePosition getPosition() {
2327
return position;
2428
}
2529

30+
public SourcePosition getAnnotationPosition() {
31+
return annotationPosition;
32+
}
33+
2634
public static PlacementInCode createPlacement(CtElement elem) {
2735
CtElement elemCopy = elem.clone();
2836
// cleanup annotations
@@ -38,7 +46,8 @@ public static PlacementInCode createPlacement(CtElement elem) {
3846
}
3947
}
4048
String elemText = elemCopy.toString();
41-
return new PlacementInCode(elemText, elem.getPosition());
49+
SourcePosition annotationPosition = Utils.getFirstLJAnnotationPosition(elem);
50+
return new PlacementInCode(elemText, elem.getPosition(), annotationPosition);
4251
}
4352

4453
public String toString() {

liquidjava-verifier/src/main/java/liquidjava/processor/context/RefinedVariable.java

Lines changed: 2 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -4,21 +4,16 @@
44
import java.util.List;
55
import java.util.Set;
66
import liquidjava.rj_language.Predicate;
7-
import liquidjava.utils.Utils;
8-
import spoon.reflect.cu.SourcePosition;
97
import spoon.reflect.declaration.CtElement;
108
import spoon.reflect.reference.CtTypeReference;
119

1210
public abstract class RefinedVariable extends Refined {
1311
private final List<CtTypeReference<?>> supertypes;
1412
private PlacementInCode placementInCode;
15-
private boolean isParameter;
16-
private SourcePosition annPosition;
1713

1814
public RefinedVariable(String name, CtTypeReference<?> type, Predicate c) {
1915
super(name, type, c);
2016
supertypes = new ArrayList<>();
21-
isParameter = false;
2217
}
2318

2419
public abstract Predicate getMainRefinement();
@@ -40,23 +35,18 @@ public void addSuperTypes(CtTypeReference<?> ts, Set<CtTypeReference<?>> sts) {
4035
supertypes.add(ct);
4136
}
4237

43-
public void addPlacementInCode(CtElement element) {
38+
public void setPlacementInCode(CtElement element) {
4439
placementInCode = PlacementInCode.createPlacement(element);
45-
annPosition = Utils.getFirstLJAnnotationPosition(element);
4640
}
4741

48-
public void addPlacementInCode(PlacementInCode placement) {
42+
public void setPlacementInScope(PlacementInCode placement) {
4943
placementInCode = placement;
5044
}
5145

5246
public PlacementInCode getPlacementInCode() {
5347
return placementInCode;
5448
}
5549

56-
public SourcePosition getAnnPosition() {
57-
return annPosition;
58-
}
59-
6050
@Override
6151
public int hashCode() {
6252
final int prime = 31;
@@ -80,12 +70,4 @@ public boolean equals(Object obj) {
8070
return supertypes.equals(other.supertypes);
8171
}
8272
}
83-
84-
public void setIsParameter(boolean b) {
85-
isParameter = b;
86-
}
87-
88-
public boolean isParameter() {
89-
return isParameter;
90-
}
9173
}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Variable.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ else if (has(ifbeforeIndex)) // value before and in else
148148
ref = createITEConstraint(nName, cond.negate(), get(ifelseIndex));
149149
}
150150
VariableInstance jointReturn = new VariableInstance(nName, super.getType(), ref, this);
151-
jointReturn.addPlacementInCode(getPlacementInCode());
151+
jointReturn.setPlacementInScope(getPlacementInCode());
152152
return Optional.of(jointReturn);
153153
}
154154

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,6 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
154154
c = oc.get().substituteVariable(Keys.WILDCARD, paramName);
155155
param.putMetadata(Keys.REFINEMENT, c);
156156
RefinedVariable v = rtc.getContext().addVarToContext(param.getSimpleName(), param.getType(), c, param);
157-
v.setIsParameter(true);
158157
rtc.getMessageFromAnnotation(param).ifPresent(v::setMessage);
159158
if (v instanceof Variable)
160159
f.addArgRefinements((Variable) v);

0 commit comments

Comments
 (0)