Fix Field Initialization

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/state_field_initializer_correct/StateFieldInitializer.java

@@ -0,0 +1,23 @@
+package testSuite.classes.state_field_initializer_correct;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+public class StateFieldInitializer {
+
+    private final Obj obj = new Obj();
+
+    public void test() {
+        obj.foo();
+    }
+}
+
+@Ghost("boolean ready")
+class Obj {
+
+    @StateRefinement(to="ready(this)")
+    Obj() {}
+
+    @StateRefinement(from="ready(this)")
+    void foo() {}
+}

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

@@ -262,6 +262,11 @@ public <T> void visitCtField(CtField<T> f) {
             ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name);
         }
         RefinedVariable v = context.addVarToContext(name, f.getType(), ret, f);
+        if (f.getAssignment() != null) {
+            Predicate refinement = getRefinement(f.getAssignment());
+            checkVariableRefinements(refinement != null ? refinement : new Predicate(), name, f.getType(), f, f);
+            AuxStateHandler.addStateRefinements(this, name, f.getAssignment());
+        }
         getMessageFromAnnotation(f).ifPresent(v::setMessage);
         if (v instanceof Variable) {
             ((Variable) v).setLocation("this");