Skip to content

Update Charon submodule to v0.1.88 - #4702

Merged
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:charon-update-v0.1.88-pr
Jul 30, 2026
Merged

Update Charon submodule to v0.1.88#4702
feliperodri merged 1 commit into
model-checking:mainfrom
tautschnig:charon-update-v0.1.88-pr

Conversation

@tautschnig

Copy link
Copy Markdown
Member

Advance the Charon pin from v0.1.87 (c4af1eaf) to v0.1.88 (607f5683), continuing the incremental effort to catch the pinned Charon up with upstream (the endgame is dropping scripts/charon-patch.diff entirely).

Charon v0.1.88 turns calls from ULLBC statements into block terminators (RawTerminator::Call with an explicit target block), matching MIR's structure, and adds the no_ops_to_function_calls translation option (kept at the previous behavior).

Refresh scripts/charon-patch.diff so its hunks apply against the v0.1.88 sources (context-line drift only; the patch content is unchanged).

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Advance the Charon pin from v0.1.87 (c4af1eaf) to v0.1.88 (607f5683),
continuing the incremental effort to catch the pinned Charon up with upstream
(the endgame is dropping scripts/charon-patch.diff entirely).

Charon v0.1.88 turns calls from ULLBC statements into block terminators
(`RawTerminator::Call` with an explicit `target` block), matching MIR's
structure, and adds the `no_ops_to_function_calls` translation option (kept at
the previous behavior).

Refresh scripts/charon-patch.diff so its hunks apply against the v0.1.88
sources (context-line drift only; the patch content is unchanged).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Copilot AI review requested due to automatic review settings July 30, 2026 01:28
@tautschnig
tautschnig requested a review from a team as a code owner July 30, 2026 01:28

Copilot AI left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

@github-actions github-actions Bot added Z-EndToEndBenchCI Tag a PR to run benchmark CI Z-CompilerBenchCI Tag a PR to run benchmark CI labels Jul 30, 2026
@feliperodri
feliperodri added this pull request to the merge queue Jul 30, 2026
Merged via the queue into model-checking:main with commit a40c84b Jul 30, 2026
33 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants