Skip to content

Commit 747fcd3

Browse files
committed
Remove Positions
1 parent 9024b64 commit 747fcd3

3 files changed

Lines changed: 1 addition & 17 deletions

File tree

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

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ public class RefinedFunction extends Refined {
1212
private String targetClass;
1313
private List<ObjectState> stateChange;
1414
private String signature;
15-
private PlacementInCode placementInCode;
1615

1716
public RefinedFunction() {
1817
argRefinements = new ArrayList<>();
@@ -51,18 +50,6 @@ public String getSignature() {
5150
return signature;
5251
}
5352

54-
public void setPlacementInCode(CtElement element) {
55-
placementInCode = PlacementInCode.createPlacement(element);
56-
}
57-
58-
public void setPlacementInScope(PlacementInCode placement) {
59-
placementInCode = placement;
60-
}
61-
62-
public PlacementInCode getPlacementInCode() {
63-
return placementInCode;
64-
}
65-
6653
public Predicate getRenamedRefinements(Context c, CtElement element) {
6754
return getRenamedRefinements(getAllRefinements(), c, element);
6855
}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -379,7 +379,7 @@ public void visitCtIf(CtIf ifElement) {
379379
thenRefs = Predicate.createConjunction(expRefs, freshIsTrue);
380380
elseRefs = Predicate.createConjunction(expRefs, freshIsFalse);
381381
}
382-
382+
383383
freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp);
384384
}
385385
vcChecker.addPathVariable(freshRV);

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

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,6 @@ public void getConstructorRefinements(CtConstructor<?> c) throws LJError {
4343
RefinedFunction f = new RefinedFunction();
4444
f.setName(c.getSimpleName());
4545
f.setType(c.getType());
46-
f.setPlacementInCode(c);
4746
handleFunctionRefinements(f, c, c.getParameters());
4847
f.setRefReturn(new Predicate());
4948
CtTypeReference<?> declaring = c.getDeclaringType() != null ? c.getDeclaringType().getReference() : null;
@@ -79,7 +78,6 @@ public <R> void getMethodRefinements(CtMethod<R> method) throws LJError {
7978
RefinedFunction f = new RefinedFunction();
8079
f.setName(method.getSimpleName().replaceAll("\\p{C}", "")); // remove any empty chars from string
8180
f.setType(method.getType());
82-
f.setPlacementInCode(method);
8381
f.setRefReturn(new Predicate());
8482

8583
CtClass<?> klass = null;
@@ -117,7 +115,6 @@ public <R> void getMethodRefinements(CtMethod<R> method, String prefix) throws L
117115
RefinedFunction f = new RefinedFunction();
118116
f.setName(functionName.replaceAll("\\p{C}", "")); // remove any empty chars from string
119117
f.setType(method.getType());
120-
f.setPlacementInCode(method);
121118
f.setRefReturn(new Predicate());
122119
f.setClass(prefix);
123120
f.setSignature(String.format("%s.%s", prefix, method.getSignature()));

0 commit comments

Comments
 (0)