Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

bvSliceBE too restrictive. #113

Closed
robdockins opened this issue Apr 14, 2021 · 0 comments · Fixed by #129
Closed

bvSliceBE too restrictive. #113

robdockins opened this issue Apr 14, 2021 · 0 comments · Fixed by #129
Assignees
@robdockins
Labels
bug Something isn't working

Comments

@robdockins
Copy link
Contributor

CF GaloisInc/saw-script#1166

%< ---------------------------------------------------
Revision: 8402ae2
Branch: HEAD
Location: bvSliceBE
Message: invalid arguments to slice: 128 0 from vector of length 128
CallStack (from HasCallStack):
panic, called at src/What4/Panic.hs:17:9 in what4-1.0.0.0.99-inplace:What4.Panic
panic, called at src/What4/SWord.hs:325:5 in what4-1.0.0.0.99-inplace:What4.SWord
%< ---------------------------------------------------

A slice of 0 bits is rejected by the SWord module with a panic, but it should probably just be accepted instead and return the distinguished ZBV value instead.
@robdockins robdockins added the bug Something isn't working label Apr 14, 2021
@robdockins robdockins self-assigned this Jun 11, 2021
robdockins added a commit that referenced this issue Jun 11, 2021
@robdockins
Relax the failure conditions for bvSliceBE and bvSliceLE.
cabb677 
Previously, these would panic if a 0-bit slice was requested.  Instead,
they now return the distinguished `ZBV` 0-length bitvector value.

Minor other tweaks.

Fixes #113
@robdockins robdockins mentioned this issue Jun 11, 2021
Merged
robdockins added a commit that referenced this issue Jun 14, 2021
@robdockins
Relax the failure conditions for bvSliceBE and bvSliceLE.
2964391 
Previously, these would panic if a 0-bit slice was requested.  Instead,
they now return the distinguished `ZBV` 0-length bitvector value.

Minor other tweaks.

Fixes #113
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robdockins robdockins

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Relax the failure conditions for bvSliceBE and bvSliceLE. GaloisInc/what4
1 participant
@robdockins