GeezerVison

The World Wide Web, restored to 800 pixels of glory.

GeezerVison is showing github.com — Fix Field Initialization by rcosta358 · Pull Request #281 · liquid-java/liquidjava

Fix Field Initialization #281

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

rcosta358 merged 2 commits into main from fix-field-initialization

Aug 11, 2026

Uh oh!

There was an error while loading. Please reload this page.

Merged

Fix Field Initialization #281

Show file tree

Hide file tree

Changes from all commits

Commits

Show all changes

2 commits

Select commit Hold shift + click to select a range

333d176

Fix Field Initialization

rcosta358 Aug 6, 2026

74dfda1

Fix Instance Variables

rcosta358 Aug 11, 2026

File filter

Filter by extension .java (3) All 1 file type selected

Viewed files

Clear filters

Conversations

Failed to load comments.

Uh oh!

There was an error while loading. Please reload this page.

Jump to

Jump to file

Failed to load files.

Uh oh!

There was an error while loading. Please reload this page.

Diff view

Unified

Split

Hide whitespace

Diff view

Unified

Split

Hide whitespace

There are no files selected for viewing

23 changes: 23 additions & 0 deletions 23 ...rc/main/java/testSuite/classes/state_field_initializer_correct/StateFieldInitializer.java

Show comments

View file

Open in desktop

Original file line number	Diff line number	Diff line change
		@@ -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() {}
		}

8 changes: 8 additions & 0 deletions 8 liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

Show comments

View file

Open in desktop

Original file line number	Diff line number	Diff line change
Expand Up		@@ -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<>();
Expand Down

7 changes: 7 additions & 0 deletions 7 ...verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

Show comments

View file

Open in desktop

Original file line number	Diff line number	Diff line change
Expand Up		@@ -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);
Expand All		@@ -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);
		}
Expand Down Expand Up		@@ -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");
Expand Down

Oops, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

Add this suggestion to a batch that can be applied as a single commit. This suggestion is invalid because no changes were made to the code. Suggestions cannot be applied while the pull request is closed. Suggestions cannot be applied while viewing a subset of changes. Only one suggestion per line can be applied in a batch. Add this suggestion to a batch that can be applied as a single commit. Applying suggestions on deleted lines is not supported. You must change the existing code in this line in order to create a valid suggestion. Outdated suggestions cannot be applied. This suggestion has been applied or marked resolved. Suggestions cannot be applied from pending reviews. Suggestions cannot be applied on multi-line comments. Suggestions cannot be applied while the pull request is queued to merge. Suggestion cannot be applied right now. Please check back later.

You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.