Skip to content

Commit 707afb1

Browse files
committed
Add Missing Binding
1 parent f8d3f3e commit 707afb1

File tree

2 files changed

+17
-1
lines changed

2 files changed

+17
-1
lines changed
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Ghost;
4+
import liquidjava.specification.Refinement;
5+
import liquidjava.specification.RefinementPredicate;
6+
import liquidjava.specification.StateRefinement;
7+
import liquidjava.specification.StateSet;
8+
9+
@Ghost("int progress")
10+
@StateSet({"downloading", "completed"})
11+
public class CorrectStateAndParameterRefinementThis {
12+
13+
@StateRefinement(from = "downloading(this)", to = "progress(this) == percentage")
14+
public void updateProgress(@Refinement("percentage > progress(this)") int percentage) {}
15+
}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,7 @@ private static Predicate createStatePredicate(String value, String targetClass,
216216
CtTypeReference<?> r = tc.getFactory().Type().createReference(targetClass);
217217
String nameOld = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
218218
String name = String.format(Formats.INSTANCE, Keys.THIS, tc.getContext().getCounter());
219+
tc.getContext().addVarToContext(Keys.THIS, r, new Predicate(), e);
219220
tc.getContext().addVarToContext(name, r, new Predicate(), e);
220221
tc.getContext().addVarToContext(nameOld, r, new Predicate(), e);
221222
// TODO REVIEW!!
@@ -616,4 +617,4 @@ private static List<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
616617
.getCanonicalName().contentEquals("liquidjava.specification.StateRefinement"))
617618
.collect(Collectors.toList());
618619
}
619-
}
620+
}

0 commit comments

Comments
 (0)