Skip to content

Commit 758650d

Browse files
authored
Skip Null Literals in RefinementTypeChecker (#63)
1 parent 7bb6d67 commit 758650d

File tree

2 files changed

+6
-1
lines changed

2 files changed

+6
-1
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@
1212
import liquidjava.rj_language.BuiltinFunctionPredicate;
1313
import liquidjava.rj_language.Predicate;
1414
import liquidjava.rj_language.parsing.ParsingException;
15+
import liquidjava.utils.Utils;
16+
1517
import org.apache.commons.lang3.NotImplementedException;
1618
import spoon.reflect.code.CtArrayRead;
1719
import spoon.reflect.code.CtArrayWrite;
@@ -264,8 +266,10 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
264266
lit.putMetadata(REFINE_KEY, Predicate.createEquals(Predicate.createVar(WILD_VAR),
265267
Predicate.createLit(lit.getValue().toString(), type)));
266268

267-
} else if (lit.getType().getQualifiedName().contentEquals("java.lang.String")) {
269+
} else if (lit.getType().getQualifiedName().equals("java.lang.String")) {
268270
// Only taking care of strings inside refinements
271+
} else if (type.equals(Utils.NULL_TYPE)) {
272+
// Skip null literals
269273
} else {
270274
throw new NotImplementedException(
271275
String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName()));

liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ public class Utils {
3535
public static final String SHORT = "short";
3636
public static final String LONG = "long";
3737
public static final String FLOAT = "float";
38+
public static final String NULL_TYPE = "<nulltype>";
3839

3940
private static final Set<String> DEFAULT_NAMES = Set.of("old", "length", "addToIndex", "getFromIndex");
4041

0 commit comments

Comments
 (0)