Skip to content

Commit

Permalink
Improved compilation scheme for enums.
Browse files Browse the repository at this point in the history
Now that we allow choosing values for enum constants, there are two
compilation schemes for enums (i.e., data types where no constructor
takes arguments).
- C11 enums, i.e., `typedef enum { A = 0xff, ... } t;`. These are
  mandated to have type `int` in C11; C23 allows choosing the width, but
  we don't yet assume C23. We assume `sizeof int == 4` and error out if
  any of the user-chosen constants exceed the range of `int`.
- Macros. We cannot represent arithmetic on enum constants, so there are
  no issues about integer promotions, or a constant being sign-extended
  for the wrong reasons. We just print out integer literals, and try the
  first type that fits all possible values for the enum type, with a
  preference for unsigned types.

This fixes AeneasVerif/eurydice#123
  • Loading branch information
msprotz committed Jan 8, 2025
1 parent dda5c07 commit 9063561
Show file tree
Hide file tree
Showing 21 changed files with 283 additions and 251 deletions.
44 changes: 22 additions & 22 deletions krmllib/hints/C.Endianness.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions krmllib/hints/C.Failure.fst.hints

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 9063561

Please sign in to comment.