From 4ddc546ec2f96e577339a4f4c766eee1cedd038f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Fri, 7 Aug 2026 00:29:35 +0100 Subject: [PATCH] Fix Field Initialization --- .../StateFieldInitializer.java | 23 +++++++++++++++++++ .../RefinementTypeChecker.java | 5 ++++ 2 files changed, 28 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/state_field_initializer_correct/StateFieldInitializer.java 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/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 33b5198c..e49cc385 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 @@ -262,6 +262,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");