Bump Strata to 24b8f04e (source range fix for invariants), and update do/while bad invariant tests#453
Merged
Merged
Conversation
…ge-tests # Conflicts: # Strata # verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java
kadirayk
changed the title
fabiomadge
approved these changes
Jun 17, 2026
fabiomadge
left a comment
fabiomadge
left a comment
Collaborator
There was a problem hiding this comment.
Approving. Reviewed the full Strata delta: with #423 on main, this advances the pin by exactly one commit (8abb4630 + #1361 = 24b8f04e), plus the test updates. You've merged main in (head 49adb8b8), so it's cleanly mergeable; CI green on both platforms.
Substance holds: the per-invariant ranges work end-to-end — the ^^^^^^ carets are enforced assertions (the harness compares full ranges, not just counts), so this genuinely tests #1361. whileBadInvariant is a good negative regression, and the new methodsInvalid = 3 is it plus the two pre-existing failures. #428's StrataCLI wiring still holds.
fabiomadge
added a commit
that referenced
this pull request
Jun 17, 2026
The rebase carried the old submodule pin; align it with main (#453's bump, per-invariant source ranges).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
What was changed?
Bumped the Strata submodule from
e115b8ecto24b8f04e(nightly, "Per-invariant source ranges for loop-invariant diagnostics", #1361) and brought JVerify in line with the updated Laurel dialect.24b8f04e.VerifyDoWhiletest: updated the expected diagnostic fordoWhileBadInitialInvariantto the new, tighter per-invariant range (points at the invariant condition rather than the whole do-while statement); added a negative regression casewhileBadInvariant(invariant holds on entry but is not preserved by the loop body) with a matching diagnostic marker and doc comment; updated the@JVerifyTestcounts to enforce the new expectations (methodsInvalid = 3, errorCount = 3).This is not a user-visible behavior change for JVerify itself; it tracks the upstream Strata improvement to invariant diagnostic source ranges.
How has this been tested?
./gradlew buildpasses (compile + full test suite)./gradlew :verifier:test --tests "*VerifyDoWhile*" --rerun-taskspasses, exercising the updated and newly added invariant diagnostic cases.Fixes #437
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache-2.0.