Skip to content

Commit b8f8120

Browse files
Preserve guards for blank primitive captures
1 parent 067cf95 commit b8f8120

2 files changed

Lines changed: 14 additions & 4 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/CorrectDeferredCallbackState.java‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,4 +89,15 @@ void immutableCaptureGuard(int n, boolean choose) {
8989
}
9090
}
9191

92+
void blankPrimitiveCaptureGuard(int input) {
93+
int n;
94+
n = input;
95+
if (n > 0) {
96+
Runnable later = () -> {
97+
@Refinement("_ > 0") int positive = n;
98+
};
99+
@Refinement("_ > 0") int stillPositive = n;
100+
}
101+
}
102+
92103
}

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -437,10 +437,9 @@ private Set<String> immutableLambdaCaptureNames(CtLambda<?> lambda) {
437437
if (access instanceof CtFieldAccess<?> || access.getType() == null || !access.getType().isPrimitive()
438438
|| declaration == null || declaration.hasParent(lambda))
439439
continue;
440-
CtExecutable<?> executable = declaration instanceof CtParameter<?> parameter
441-
? parameter.getParent(CtExecutable.class) : declaration.getParent(CtExecutable.class);
442-
if (executable == null || executable.getElements(new TypeFilter<>(CtVariableWrite.class)).stream()
443-
.anyMatch(write -> write.getVariable().getDeclaration() == declaration))
440+
// Java requires captured locals and parameters to be final or effectively final, including blank
441+
// locals assigned before capture. Their primitive values cannot change before invocation.
442+
if (!(declaration instanceof CtLocalVariable<?> || declaration instanceof CtParameter<?>))
444443
continue;
445444
names.add(access.getVariable().getSimpleName());
446445
}

0 commit comments

Comments
 (0)