forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 25
Open
Labels
Description
The C23 standard provides the following definition of structure type compatibility:
Two types are compatible types if they are the same. Additional rules for determining whether two
types are compatible are described in 6.7.3 for type specifiers, in 6.7.4 for type qualifiers, and in 6.7.7
for declarators.45) Moreover, two complete structure, union, or enumerated types declared with the
same tag are compatible if members satisfy the following requirements:
— there shall be a one-to-one correspondence between their members such that each pair of
corresponding members are declared with compatible types;
— if one member of the pair is declared with an alignment specifier, the other is declared with an
equivalent alignment specifier;
— and, if one member of the pair is declared with a name, the other is declared with the same
name.
For two structures, corresponding members shall be declared in the same orde
Compared to the previous versions of the standard, this permits re-defnition of the same structure specifier within a translation unit. Thus,
in the following example both declarations of struct S1 should be considered compatible:
struct S1 {
int a;
};
void fn(struct S1 { int a; } arg) {}However, when processed with CIL, the structure specifier from the function argument gets hoisted into the file scope and renamed to S1___0, which makes both definitions incompatible, thus breaking semantics of the original program. As a result, Goblint analysis performance is degraded too as it is unable to reason about conversions between these two types.
Reactions are currently unavailable