Remove use of partial fields and add warning. #111
Merged
Conversation
This file contains 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
Partial fields are the situation where an ADT is defined with record syntax. The field accessors are of type `ADT -> field`, but the field is only valid for one constructor of the ADT, so proper usage requires matching on the constructor before using field accessors, and omitting this matching can lead to invalid accesses. This change modifies the only use of this in What4 to ensure that the Record types are not ADT's and vice-versa.
robdockins
approved these changes
Mar 25, 2021
brianhuffman
pushed a commit
to GaloisInc/saw-script
that referenced
this pull request
Apr 8, 2021
This patch includes the following submodule PRs: - GaloisInc/what4#111 - GaloisInc/crucible#699
RyanGlScott
added a commit
that referenced
this pull request
May 10, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Partial fields are the situation where an ADT is defined with record
syntax. The field accessors are of type
ADT -> field, but the fieldis only valid for one constructor of the ADT, so proper usage requires
matching on the constructor before using field accessors, and omitting
this matching can lead to invalid accesses.
This change modifies the only use of this in What4 to ensure that the
Record types are not ADT's and vice-versa.