Skip to content

Bump Charon#919

Merged
Nadrieril merged 2 commits into
AeneasVerif:mainfrom
N1ark:charon-1088
Apr 22, 2026
Merged

Bump Charon#919
Nadrieril merged 2 commits into
AeneasVerif:mainfrom
N1ark:charon-1088

Conversation

@N1ark
Copy link
Copy Markdown
Contributor

@N1ark N1ark commented Apr 8, 2026

Partner PR to AeneasVerif/charon#1088

@N1ark
Copy link
Copy Markdown
Contributor Author

N1ark commented Apr 8, 2026

@sonmarcho CI fails, could you explain to me why I am very unfamiliar with all this 🫠

@sonmarcho
Copy link
Copy Markdown
Member

This PR introduced a bug in the extraction: Aeneas now generates FunsExternal_Template files in situations when there are no opaque/axiomatized function definitions. As the corresponding FunsExternal files (with hand-written models for these opaque functions) are missing, build fails.

Comment thread src/llbc/LlbcAstUtils.ml Outdated
@N1ark N1ark force-pushed the charon-1088 branch 2 times, most recently from 9400379 to 9e8bf8b Compare April 17, 2026 13:45
Comment thread src/llbc/LlbcAstUtils.ml Outdated
Comment thread src/PrePasses.ml Outdated
Comment thread src/Translate.ml Outdated
@N1ark N1ark force-pushed the charon-1088 branch 4 times, most recently from 513bac8 to 3de1b3a Compare April 20, 2026 17:28
@N1ark
Copy link
Copy Markdown
Contributor Author

N1ark commented Apr 21, 2026

@sonmarcho addressed the comments! any other remarks or is this mergeable?:3

@sonmarcho
Copy link
Copy Markdown
Member

Sorry about that: I just approved :)

@Nadrieril Nadrieril merged commit de2a2db into AeneasVerif:main Apr 22, 2026
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants