Skip to content

Commit 79afe64

Browse files
CatarinaGamboaCatarinaGamboa
authored
formatter (#40)
1 parent 8909265 commit 79afe64

Some content is hidden

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

49 files changed

+1013
-988
lines changed

‎liquidjava-verifier/src/main/java/liquidjava/errors/ErrorEmitter.java‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,11 @@ public class ErrorEmitter {
1414
private int errorStatus;
1515
private HashMap<String, PlacementInCode> map;
1616

17-
public ErrorEmitter() {}
17+
public ErrorEmitter() {
18+
}
1819

19-
public void addError(
20-
String titleMessage, String msg, SourcePosition p, int errorStatus, HashMap<String, PlacementInCode> map) {
20+
public void addError(String titleMessage, String msg, SourcePosition p, int errorStatus,
21+
HashMap<String, PlacementInCode> map) {
2122
this.titleMessage = titleMessage;
2223
fullMessage = msg;
2324
try {

‎liquidjava-verifier/src/main/java/liquidjava/errors/ErrorHandler.java‎

Lines changed: 21 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -20,22 +20,13 @@ public class ErrorHandler {
2020
* @param expectedType
2121
* @param cSMT
2222
*/
23-
public static <T> void printError(
24-
CtElement var,
25-
Predicate expectedType,
26-
Predicate cSMT,
27-
HashMap<String, PlacementInCode> map,
28-
ErrorEmitter ee) {
23+
public static <T> void printError(CtElement var, Predicate expectedType, Predicate cSMT,
24+
HashMap<String, PlacementInCode> map, ErrorEmitter ee) {
2925
printError(var, null, expectedType, cSMT, map, ee);
3026
}
3127

32-
public static <T> void printError(
33-
CtElement var,
34-
String moreInfo,
35-
Predicate expectedType,
36-
Predicate cSMT,
37-
HashMap<String, PlacementInCode> map,
38-
ErrorEmitter errorl) {
28+
public static <T> void printError(CtElement var, String moreInfo, Predicate expectedType, Predicate cSMT,
29+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
3930
String resumeMessage = "Type expected:" + expectedType.toString(); // + "; " +"Refinement found:" +
4031
// cSMT.toString();
4132

@@ -44,7 +35,8 @@ public static <T> void printError(
4435
// title
4536
StringBuilder sbtitle = new StringBuilder();
4637
sbtitle.append("Failed to check refinement at: \n\n");
47-
if (moreInfo != null) sbtitle.append(moreInfo + "\n");
38+
if (moreInfo != null)
39+
sbtitle.append(moreInfo + "\n");
4840
sbtitle.append(var.toString());
4941
// all message
5042
sb.append(sbtitle.toString() + "\n\n");
@@ -57,13 +49,8 @@ public static <T> void printError(
5749
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 1, map);
5850
}
5951

60-
public static void printStateMismatch(
61-
CtElement element,
62-
String method,
63-
VCImplication constraintForErrorMsg,
64-
String states,
65-
HashMap<String, PlacementInCode> map,
66-
ErrorEmitter errorl) {
52+
public static void printStateMismatch(CtElement element, String method, VCImplication constraintForErrorMsg,
53+
String states, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
6754

6855
String resumeMessage = "Failed to check state transitions. " + "Expected possible states:" + states; // + ";
6956
// Found
@@ -91,12 +78,8 @@ public static void printStateMismatch(
9178
errorl.addError(resumeMessage, sb.toString(), element.getPosition(), 1, map);
9279
}
9380

94-
public static <T> void printErrorUnknownVariable(
95-
CtElement var,
96-
String et,
97-
String correctRefinement,
98-
HashMap<String, PlacementInCode> map,
99-
ErrorEmitter errorl) {
81+
public static <T> void printErrorUnknownVariable(CtElement var, String et, String correctRefinement,
82+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
10083

10184
String resumeMessage = "Encountered unknown variable";
10285

@@ -114,13 +97,8 @@ public static <T> void printErrorUnknownVariable(
11497
errorl.addError(resumeMessage, sb.toString(), var.getPosition(), 2, map);
11598
}
11699

117-
public static <T> void printNotFound(
118-
CtElement var,
119-
Predicate constraint,
120-
Predicate constraint2,
121-
String msg,
122-
HashMap<String, PlacementInCode> map,
123-
ErrorEmitter errorl) {
100+
public static <T> void printNotFound(CtElement var, Predicate constraint, Predicate constraint2, String msg,
101+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
124102

125103
StringBuilder sb = new StringBuilder();
126104
sb.append("______________________________________________________\n");
@@ -136,12 +114,8 @@ public static <T> void printNotFound(
136114
errorl.addError(msg, sb.toString(), var.getPosition(), 2, map);
137115
}
138116

139-
public static <T> void printErrorArgs(
140-
CtElement var,
141-
Predicate expectedType,
142-
String msg,
143-
HashMap<String, PlacementInCode> map,
144-
ErrorEmitter errorl) {
117+
public static <T> void printErrorArgs(CtElement var, Predicate expectedType, String msg,
118+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
145119
StringBuilder sb = new StringBuilder();
146120
sb.append("______________________________________________________\n");
147121
String title = "Error in ghost invocation: " + msg + "\n";
@@ -154,12 +128,8 @@ public static <T> void printErrorArgs(
154128
errorl.addError(title, sb.toString(), var.getPosition(), 2, map);
155129
}
156130

157-
public static void printErrorTypeMismatch(
158-
CtElement element,
159-
Predicate expectedType,
160-
String message,
161-
HashMap<String, PlacementInCode> map,
162-
ErrorEmitter errorl) {
131+
public static void printErrorTypeMismatch(CtElement element, Predicate expectedType, String message,
132+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
163133
StringBuilder sb = new StringBuilder();
164134
sb.append("______________________________________________________\n");
165135
sb.append(message + "\n\n");
@@ -171,8 +141,8 @@ public static void printErrorTypeMismatch(
171141
errorl.addError(message, sb.toString(), element.getPosition(), 2, map);
172142
}
173143

174-
public static void printSameStateSetError(
175-
CtElement element, Predicate p, String name, HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
144+
public static void printSameStateSetError(CtElement element, Predicate p, String name,
145+
HashMap<String, PlacementInCode> map, ErrorEmitter errorl) {
176146
String resume = "Error found multiple disjoint states from a State Set in a refinement";
177147

178148
StringBuilder sb = new StringBuilder();
@@ -249,7 +219,8 @@ public static void printSyntaxError(String msg, String ref, ErrorEmitter errorl)
249219

250220
private static String printLine() {
251221
StringBuilder sb = new StringBuilder();
252-
for (int i = 0; i < 130; i++) sb.append("-"); // -----------
222+
for (int i = 0; i < 130; i++)
223+
sb.append("-"); // -----------
253224
return sb.toString();
254225
}
255226

@@ -267,9 +238,7 @@ private static String printMap(HashMap<String, PlacementInCode> map) {
267238
formatter.format(printLine() + "\n");
268239
// data
269240
for (String s : map.keySet())
270-
formatter.format(
271-
"| %-32s | %-60s | %-1s \n",
272-
s, map.get(s).getText(), map.get(s).getSimplePosition());
241+
formatter.format("| %-32s | %-60s | %-1s \n", s, map.get(s).getText(), map.get(s).getSimplePosition());
273242
// end
274243
formatter.format(printLine() + "\n\n");
275244
String s = formatter.toString();

‎liquidjava-verifier/src/main/java/liquidjava/processor/RefinementProcessor.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,8 @@ public void process(CtPackage pkg) {
3939
pkg.accept(new MethodsFirstChecker(c, factory, errorEmitter)); // double passing idea (instead of headers)
4040

4141
pkg.accept(new RefinementTypeChecker(c, factory, errorEmitter));
42-
if (errorEmitter.foundError()) return;
42+
if (errorEmitter.foundError())
43+
return;
4344
}
4445
}
4546
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,31 +30,32 @@ public String toString() {
3030
if (name != null && type != null) {
3131
String qualType = type.getQualifiedName();
3232
String simpleType = qualType.contains(".") ? qualType.substring(qualType.lastIndexOf(".") + 1) : qualType;
33-
return String.format(
34-
"%-20s %s %s",
35-
"∀" + name + ":" + simpleType + ",",
36-
refinement.toString(),
33+
return String.format("%-20s %s %s", "∀" + name + ":" + simpleType + ",", refinement.toString(),
3734
next != null ? " => \n" + next.toString() : "");
38-
} else return String.format("%-20s %s", "", refinement.toString());
35+
} else
36+
return String.format("%-20s %s", "", refinement.toString());
3937
}
4038

4139
public Predicate toConjunctions() {
4240
Predicate c = new Predicate();
43-
if (name == null && type == null && next == null) return c;
41+
if (name == null && type == null && next == null)
42+
return c;
4443
c = auxConjunction(c);
4544
return c;
4645
}
4746

4847
private Predicate auxConjunction(Predicate c) {
4948
Predicate t = Predicate.createConjunction(c, refinement);
50-
if (next == null) return t;
49+
if (next == null)
50+
return t;
5151
t = next.auxConjunction(t);
5252
return t;
5353
}
5454

5555
public VCImplication clone() {
5656
VCImplication vc = new VCImplication(this.name, this.type, this.refinement.clone());
57-
if (this.next != null) vc.next = this.next.clone();
57+
if (this.next != null)
58+
vc.next = this.next.clone();
5859
return vc;
5960
}
6061
}

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,7 @@ public <T> void visitCtClass(CtClass<T> ctClass) {
3333
return;
3434
}
3535

36-
ctClass.getDeclaredFields().stream()
37-
.filter(fld -> fld.getType().getQualifiedName().equals("int"))
36+
ctClass.getDeclaredFields().stream().filter(fld -> fld.getType().getQualifiedName().equals("int"))
3837
.forEach(fld -> {
3938
CtTypeReference<?> fld_type = fld.getType();
4039
CtAnnotation<?> gen_ann = factory.createAnnotation(factory.createCtTypeReference(Ghost.class));

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

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -64,16 +64,17 @@ public Predicate getPremises(List<String> list, List<String> newNames, CtElement
6464
List<Predicate> invocationPredicates = getPredicatesFromExpression(list, elem, ee);
6565
Predicate prem = new Predicate();
6666
for (int i = 0; i < invocationPredicates.size(); i++) {
67-
prem = Predicate.createConjunction(
68-
prem, Predicate.createEquals(Predicate.createVar(newNames.get(i)), invocationPredicates.get(i)));
67+
prem = Predicate.createConjunction(prem,
68+
Predicate.createEquals(Predicate.createVar(newNames.get(i)), invocationPredicates.get(i)));
6969
}
7070
return prem.clone();
7171
}
7272

7373
private List<Predicate> getPredicatesFromExpression(List<String> list, CtElement elem, ErrorEmitter ee)
7474
throws ParsingException {
7575
List<Predicate> lp = new ArrayList<>();
76-
for (String e : list) lp.add(new Predicate(e, elem, ee));
76+
for (String e : list)
77+
lp.add(new Predicate(e, elem, ee));
7778

7879
return lp;
7980
}

0 commit comments

Comments
 (0)