Preserve refinement on forward declared field reads (fix #316)

Author: rcosta358

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;
+    }
+}

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

@@ -308,6 +308,10 @@ public <T> void visitCtFieldRead(CtFieldRead<T> 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?