diff --git a/liquidjava-example/src/main/java/testSuite/classes/state_field_initializer_correct/StateFieldInitializer.java b/liquidjava-example/src/main/java/testSuite/classes/state_field_initializer_correct/StateFieldInitializer.java
new file mode 100644
index 00000000..ae3c3f51
--- /dev/null
+++ b/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() {}
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
index ddb55cf3..660a92d9 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java
+++ b/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<>();
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 84d90a89..bf6dcc99 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
@@ -107,6 +107,7 @@ public void visitCtAnnotationType(CtAnnotationType ann
public void visitCtConstructor(CtConstructor constructor) {
context.clearInstanceVariables();
context.enterContext();
+ context.restoreInstanceVariables();
mfc.loadFunctionInfo(constructor);
try {
super.visitCtConstructor(constructor);
@@ -121,6 +122,7 @@ public void visitCtConstructor(CtConstructor constructor) {
public void visitCtMethod(CtMethod method) {
context.clearInstanceVariables();
context.enterContext();
+ context.restoreInstanceVariables();
if (!method.getSignature().equals("main(java.lang.String[])")) {
mfc.loadFunctionInfo(method);
}
@@ -266,6 +268,11 @@ public void visitCtField(CtField 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");