Skip to content

Commit ab4d600

Browse files
author
RajShivu
committed
Assert: checked assert validation tests
1 parent e111574 commit ab4d600

File tree

2 files changed

+10
-2
lines changed

2 files changed

+10
-2
lines changed

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,7 @@ private Predicate handleFunctionRefinements(RefinedFunction f, CtElement method,
161161
Optional<Predicate> oret = rtc.getRefinementFromAnnotation(method);
162162
Predicate ret = oret.orElse(new Predicate());
163163
ret = ret.substituteVariable("return", Keys.WILDCARD);
164+
ret = ret.substituteVariable("$result", Keys.WILDCARD);// added for refinement
164165
f.setRefReturn(ret);
165166
return Predicate.createConjunction(joint, ret);
166167
}
@@ -180,6 +181,13 @@ public <R> void getReturnRefinements(CtReturn<R> ret) throws LJError {
180181
RefinedFunction fi = rtc.getContext().getFunction(method.getSimpleName(),
181182
((CtClass<?>) method.getParent()).getQualifiedName(), method.getParameters().size());
182183

184+
if (fi == null)
185+
return;// null check refinement
186+
187+
if (fi.getRefReturn() == null) {
188+
return;
189+
}
190+
183191
List<Variable> lv = fi.getArguments();
184192
for (Variable v : lv) {
185193
rtc.getContext().addVarToContext(v);

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestMultiple.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ public void testMultipleErrorDirectory() {
1414
String path = "../liquidjava-example/src/main/java/testMultiple/errors";
1515
CommandLineLauncher.launch(path);
1616
Diagnostics diagnostics = Diagnostics.getInstance();
17-
assertEquals(9, diagnostics.getErrors().size());// 9
17+
assertEquals(9, diagnostics.getErrors().size());
1818
}
1919

2020
@Test
@@ -39,7 +39,7 @@ public void testMultipleDirectory() {
3939
CommandLineLauncher.launch(path);
4040
Diagnostics diagnostics = Diagnostics.getInstance();
4141

42-
assertEquals(11, diagnostics.getErrors().size());// 11
42+
assertEquals(11, diagnostics.getErrors().size());
4343
assertEquals(3, diagnostics.getWarnings().size());
4444
}
4545
}

0 commit comments

Comments
 (0)