Fix Field Initialization

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/context/Context.java

@@ -47,6 +47,14 @@ public void clearInstanceVariables() {
         ctxInstanceVars = new ArrayList<>();
     }
 
+    public void restoreInstanceVariables() {
+        for (RefinedVariable variable : getCtxVars()) {
+            if (variable instanceof Variable) {
+                ((Variable) variable).getLastInstance().ifPresent(this::addInstanceVariable);
+            }
+        }
+    }
+
     public void reinitializeAllContext() {
         reinitializeContext();
         ctxFunctions = new ArrayList<>();

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

@@ -107,6 +107,7 @@ public <A extends Annotation> void visitCtAnnotationType(CtAnnotationType<A> ann
     public <T> void visitCtConstructor(CtConstructor<T> constructor) {
         context.clearInstanceVariables();
         context.enterContext();
+        context.restoreInstanceVariables();
         mfc.loadFunctionInfo(constructor);
         try {
             super.visitCtConstructor(constructor);
@@ -121,6 +122,7 @@ public <T> void visitCtConstructor(CtConstructor<T> constructor) {
     public <R> void visitCtMethod(CtMethod<R> method) {
         context.clearInstanceVariables();
         context.enterContext();
+        context.restoreInstanceVariables();
         if (!method.getSignature().equals("main(java.lang.String[])")) {
             mfc.loadFunctionInfo(method);
         }
@@ -266,6 +268,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");