Skip to content

Commit 0f5e5d8

Browse files
committed
Minor Change
1 parent e895d71 commit 0f5e5d8

5 files changed

Lines changed: 10 additions & 11 deletions

File tree

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ public String getSnippet() {
129129

130130
// line number padding + pipe + column offset
131131
String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
132-
+ " ".repeat(visualColStart - 1);
132+
+ " ".repeat(visualColStart - 1);
133133
String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
134134
sb.append(indent).append(markers);
135135

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -82,8 +82,8 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
8282
Predicate p = new Predicate(ref.get(), element);
8383
if (!p.getExpression().isBooleanExpression()) {
8484
SourcePosition position = Utils.getAnnotationPosition(element, ref.get());
85-
throw new InvalidRefinementError(position,
86-
"Refinement predicate must be a boolean expression", ref.get());
85+
throw new InvalidRefinementError(position, "Refinement predicate must be a boolean expression",
86+
ref.get());
8787
}
8888
constr = Optional.of(p);
8989
}
@@ -251,8 +251,8 @@ protected void handleAlias(String ref, CtElement element, SourcePosition positio
251251
if (klass != null && path != null) {
252252
a.parse(path);
253253
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
254-
throw new InvalidRefinementError(position,
255-
"Refinement alias must return a boolean expression", ref);
254+
throw new InvalidRefinementError(position, "Refinement alias must return a boolean expression",
255+
ref);
256256
}
257257
AliasWrapper aw = new AliasWrapper(a, factory, klass, path);
258258
context.addAlias(aw);

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -210,8 +210,8 @@ private static Predicate createStatePredicate(String value, String targetClass,
210210
Predicate p = new Predicate(value, e, prefix);
211211
if (!p.getExpression().isBooleanExpression()) {
212212
SourcePosition position = Utils.getAnnotationPosition(e, value);
213-
throw new InvalidRefinementError(position,
214-
"State refinement transition must be a boolean expression", value);
213+
throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression",
214+
value);
215215
}
216216
CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
217217
String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());

liquidjava-verifier/src/main/java/liquidjava/rj_language/parsing/RefinementsParser.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,8 @@ public static AliasDTO getAliasDeclaration(String s) throws LJError {
5656
AliasVisitor av = new AliasVisitor(input);
5757
AliasDTO alias = av.getAlias(rc);
5858
if (alias == null)
59-
throw new SyntaxError("Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s);
59+
throw new SyntaxError(
60+
"Invalid alias definition, expected e.g. @RefinementAlias(\"Positive(int v) { v >= 0 }\")", s);
6061
return alias;
6162
}
6263

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/GhostVisitor.java

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,7 @@ public static GhostDTO getGhostDecl(ParseTree rc) {
1919
List<String> ls = args.stream().map(Pair::first).collect(Collectors.toList());
2020
return new GhostDTO(name, ls, type);
2121
} else if (rc.getChildCount() > 0) {
22-
int i = rc.getChildCount();
23-
if (i > 0)
24-
return getGhostDecl(rc.getChild(0));
22+
return getGhostDecl(rc.getChild(0));
2523
}
2624
return null;
2725
}

0 commit comments

Comments
 (0)