crucible: Add a GlobalPair to AbortedExit
#1331
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
langston-barrett
force-pushed
the
lb/abort-globals
branch
from
07a1425 to
e3a3280
Compare
Contributor
Author
|
Will wait for #1333 and rebase onto that (moving the CHANGELOG entries to the |
Of all of the constructors of `ExecState`, `ResultState` of `AbortedExit` was the only one from which one could not obtain a `SymGlobalState`. Not sure why this was, it doesn't seem necessary. Fixes GaloisInc#1326.
langston-barrett
force-pushed
the
lb/abort-globals
branch
from
e3a3280 to
97b41db
Compare
RyanGlScott
approved these changes
Mar 25, 2025
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Mar 27, 2025
This bumps the `crucible` submodule, bringing in the changes from GaloisInc/crucible#1331 in the process. This requires some minor code changes to account for `AbortedExit` now having a `GlobalPair`.
RyanGlScott
added a commit
to GaloisInc/asl-translator
that referenced
this pull request
Apr 9, 2025
This bumps the following submodules: * `crucible`, to bring in the changes from GaloisInc/crucible#1331 (the primary purpose of this patch) * `what4`, which is necessary to stay in sync with `crucible`. GaloisInc/crucible#1331 adds a new field to `AbortedExit`, which `asl-translator` pattern-matches on in `Language.ASL`. As such, this patch also makes a minor code change to keep that particular bit of code compiling.
RyanGlScott
added a commit
to GaloisInc/macaw
that referenced
this pull request
Apr 9, 2025
This bumps the following submodules: * `crucible`, to bring in the changes from GaloisInc/crucible#1331 (the primary purpose of this patch) * `asl-translator`, to bring in the changes from GaloisInc/asl-translator#57 to stay in sync with `crucible`. * `what4`, which is necessary to stay in sync with `crucible`. GaloisInc/crucible#1331 adds a new field to `AbortedExit`, which `macaw-refinement` pattern-matches on in `Data.Macaw.Refinement.SymbolicExecution`. As such, this patch also makes a minor code change to keep that particular bit of code compiling.
RyanGlScott
added a commit
to GaloisInc/macaw
that referenced
this pull request
Apr 9, 2025
This bumps the following submodules: * `crucible`, to bring in the changes from GaloisInc/crucible#1331 (the primary purpose of this patch) * `asl-translator`, to bring in the changes from GaloisInc/asl-translator#57 to stay in sync with `crucible`. * `llvm-pretty`, `llvm-pretty-bc-parser`, and `what4`, which are necessary to stay in sync with `crucible`. GaloisInc/crucible#1331 adds a new field to `AbortedExit`, which `macaw-refinement` pattern-matches on in `Data.Macaw.Refinement.SymbolicExecution`. As such, this patch also makes a minor code change to keep that particular bit of code compiling.
RyanGlScott
added a commit
to GaloisInc/asl-translator
that referenced
this pull request
Apr 9, 2025
Bump submodules, adapt to changes in GaloisInc/crucible#1331
RyanGlScott
added a commit
to GaloisInc/macaw
that referenced
this pull request
Apr 9, 2025
Bump submodules, adapt to changes in GaloisInc/crucible#1331
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.
Of all of the constructors of
ExecState,ResultStateofAbortedExitwas the only one from which one could not obtain aSymGlobalState. Not sure why this was, it doesn't seem necessary.Fixes #1326.