Skip to content

Commit e081e5e

Browse files
committed
Fix Instance Variable Leak Between Methods
1 parent d91f256 commit e081e5e

3 files changed

Lines changed: 23 additions & 0 deletions

File tree

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class ErrorRecursiveSiblingParameter {
6+
7+
int fibonacci(@Refinement("_ > 0") int n) {
8+
if (n == 1)
9+
return 1;
10+
else
11+
return fibonacci(n - 1) + fibonacci(n - 2); // Refinement Error
12+
}
13+
14+
int factorial(@Refinement("_ > 0") int n) {
15+
return n * factorial(n - 1); // Refinement Error
16+
}
17+
}

liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,10 @@ public static Context getInstance() {
4040
public void reinitializeContext() {
4141
ctxVars = new Stack<>();
4242
ctxVars.add(new ArrayList<>()); // global vars
43+
clearInstanceVariables();
44+
}
45+
46+
public void clearInstanceVariables() {
4347
ctxInstanceVars = new ArrayList<>();
4448
}
4549

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,7 @@ public <A extends Annotation> void visitCtAnnotationType(CtAnnotationType<A> ann
105105

106106
@Override
107107
public <T> void visitCtConstructor(CtConstructor<T> constructor) {
108+
context.clearInstanceVariables();
108109
context.enterContext();
109110
mfc.loadFunctionInfo(constructor);
110111
try {
@@ -117,6 +118,7 @@ public <T> void visitCtConstructor(CtConstructor<T> constructor) {
117118
}
118119

119120
public <R> void visitCtMethod(CtMethod<R> method) {
121+
context.clearInstanceVariables();
120122
context.enterContext();
121123
if (!method.getSignature().equals("main(java.lang.String[])")) {
122124
mfc.loadFunctionInfo(method);

0 commit comments

Comments
 (0)