diff --git a/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java new file mode 100644 index 00000000..4f7190cf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java @@ -0,0 +1,17 @@ +package testSuite.classes.forward_field_read_correct; + +import liquidjava.specification.Refinement; + +public class ReadBefore { + private final Job job = new Job(); + + @Refinement("_ >= 0") + public int get() { + return job.port; + } + + static class Job { + @Refinement("_ >= 0") + int port; + } +} 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 bf6dcc99..56475917 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 @@ -308,6 +308,10 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral))); } else if (tryStaticFinalConstantRefinement(fieldRead)) { // refinement metadata set by helper + } else if (fieldRead.getVariable().getDeclaration() != null) { + Predicate declared = getRefinementFromAnnotation(fieldRead.getVariable().getDeclaration()) + .orElseGet(Predicate::new); + fieldRead.putMetadata(Keys.REFINEMENT, declared.substituteVariable(fieldName, Keys.WILDCARD)); } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE?