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");