From 8eaff6bf3933f2213ae85584009e05123c40fa65 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 10:47:14 +0200 Subject: clightgen: handle empty names given to padding bit fields In the Clight AST, padding bit fields (such as `int : 6;`) in composite declarations are given an ident that corresponds to the empty string. Previously, clightgen would give name `_` to this ident, but this is not valid Coq. This commit gives name `empty_ident` to the empty ident. This name does not start with an underscore, so it cannot conflict with the names for regular idents, which all start with `_`. --- test/clightgen/bitfields.c | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/clightgen/bitfields.c (limited to 'test') diff --git a/test/clightgen/bitfields.c b/test/clightgen/bitfields.c new file mode 100644 index 00000000..34f6a686 --- /dev/null +++ b/test/clightgen/bitfields.c @@ -0,0 +1,13 @@ +struct s { + int a: 10; + char : 6; + _Bool b : 1; + int : 0; + short c: 7; +}; + +int f(void) +{ + struct s x = { -1, 1, 2 }; + return x.a + x.b + x.c; +} -- cgit