Skip to content

Commit 9063561

Browse files
committed
Improved compilation scheme for enums.
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
1 parent dda5c07 commit 9063561

21 files changed

+283
-251
lines changed

krmllib/hints/C.Endianness.fst.hints

Lines changed: 22 additions & 22 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

krmllib/hints/C.Failure.fst.hints

Lines changed: 2 additions & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)