Fix rewrites for the cpp backend #1509
Merged
Conversation
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
Test Results 16 files 35 suites 0s ⏱️ Results for commit c593f2a. ♻️ This comment has been updated with latest results. |
Alasdair
reviewed
Oct 14, 2025
Collaborator
|
If I check out your RISC-V PR and built it with this commit, then |
Set the target name in the rewrites to 'cpp' for the C++ backend.
Timmmm
force-pushed
the
user/timh/cpp_rewrites
branch
2 times, most recently
from
d0d5864 to
4ad7655
Compare
Timmmm
changed the title
Contributor
Author
|
Ah I think probably it was getting confused with the missing |
Contributor
Author
|
Hmm not sure why the tests are still failing though... |
Collaborator
|
I think they just needed a |
jn80842
pushed a commit
to GaloisInc/sail
that referenced
this pull request
Dec 11, 2025
* Fix rewrites for the cpp backend Set the target name in the rewrites to 'cpp' for the C++ backend. * Adjust failing C++ tests
Alasdair
added a commit
to Alasdair/opam-repository
that referenced
this pull request
Dec 22, 2025
CHANGES: This is bugfix release for Sail 0.20. It includes fixes for the following issues, among others: * rems-project/sail#1532 * rems-project/sail#1529 * rems-project/sail#1512 * rems-project/sail#1509 * rems-project/sail#1554 It also includes various improvements to the Sail formatter, and some improvements to the loop syntax that should make while and foreach loops slightly more consistent. This point release also includes the change that unifies the `bit` type with the `bits(1)` type. In principle, this means that strictly more programs should be permitted than before, so we have decided to forgo a major version increment for this. The change may be noticable to those using Sail generated theorem prover definitions.
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.
I noticed a weird issue with the C++ backend (RISC-V PR). Basically where we have something like this:
It was no longer using the external
cppversion and instead always falling back to the Sail= falseimplementation. If I comment out thefunction get_config_print_instr () = falsethen it works fine.This PR fixes that.