Skip to content

Commit e64d5b7

Browse files
rcosta358rcosta358
committed
Remove Redundant Error Check & Fix Typos
1 parent ba23ac7 commit e64d5b7

7 files changed

Lines changed: 18 additions & 39 deletions

File tree

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

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
package liquidjava.processor;
22

3-
import static liquidjava.diagnostics.Diagnostics.diagnostics;
4-
53
import java.util.ArrayList;
64
import java.util.List;
75

@@ -32,14 +30,9 @@ public void process(CtPackage pkg) {
3230
c.reinitializeAllContext();
3331

3432
pkg.accept(new FieldGhostsGeneration(c, factory)); // generate annotations for field ghosts
35-
36-
// void spoon.reflect.visitor.CtVisitable.accept(CtVisitor arg0)
3733
pkg.accept(new ExternalRefinementTypeChecker(c, factory));
3834
pkg.accept(new MethodsFirstChecker(c, factory)); // double passing idea (instead of headers)
39-
4035
pkg.accept(new RefinementTypeChecker(c, factory));
41-
if (diagnostics.foundError())
42-
return;
4336
}
4437
}
4538
}

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

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,6 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
8686
if (!p.getExpression().isBooleanExpression()) {
8787
diagnostics.add(new InvalidRefinementError(element, "Refinement predicate must be a boolean expression",
8888
ref.get()));
89-
return Optional.empty();
9089
}
9190
if (diagnostics.foundError())
9291
return Optional.empty();
@@ -317,8 +316,8 @@ public boolean checksStateSMT(Predicate prevState, Predicate expectedState, Sour
317316
return vcChecker.canProcessSubtyping(prevState, expectedState, context.getGhostState(), p, factory);
318317
}
319318

320-
public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customeMessage) {
321-
vcChecker.printSubtypingError(element, expectedType, foundType, customeMessage);
319+
public void createError(CtElement element, Predicate expectedType, Predicate foundType, String customMessage) {
320+
vcChecker.printSubtypingError(element, expectedType, foundType, customMessage);
322321
}
323322

324323
public void createSameStateError(CtElement element, Predicate expectedType, String klass) {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -311,7 +311,7 @@ private TranslationTable createMap(CtElement element, Predicate expectedType) {
311311
}
312312

313313
protected void printSubtypingError(CtElement element, Predicate expectedType, Predicate foundType,
314-
String customeMsg) {
314+
String customMsg) {
315315
List<RefinedVariable> lrv = new ArrayList<>(), mainVars = new ArrayList<>();
316316
gatherVariables(expectedType, lrv, mainVars);
317317
gatherVariables(foundType, lrv, mainVars);

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
import liquidjava.processor.refinement_checker.TypeChecker;
1616
import liquidjava.utils.constants.Formats;
1717
import liquidjava.utils.constants.Keys;
18-
import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinememtsPassage;
18+
import liquidjava.processor.refinement_checker.object_checkers.AuxHierarchyRefinementsPassage;
1919
import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
2020
import liquidjava.rj_language.Predicate;
2121
import liquidjava.rj_language.parsing.ParsingException;
@@ -107,7 +107,7 @@ public <R> void getMethodRefinements(CtMethod<R> method) throws ParsingException
107107
AuxStateHandler.handleMethodState(method, f, rtc, prefix);
108108

109109
if (klass != null)
110-
AuxHierarchyRefinememtsPassage.checkFunctionInSupertypes(klass, method, f, rtc);
110+
AuxHierarchyRefinementsPassage.checkFunctionInSupertypes(klass, method, f, rtc);
111111
}
112112

113113
public <R> void getMethodRefinements(CtMethod<R> method, String prefix) throws ParsingException {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinememtsPassage.java renamed to liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxHierarchyRefinementsPassage.java

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,5 @@
11
package liquidjava.processor.refinement_checker.object_checkers;
22

3-
import static liquidjava.diagnostics.Diagnostics.diagnostics;
4-
53
import java.util.HashMap;
64
import java.util.List;
75
import java.util.Optional;
@@ -20,7 +18,7 @@
2018
import spoon.reflect.declaration.CtParameter;
2119
import spoon.reflect.reference.CtTypeReference;
2220

23-
public class AuxHierarchyRefinememtsPassage {
21+
public class AuxHierarchyRefinementsPassage {
2422

2523
public static <R> void checkFunctionInSupertypes(CtClass<?> klass, CtMethod<R> method, RefinedFunction f,
2624
TypeChecker tc) {
@@ -83,10 +81,9 @@ static void transferArgumentsRefinements(RefinedFunction superFunction, RefinedF
8381
if (argRef.isBooleanTrue()) {
8482
arg.setRefinement(superArgRef.substituteVariable(newName, arg.getName()));
8583
} else {
86-
boolean f = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
87-
if (!f) {
88-
if (!diagnostics.foundError())
89-
tc.createError(method, argRef, superArgRef, "");
84+
boolean ok = tc.checksStateSMT(superArgRef, argRef, params.get(i).getPosition());
85+
if (!ok) {
86+
tc.createError(method, argRef, superArgRef, "");
9087
}
9188
}
9289
}

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

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -197,23 +197,20 @@ private static Predicate createStatePredicate(String value, /* RefinedFunction f
197197
new InvalidRefinementError(e, "State refinement transition must be a boolean expression", value));
198198
return new Predicate();
199199
}
200-
String t = targetClass; // f.getTargetClass();
201-
CtTypeReference<?> r = tc.getFactory().Type().createReference(t);
202-
200+
CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
203201
String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
204202
String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
205203
tc.getContext().addVarToContext(name, r, new Predicate(), e);
206204
tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
207205
// TODO REVIEW!!
208206
// what is it for?
209-
Predicate c1 = isTo ? getMissingStates(t, tc, p) : p;
207+
Predicate c1 = isTo ? getMissingStates(targetClass, tc, p) : p;
210208
Predicate c = c1.substituteVariable(Keys.THIS, name);
211209
c = c.changeOldMentions(nameOld, name);
212-
boolean b = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition());
213-
if (b && !diagnostics.foundError()) {
214-
tc.createSameStateError(e, p, t);
210+
boolean ok = tc.checksStateSMT(new Predicate(), c.negate(), e.getPosition());
211+
if (ok) {
212+
tc.createSameStateError(e, p, targetClass);
215213
}
216-
217214
return c1;
218215
}
219216

@@ -400,10 +397,8 @@ public static void updateGhostField(CtFieldWrite<?> fw, TypeChecker tc) {
400397
.changeOldMentions(vi.getName(), instanceName);
401398

402399
if (!tc.checksStateSMT(prevState, expectState, fw.getPosition())) { // Invalid field transition
403-
if (!diagnostics.foundError()) { // No errors so far
404-
Predicate[] states = { stateChange.getFrom() };
405-
tc.createStateMismatchError(fw, fw.toString(), prevState, states);
406-
}
400+
Predicate[] states = { stateChange.getFrom() };
401+
tc.createStateMismatchError(fw, fw.toString(), prevState, states);
407402
return;
408403
}
409404

@@ -488,13 +483,11 @@ private static Predicate changeState(TypeChecker tc, VariableInstance vi,
488483
return transitionedState;
489484
}
490485
}
491-
if (!found && !diagnostics.foundError()) { // Reaches the end of stateChange no matching states
486+
if (!found) { // Reaches the end of stateChange no matching states
492487
Predicate[] states = stateChanges.stream().filter(ObjectState::hasFrom).map(ObjectState::getFrom)
493488
.toArray(Predicate[]::new);
494-
String simpleInvocation = invocation.toString(); // .getExecutable().toString();
489+
String simpleInvocation = invocation.toString();
495490
tc.createStateMismatchError(invocation, simpleInvocation, prevState, states);
496-
// ErrorPrinter.printStateMismatch(invocation, simpleInvocation, prevState,
497-
// states);
498491
}
499492
return new Predicate();
500493
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,6 @@ public Predicate(String ref, CtElement element) throws ParsingException {
7676
public Predicate(String ref, CtElement element, String prefix) throws ParsingException {
7777
this.prefix = prefix;
7878
exp = parse(ref, element);
79-
if (diagnostics.foundError()) {
80-
return;
81-
}
8279
if (!(exp instanceof GroupExpression)) {
8380
exp = new GroupExpression(exp);
8481
}

0 commit comments

Comments
 (0)