Skip to content

Commit 5c8cc91

Browse files
rcosta358rcosta358
committed
Fix Names to camelCase
1 parent e8af6f1 commit 5c8cc91

File tree

7 files changed

+43
-43
lines changed

7 files changed

+43
-43
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/processor/ann_generation/FieldGhostsGeneration.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,10 +28,10 @@ public Factory getFactory() {
2828
public <T> void visitCtClass(CtClass<T> ctClass) {
2929
ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int"))
3030
.forEach(fld -> {
31-
CtTypeReference<?> fld_type = fld.getType();
32-
CtAnnotation<?> gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
33-
gen_ann.addValue("value", fld_type.getSimpleName() + " " + fld.getSimpleName());
34-
ctClass.addAnnotation(gen_ann);
31+
CtTypeReference<?> fldType = fld.getType();
32+
CtAnnotation<?> genAnn = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));
33+
genAnn.addValue("value", fldType.getSimpleName() + " " + fld.getSimpleName());
34+
ctClass.addAnnotation(genAnn);
3535
});
3636

3737
super.visitCtClass(ctClass);

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostFunction.java‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -10,53 +10,53 @@
1010
public class GhostFunction {
1111

1212
private final String name;
13-
private final List<CtTypeReference<?>> param_types;
14-
private final CtTypeReference<?> return_type;
13+
private final List<CtTypeReference<?>> paramTypes;
14+
private final CtTypeReference<?> returnType;
1515
private final String prefix;
1616

1717
public GhostFunction(GhostDTO f, Factory factory, String prefix) {
1818
String klass = this.getParentClassName(prefix);
1919
this.name = f.name();
20-
this.return_type = Utils.getType(f.return_type().equals(klass) ? prefix : f.return_type(), factory);
21-
this.param_types = new ArrayList<>();
20+
this.returnType = Utils.getType(f.returnType().equals(klass) ? prefix : f.returnType(), factory);
21+
this.paramTypes = new ArrayList<>();
2222
this.prefix = prefix;
23-
for (String t : f.param_types()) {
24-
this.param_types.add(Utils.getType(t.equals(klass) ? prefix : t, factory));
23+
for (String t : f.paramTypes()) {
24+
this.paramTypes.add(Utils.getType(t.equals(klass) ? prefix : t, factory));
2525
}
2626
}
2727

28-
public GhostFunction(String name, List<String> param_types, CtTypeReference<?> return_type, Factory factory,
28+
public GhostFunction(String name, List<String> paramTypes, CtTypeReference<?> returnType, Factory factory,
2929
String prefix) {
3030
String klass = this.getParentClassName(prefix);
31-
String type = return_type.toString().equals(klass) ? prefix : return_type.toString();
31+
String type = returnType.toString().equals(klass) ? prefix : returnType.toString();
3232
this.name = name;
33-
this.return_type = Utils.getType(type, factory);
34-
this.param_types = new ArrayList<>();
33+
this.returnType = Utils.getType(type, factory);
34+
this.paramTypes = new ArrayList<>();
3535
this.prefix = prefix;
36-
for (String mType : param_types) {
37-
this.param_types.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory));
36+
for (String mType : paramTypes) {
37+
this.paramTypes.add(Utils.getType(mType.equals(klass) ? prefix : mType, factory));
3838
}
3939
}
4040

41-
protected GhostFunction(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String prefix) {
41+
protected GhostFunction(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix) {
4242
this.name = name;
43-
this.return_type = return_type;
44-
this.param_types = list;
43+
this.returnType = returnType;
44+
this.paramTypes = list;
4545
this.prefix = prefix;
4646
}
4747

4848
public CtTypeReference<?> getReturnType() {
49-
return return_type;
49+
return returnType;
5050
}
5151

5252
public List<CtTypeReference<?>> getParametersTypes() {
53-
return param_types;
53+
return paramTypes;
5454
}
5555

5656
public String toString() {
5757
StringBuilder sb = new StringBuilder();
58-
sb.append("ghost ").append(return_type.toString()).append(" ").append(name).append("(");
59-
for (CtTypeReference<?> t : param_types) {
58+
sb.append("ghost ").append(returnType.toString()).append(" ").append(name).append("(");
59+
for (CtTypeReference<?> t : paramTypes) {
6060
sb.append(t.toString()).append(" ,");
6161
}
6262
sb.delete(sb.length() - 2, sb.length());

‎liquidjava-verifier/src/main/java/liquidjava/processor/context/GhostState.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ public class GhostState extends GhostFunction {
99
private GhostFunction parent;
1010
private Predicate refinement;
1111

12-
public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> return_type, String prefix) {
13-
super(name, list, return_type, prefix);
12+
public GhostState(String name, List<CtTypeReference<?>> list, CtTypeReference<?> returnType, String prefix) {
13+
super(name, list, returnType, prefix);
1414
}
1515

1616
public void setGhostParent(GhostFunction parent) {

‎liquidjava-verifier/src/main/java/liquidjava/processor/facade/GhostDTO.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22

33
import java.util.List;
44

5-
public record GhostDTO(String name, List<String> param_types, String return_type) {
5+
public record GhostDTO(String name, List<String> paramTypes, String returnType) {
66
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -150,7 +150,7 @@ private void createStateSet(CtNewArray<String> e, int set, CtElement element) th
150150
private void createStateGhost(String string, CtAnnotation<? extends Annotation> ann, CtElement element)
151151
throws LJError {
152152
GhostDTO gd = RefinementsParser.getGhostDeclaration(string);
153-
if (!gd.param_types().isEmpty()) {
153+
if (!gd.paramTypes().isEmpty()) {
154154
throw new CustomError(
155155
"Ghost States have the class as parameter " + "by default, no other parameters are allowed", ann);
156156
}
@@ -160,7 +160,7 @@ private void createStateGhost(String string, CtAnnotation<? extends Annotation>
160160
context.addGhostClass(sn);
161161
List<CtTypeReference<?>> param = Collections.singletonList(factory.Type().createReference(qn));
162162

163-
CtTypeReference<?> r = factory.Type().createReference(gd.return_type());
163+
CtTypeReference<?> r = factory.Type().createReference(gd.returnType());
164164
GhostState gs = new GhostState(gd.name(), param, r, qn);
165165
context.addToGhostClass(sn, gs);
166166
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -185,23 +185,23 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
185185
String elemName = elemVar.getVariable().getSimpleName();
186186
if (elemVar instanceof CtFieldRead)
187187
elemName = String.format(Formats.THIS, elemName);
188-
Predicate elem_ref = rtc.getContext().getVariableRefinements(elemName);
188+
Predicate elemRef = rtc.getContext().getVariableRefinements(elemName);
189189

190190
String returnName = elemName;
191191

192192
CtElement parent = operator.getParent();
193193
// No need for specific values
194194
if (parent != null && !(parent instanceof CtIfImpl)) {
195-
elem_ref = rtc.getRefinement(elemVar);
195+
elemRef = rtc.getRefinement(elemVar);
196196
String newName = String.format(Formats.INSTANCE, elemName, rtc.getContext().getCounter());
197-
Predicate newElem_ref = elem_ref.substituteVariable(Keys.WILDCARD, newName);
198-
RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElem_ref,
197+
Predicate newElemRef = elemRef.substituteVariable(Keys.WILDCARD, newName);
198+
RefinedVariable newVi = rtc.getContext().addVarToContext(newName, elemVar.getType(), newElemRef,
199199
elemVar);
200200
rtc.getContext().addSpecificVariable(newVi);
201201
returnName = newName;
202202
}
203203

204-
Predicate e = elem_ref.substituteVariable(Keys.WILDCARD, elemName);
204+
Predicate e = elemRef.substituteVariable(Keys.WILDCARD, elemName);
205205
rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar);
206206
return Predicate.createVar(returnName);
207207
} else if (element instanceof CtBinaryOperator<?> binop) {

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -383,13 +383,13 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) throws L
383383
}
384384

385385
String parentTargetName = ((CtVariableRead<?>) fw.getTarget()).getVariable().getSimpleName();
386-
Optional<VariableInstance> invocation_callee = tc.getContext().getLastVariableInstance(parentTargetName);
386+
Optional<VariableInstance> invocationCallee = tc.getContext().getLastVariableInstance(parentTargetName);
387387

388-
if (invocation_callee.isEmpty()) {
388+
if (invocationCallee.isEmpty()) {
389389
return;
390390
}
391391

392-
VariableInstance vi = invocation_callee.get();
392+
VariableInstance vi = invocationCallee.get();
393393
String instanceName = vi.getName();
394394
Predicate prevState = vi.getRefinement().substituteVariable(Keys.WILDCARD, instanceName)
395395
.substituteVariable(parentTargetName, instanceName);
@@ -563,9 +563,9 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem
563563
// v--------- field read
564564
// means invocation is in a form of `t.method(args)`
565565
String name = v.getVariable().getSimpleName();
566-
Optional<VariableInstance> invocation_callee = tc.getContext().getLastVariableInstance(name);
567-
if (invocation_callee.isPresent()) {
568-
invocation.putMetadata(Keys.TARGET, invocation_callee.get());
566+
Optional<VariableInstance> invocationCallee = tc.getContext().getLastVariableInstance(name);
567+
if (invocationCallee.isPresent()) {
568+
invocation.putMetadata(Keys.TARGET, invocationCallee.get());
569569
} else if (target2.getMetadata(Keys.TARGET) == null) {
570570
RefinedVariable var = tc.getContext().getVariableByName(name);
571571
String nName = String.format(Formats.INSTANCE, name, tc.getContext().getCounter());
@@ -579,10 +579,10 @@ static String searchFistVariableTarget(TypeChecker tc, CtElement target2, CtElem
579579
} else if (target2.getMetadata(Keys.TARGET) != null) {
580580
// invocation is in
581581
// who did put the metadata here then?
582-
VariableInstance target2_vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
583-
Optional<Variable> v = target2_vi.getParent();
584-
invocation.putMetadata(Keys.TARGET, target2_vi);
585-
return v.map(Refined::getName).orElse(target2_vi.getName());
582+
VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET);
583+
Optional<Variable> v = target2Vi.getParent();
584+
invocation.putMetadata(Keys.TARGET, target2Vi);
585+
return v.map(Refined::getName).orElse(target2Vi.getName());
586586
}
587587
return null;
588588
}

0 commit comments

Comments
 (0)