Lem and Coq fixes for C test suite #347
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
(broke some Lem tests)
It's used as a type checking hint, so dropping it causes later checking phases to fail.
- hex_str_upper primitive - tweak a couple of tests - check stderr output - add more expected failures
Necessary to avoid redundant patterns which aren't allowed in Coq.
- field names should always use id rewriting - parens in cons exps/pats - max_int and min_int built-ins
Necessary for some of the C tests suite; useful for warnings.
- rewrite complex patterns in top-level let bindings - print recursive function with implicit decreasing arguments properly - avoid built-in type "vec" - rerun effect inference when exhaustivity rewrite introduces a match failure - don't generate autocast for an argument with an existentially bound size - correct Coq built-ins in several tests - add expected test failures
Fixes a bug where a bitfield called (eg) B1 was renamed to B1' to avoid a clash, but one place used B1_bits and another B1'_bits
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.
No description provided.