From d0790051bdc85719903395877a7116313feba5d1 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:25:20 +0100 Subject: [PATCH 1/3] Treat operations and fields with unresolved types as unrefined (#388, #389, #390) When a class is not on the classpath (the usual case when one file of a project is verified), Spoon leaves the type of operations on its values, and the declaring type of its fields, unset, and the verifier crashed on them. - A binary operation whose type, or the type of one of its operands, is unknown is now a fresh unknown boolean for comparisons and logical operators, and is left unrefined otherwise; an operator assignment with such a right-hand side gives the variable an unknown value. - A negation of an operand with an unknown type is boolean; other unary operators on such operands are left unrefined. - A field whose declaring type is unknown is qualified with its name only, so it matches no known field, and is not treated as an enum constant. Unknown values carry no information, so a refinement that depends on them is reported as not provable rather than accepted; violations next to them are still reported (Error* fixtures). The example module excludes the *Unresolved* test cases from javac, as they import missing classes on purpose. Fixes #388 Fixes #389 Fixes #390 Co-Authored-By: Claude Opus 5.5 --- liquidjava-example/pom.xml | 104 +++++++++--------- .../CorrectUnresolvedBinaryOperator.java | 59 ++++++++++ .../CorrectUnresolvedFieldDeclaringType.java | 17 +++ .../CorrectUnresolvedUnaryOperator.java | 22 ++++ .../ErrorUnresolvedBinaryOperator.java | 18 +++ .../ErrorUnresolvedFieldDeclaringType.java | 18 +++ .../ErrorUnresolvedOperationValue.java | 14 +++ .../ErrorUnresolvedUnaryOperator.java | 18 +++ .../RefinementTypeChecker.java | 3 +- .../general_checkers/OperationsChecker.java | 61 +++++++++- .../src/main/java/liquidjava/utils/Utils.java | 2 + 11 files changed, 279 insertions(+), 57 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java diff --git a/liquidjava-example/pom.xml b/liquidjava-example/pom.xml index 0e1f58082..d029b288d 100644 --- a/liquidjava-example/pom.xml +++ b/liquidjava-example/pom.xml @@ -1,50 +1,54 @@ - - - 4.0.0 - liquidjava-example - liquidjava-example - 0.0.1-SNAPSHOT - liquidjava-example - jar - - - - - org.apache.maven.plugins - maven-compiler-plugin - ${pVersion.compiler} - - 20 - 20 - - - - - - - UTF-8 - 20 - 20 - - 4.13.1 - 1.3.0 - - 3.8.0 - 2.22.1 - - - - - org.mdkt.compiler - InMemoryJavaCompiler - ${version.memcompiler} - - - io.github.liquid-java - liquidjava-api - 0.0.7 - - - + + + 4.0.0 + liquidjava-example + liquidjava-example + 0.0.1-SNAPSHOT + liquidjava-example + jar + + + + + org.apache.maven.plugins + maven-compiler-plugin + ${pVersion.compiler} + + 20 + 20 + + + testSuite/**/*Unresolved*.java + + + + + + + + UTF-8 + 20 + 20 + + 4.13.1 + 1.3.0 + + 3.8.0 + 2.22.1 + + + + + org.mdkt.compiler + InMemoryJavaCompiler + ${version.memcompiler} + + + io.github.liquid-java + liquidjava-api + 0.0.7 + + + diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java new file mode 100644 index 000000000..14775088b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedBinaryOperator.java @@ -0,0 +1,59 @@ +package testSuite; + +import org.example.missing.Item; +import org.example.missing.Interrupts; + +import liquidjava.specification.Refinement; + +// Operations whose operand types cannot be resolved (classes not on the classpath) are unrefined (#388, #344) +@SuppressWarnings("unused") +public class CorrectUnresolvedBinaryOperator { + static boolean same(Item a, Item b) { + if (a.id() == b.id()) { + return true; + } + return false; + } + + static boolean comparedToConstant(Item p, int id) { + return p.getValue() == id; + } + + static void inLoop(Item embedding) { + for (int i = 0; i < embedding.length(); i++) { + } + } + + static void withKnownOperand(boolean someHandlerDefined) { + if (!someHandlerDefined || Interrupts.isInterruptsDisabled()) { + return; + } + } + + static boolean nested(Item x) { + return x.a() + 1 > 0; + } + + static String concatenation(Item i) { + return "Configuration is not an SQL config:" + i.name(); + } + + static void unknownVarNullCheck(Item x) { + var v = x.a(); + if (v == null) { + return; + } + } + + static void operatorAssignment(Item x) { + int c = 0; + c += x.a(); + } + + static void knownValuesStillUsed(Item x, int k) { + if (k > 0 && x.ok()) { + @Refinement("_ > 0") + int y = 1; + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java new file mode 100644 index 000000000..5ffb3609f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedFieldDeclaringType.java @@ -0,0 +1,17 @@ +package testSuite; + +import org.example.missing.Config; + +// Fields whose declaring class cannot be resolved (#390) +@SuppressWarnings("unused") +public class CorrectUnresolvedFieldDeclaringType { + private static final int MIN_ADMIN_PASSWORD_LENGTH = 8; + + static boolean shortPassword(Config config) { + return config.httpAdminPassword.length() < MIN_ADMIN_PASSWORD_LENGTH; + } + + void undeclaredField(Exception e) { + log.error("get host name error:{}", e.getMessage()); // e.g., a field generated by Lombok + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java new file mode 100644 index 000000000..6a1a83a7b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectUnresolvedUnaryOperator.java @@ -0,0 +1,22 @@ +package testSuite; + +import org.example.missing.Item; +import org.example.missing.Settings; + +// A negation of a call whose type cannot be resolved is an unknown boolean (#389) +@SuppressWarnings("unused") +public class CorrectUnresolvedUnaryOperator { + static void start(Settings settings) { + if (!settings.enabled()) { + return; + } + } + + static boolean negatedComparison(Item x) { + return !(x.a() == x.b()); + } + + static int negated(Item x) { + return -x.a(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java new file mode 100644 index 000000000..f9415b3e8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedBinaryOperator.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Item; + +import liquidjava.specification.Refinement; + +// A violation under a comparison of values whose types cannot be resolved is still reported (#388) +@SuppressWarnings("unused") +public class ErrorUnresolvedBinaryOperator { + static void positive(@Refinement("_ > 0") int x) { + } + + static void comparison(Item a, Item b) { + if (a.id() == b.id()) { + positive(0); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java new file mode 100644 index 000000000..1f932c93a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedFieldDeclaringType.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Config; + +import liquidjava.specification.Refinement; + +// A violation next to a field whose declaring class cannot be resolved is still reported (#390) +@SuppressWarnings("unused") +public class ErrorUnresolvedFieldDeclaringType { + static void positive(@Refinement("_ > 0") int x) { + } + + static void field(Config config) { + if (config.httpAdminPassword.length() < 8) { + positive(-2); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java new file mode 100644 index 000000000..5d85250e5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedOperationValue.java @@ -0,0 +1,14 @@ +package testSuite; + +import org.example.missing.Item; + +import liquidjava.specification.Refinement; + +// An operation whose operand types cannot be resolved has an unknown value (#388) +@SuppressWarnings("unused") +public class ErrorUnresolvedOperationValue { + static void unknownValue(Item x) { + @Refinement("_ > 0") + int y = x.a() + 1; // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java new file mode 100644 index 000000000..1877cb305 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorUnresolvedUnaryOperator.java @@ -0,0 +1,18 @@ +package testSuite; + +import org.example.missing.Settings; + +import liquidjava.specification.Refinement; + +// A violation under a negation of a call whose type cannot be resolved is still reported (#389) +@SuppressWarnings("unused") +public class ErrorUnresolvedUnaryOperator { + static void positive(@Refinement("_ > 0") int x) { + } + + static void negation(Settings settings) { + if (!settings.enabled()) { + positive(-1); // Expect: Refinement Error + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 995c59277..0ed24307a 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -335,7 +335,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { String targetName = fieldRead.getTarget().toString(); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), BuiltinFunctionPredicate.length(targetName, fieldRead))); - } else if (fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { + } else if (fieldRead.getVariable().getDeclaringType() != null + && fieldRead.getVariable().getDeclaringType().getDeclaration() instanceof CtEnum) { // only enums declared in the analyzed sources can be translated to SMT String target = fieldRead.getVariable().getDeclaringType().getSimpleName(); String enumLiteral = String.format(Formats.ENUM, target, fieldName); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 8e3877123..7294804e2 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -43,6 +43,7 @@ import spoon.reflect.declaration.CtExecutable; import spoon.reflect.declaration.CtType; import spoon.reflect.declaration.ParentNotInitializedException; +import spoon.reflect.reference.CtTypeReference; import spoon.reflect.reference.CtVariableReference; import spoon.support.reflect.code.CtIfImpl; @@ -74,6 +75,16 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr if (parent instanceof CtAnnotation) return; // Operations in annotations are not handled here + if (hasUnresolvedType(operator)) { + // an operand's type could not be resolved (e.g. its class is not on the classpath, #388): the value of a + // comparison or logical operation is an unknown boolean, and any other operation is left unrefined + if (!isBooleanOperator(operator.getKind())) + return; + CtTypeReference booleanType = operator.getFactory().Type().booleanPrimitiveType(); + putBooleanRefinement(operator, parent, createFreshValue(operator, booleanType, new Predicate())); + return; + } + String type = operator.getType().getQualifiedName(); if (type.equals("java.lang.String")) return; @@ -93,10 +104,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr } List types = Arrays.asList(Types.IMPLEMENTED); if (type.contentEquals("boolean")) { - operator.putMetadata(Keys.REFINEMENT, oper); - if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator - || parent instanceof CtReturn) - operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); + putBooleanRefinement(operator, parent, oper); } else if (types.contains(type)) { operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); } else { @@ -105,6 +113,34 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr // TODO ADD TYPES } + private static void putBooleanRefinement(CtBinaryOperator operator, CtElement parent, Predicate oper) { + operator.putMetadata(Keys.REFINEMENT, oper); + if (parent instanceof CtLocalVariable || parent instanceof CtUnaryOperator + || parent instanceof CtReturn) + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), oper)); + } + + /** + * Whether the type of the operation, or of one of its operands (looking inside nested operations), could not be + * resolved, in which case Spoon leaves it unset + */ + private static boolean hasUnresolvedType(CtExpression e) { + if (e.getType() == null) + return true; + if (e instanceof CtBinaryOperator binop) + return hasUnresolvedType(binop.getLeftHandOperand()) || hasUnresolvedType(binop.getRightHandOperand()); + if (e instanceof CtUnaryOperator unop) + return hasUnresolvedType(unop.getOperand()); + return false; + } + + private static boolean isBooleanOperator(BinaryOperatorKind kind) { + return switch (kind) { + case EQ, NE, LT, LE, GT, GE, AND, OR, INSTANCEOF -> true; + default -> false; + }; + } + /** * Builds the refinement for a operator assignment. Java operator assignments such as {@code x += y} are modeled as * {@code x = x + y}; the returned predicate refines the assigned value as {@code _ == current(x) rhs}. @@ -114,6 +150,8 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator String op = getOperatorFromKind(assignment.getKind()); if (op == null) // x |= y, x <<= n, ...: no counterpart in the integer logic, so the new value is unknown return new Predicate(); + if (hasUnresolvedType(assignment.getAssignment())) // the right-hand side has an unknown type (#388) + return new Predicate(); Predicate left = getCurrentVariableValue(assignedName); Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment()); Predicate operation = Predicate.createOperation(left, op, right); @@ -165,6 +203,13 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro } } + CtTypeReference type = ex.getType(); + if (type == null) { + // the operand's type could not be resolved (#389): a negation is still boolean, anything else is unrefined + if (operator.getKind() != UnaryOperatorKind.NOT) + return; + type = operator.getFactory().Type().booleanPrimitiveType(); + } Predicate metadata = rtc.getRefinement(ex); String newName = !name.equals(Formats.FRESH) ? String.format(Formats.INSTANCE, name, rtc.getContext().getCounter()) @@ -176,7 +221,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro Predicate opS = unOp.substituteVariable(Keys.WILDCARD, newName); all = p instanceof CtIf ? opS : Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), opS); // TODO SEE IF () IN OPS IS NEEDED - rtc.getContext().addInstanceToContext(newName, ex.getType(), newMeta, operator); + rtc.getContext().addInstanceToContext(newName, type, newMeta, operator); operator.putMetadata(Keys.REFINEMENT, all); } @@ -424,9 +469,13 @@ private Predicate valueFromRefinement(CtExpression element, Predicate refinem } private Predicate createFreshValue(CtExpression element, Predicate refinement) { + return createFreshValue(element, element.getType(), refinement); + } + + private Predicate createFreshValue(CtExpression element, CtTypeReference type, Predicate refinement) { String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName); - rtc.getContext().addVarToContext(newName, element.getType(), freshRefinement, element); + rtc.getContext().addVarToContext(newName, type, freshRefinement, element); return Predicate.createVar(newName); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 018287e43..247b036cb 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -53,6 +53,8 @@ public static String qualifyName(String prefix, String name) { } public static String qualifyFieldName(CtFieldReference field) { + if (field.getDeclaringType() == null) // declaring class not resolved (#390): matches no known field + return "this#" + field.getSimpleName(); return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); } From fbc056e6d59fb4528be87880275dce0ae6771fce Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 13 Oct 2026 09:25:20 +0100 Subject: [PATCH 2/3] Add regression tests for var locals and yielded refined constructors (#344, #346, #347) These reproducers already verify on main: since Spoon parses at the project's compliance level (21 by default, #352, #368), a var local gets the static type of its initialiser instead of a type named "var", and switch expressions with yield are modelled correctly. With a pre-10 compliance level, the null type of a var comparison is now also handled as an unresolved type (#388). Fixes #344 Fixes #346 Fixes #347 Co-Authored-By: Claude Opus 5.5 --- .../main/java/testSuite/CorrectVarLocal.java | 28 +++++++++++++++++++ .../CorrectYieldRefinedConstructor.java | 21 ++++++++++++++ .../main/java/testSuite/ErrorVarLocal.java | 17 +++++++++++ .../ErrorYieldRefinedConstructor.java | 21 ++++++++++++++ 4 files changed, 87 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java b/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java new file mode 100644 index 000000000..1772fe3aa --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectVarLocal.java @@ -0,0 +1,28 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +// A var local has the static type of its initialiser (#344, #347) +@SuppressWarnings("unused") +@RefinementAlias("Port(int x) { 0 <= x && x <= 65535 }") +public class CorrectVarLocal { + static String name() { + return "x"; + } + + static void connect(@Refinement("Port(_)") int port) { + } + + static void nullCheck() { + var n = name(); + if (n == null) { + throw new IllegalArgumentException("no name"); + } + } + + static void refinedArgument() { + var port = 80; + connect(port); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java b/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java new file mode 100644 index 000000000..5404e5f67 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectYieldRefinedConstructor.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// Yielding a call to a refined constructor from a switch expression (#346) +@SuppressWarnings("unused") +public class CorrectYieldRefinedConstructor { + static class Conn { + public Conn(@Refinement("_ > 0") int port) { + } + } + + static Conn open(String scheme) { + return switch (scheme) { + case "tcp" -> { + yield new Conn(80); + } + default -> new Conn(1); + }; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java b/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java new file mode 100644 index 000000000..f23aff37a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorVarLocal.java @@ -0,0 +1,17 @@ +package testSuite; + +import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +// The value of a var local is still checked against a refined parameter (#347) +@SuppressWarnings("unused") +@RefinementAlias("Port(int x) { 0 <= x && x <= 65535 }") +public class ErrorVarLocal { + static void connect(@Refinement("Port(_)") int port) { + } + + static void refinedArgument() { + var port = 70000; + connect(port); // Expect: Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java b/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java new file mode 100644 index 000000000..d74bf5528 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorYieldRefinedConstructor.java @@ -0,0 +1,21 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +// The arguments of a refined constructor yielded from a switch expression are checked (#346) +@SuppressWarnings("unused") +public class ErrorYieldRefinedConstructor { + static class Conn { + public Conn(@Refinement("_ > 0") int port) { + } + } + + static Conn open(String scheme) { + return switch (scheme) { + case "tcp" -> { + yield new Conn(-1); // Expect: Refinement Error + } + default -> new Conn(1); + }; + } +} From 5eec1b5662d6eb0541c946bbcfd5508a7c83c403 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 14 Oct 2026 10:50:12 +0100 Subject: [PATCH 3/3] Drop issue numbers from code comments Co-Authored-By: Claude Opus 5.5 --- .../general_checkers/OperationsChecker.java | 6 +++--- .../src/main/java/liquidjava/utils/Utils.java | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 7294804e2..aa8d9d19b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -76,7 +76,7 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr return; // Operations in annotations are not handled here if (hasUnresolvedType(operator)) { - // an operand's type could not be resolved (e.g. its class is not on the classpath, #388): the value of a + // an operand's type could not be resolved (e.g. its class is not on the classpath): the value of a // comparison or logical operation is an unknown boolean, and any other operation is left unrefined if (!isBooleanOperator(operator.getKind())) return; @@ -150,7 +150,7 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator String op = getOperatorFromKind(assignment.getKind()); if (op == null) // x |= y, x <<= n, ...: no counterpart in the integer logic, so the new value is unknown return new Predicate(); - if (hasUnresolvedType(assignment.getAssignment())) // the right-hand side has an unknown type (#388) + if (hasUnresolvedType(assignment.getAssignment())) // the right-hand side has an unknown type return new Predicate(); Predicate left = getCurrentVariableValue(assignedName); Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment()); @@ -205,7 +205,7 @@ public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJErro CtTypeReference type = ex.getType(); if (type == null) { - // the operand's type could not be resolved (#389): a negation is still boolean, anything else is unrefined + // the operand's type could not be resolved: a negation is still boolean, anything else is unrefined if (operator.getKind() != UnaryOperatorKind.NOT) return; type = operator.getFactory().Type().booleanPrimitiveType(); diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 247b036cb..cf3042ea1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -53,7 +53,7 @@ public static String qualifyName(String prefix, String name) { } public static String qualifyFieldName(CtFieldReference field) { - if (field.getDeclaringType() == null) // declaring class not resolved (#390): matches no known field + if (field.getDeclaringType() == null) // declaring class not resolved: matches no known field return "this#" + field.getSimpleName(); return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); }