fix: pattern match on chars#917
Open
clementblaudeau wants to merge 4 commits intoAeneasVerif:mainfrom
Open
Conversation
Add test for concrete and some symbolic matches
[expand_symbolic_int] is renamed into [expand_symbolic_literal], and made to support both integers (signed/unsigned) and chars. The sanity check ensures that the target list of literals has the right type wrt the symbolic value.
Author
|
I just saw #896, which I believe this PR subsumes. |
sonmarcho
reviewed
Apr 19, 2026
Member
sonmarcho
left a comment
sonmarcho
left a comment
There was a problem hiding this comment.
Sorry for taking so long to review this: I have been very busy lately... I have a minor remark but otherwise it looks good to me, thanks for this PR!
| (literal_as_integer int_ty) | ||
| (List.map literal_as_scalar values) | ||
| ctx | ||
| int_ty values ctx |
Member
There was a problem hiding this comment.
Could you rename int_ty to lit_ty?
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
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.
Context
This PR comes as a fix for #797: pattern-matching on chars was not supported. I've tried to keep the commits as minimal and logically separated as possible, but as it's my first contribution to this project, please tell me if the style is not right.
Example
used to throw an error, now produces
Fix
While pattern-match on concrete chars is easy, pattern-match on symbolic ones required a bit more work. The
expand_symbolic_intfunction was renamed intoexpand_symbolic_literaland now supports both ints (signed/unsigned) and chars. Downstream, a newExpandCharcase was added toexpansion. I've used Claude for some of the design/fix but reviewed it very carefully.Design choices
expand_symbolic_int, we could also duplicate it and create anexpand_symbolic_char.ExpandChar, we could merge it withExpandIntfixes #797