diff --git a/regression/cbmc/gcc_enum_mode_attribute/main.c b/regression/cbmc/gcc_enum_mode_attribute/main.c new file mode 100644 index 00000000000..e815340cdfc --- /dev/null +++ b/regression/cbmc/gcc_enum_mode_attribute/main.c @@ -0,0 +1,37 @@ +#include + +// An enum with __attribute__((mode(...))). For a mode name we special-case +// (__QI__ etc.) the enum gets that width; for one we don't (e.g. plain +// "byte"), we must fall back to the enum's underlying bitvector -- NOT the +// c_enum_tag, which previously made the enum's underlying type its own tag +// (a cycle) and crashed pointer_offset_bits / alignment. Used by some +// kernel/crypto headers (net/rxrpc, crypto/krb5). +enum E +{ + A, + B, + C +} __attribute__((mode(__QI__))); +enum F +{ + X, + Y +} __attribute__((mode(byte))); + +struct s +{ + enum E e; + enum F f; + int tail; +}; + +int main(void) +{ + struct s v; + v.e = A; + v.f = X; + v.tail = 0; + assert(v.e == A); + // must be able to compute sizeof/layout without crashing + return (int)sizeof(struct s) + v.tail; +} diff --git a/regression/cbmc/gcc_enum_mode_attribute/test.desc b/regression/cbmc/gcc_enum_mode_attribute/test.desc new file mode 100644 index 00000000000..67557b7e34e --- /dev/null +++ b/regression/cbmc/gcc_enum_mode_attribute/test.desc @@ -0,0 +1,14 @@ +CORE gcc-only +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +^CONVERSION ERROR$ +-- +An enum with __attribute__((mode(...))) must not produce a self-referential +underlying type (enum whose underlying type is its own c_enum_tag), which +crashed pointer_offset_bits/alignment. Covers a special-cased mode (__QI__) +and a fall-back mode name (byte). diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 2362e3966f6..62a23a7d137 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -245,8 +245,13 @@ void c_typecheck_baset::typecheck_type(typet &type) c_index_type(), unsigned_int_type(), from_integer(4, size_type())); } } - else // give up, just use subtype - result = to_type_with_subtype(type).subtype(); + else // give up, just use the (resolved) underlying type. For an + // enum subtype this is the enum's underlying bitvector, NOT the + // c_enum_tag -- using the tag would make the enum's underlying + // type its own tag (a cycle), which later crashes + // pointer_offset_bits/alignment. This happens for mode names we + // don't special-case (e.g. mode(byte) without underscores). + result = underlying_type; // save the location result.add_source_location()=type.source_location();