2021-03-03 02:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002249Frama-CKernelpublic2016-12-05 20:30
Assigned Tomaroneze 
PlatformAluminium-20160501OSxbuntu 64bitOS Version
Product VersionFrama-C Aluminium 
Target VersionFixed in VersionFrama-C GIT, precise the release id 
Summary0002249: __attribute__((aligned(0))) tacitly causes sizeof computation to fail
DescriptionRunning "frama-c -val aaa.c" on the attached program issues the warnings:

[value] Computing initial state
aaa.c:6:[kernel] warning: division by zero. assert sizeof(struct _st) ≢ 0;
aaa.c:6:[value] Evaluation of initializer '(int)((unsigned int)1000 / sizeof(struct _st))' failed
[value] Initial state computed

When the "aligned(0)" attribute is omitted, the warning disappears. While it is acceptible that the Frama-C value analysis doesn't support all esoteric gcc contructs (like __attribute__), issueing a warning that "alignied(0)" isn't supported would help the user to understand the reasons for the warning.
TagsNo tags attached.
Attached Files
  • c file icon aaa.c (138 bytes) 2016-10-13 17:24 -
    struct _st {
       char mem;
    } __attribute__((__packed__, __aligned__(0)));
    int const sz = 1000 / sizeof(struct _st);
    void main(void) {}
    c file icon aaa.c (138 bytes) 2016-10-13 17:24 +
  • c file icon aaa2.c (110 bytes) 2016-10-17 11:59 -
    #pragma pack(0)
    struct _st {
       char mem;
    int const sz = 1000 / sizeof(struct _st);
    void main(void) {}
    c file icon aaa2.c (110 bytes) 2016-10-17 11:59 +




maroneze (administrator)

Thanks for the report.

Some work has been done on this already, but it probably won't be ready for Silicium, unfortunately.

Just out of curiosity, is there a specific semantics associated to align(0)? The GCC reference does not mention it explicitly (https://gcc.gnu.org/onlinedocs/gcc/Common-Type-Attributes.html#Common-Type-Attributes), and from there I would guess that align(1) and align(0) would behave in roughly the same way, since a minimum alignment of 1 should be enough in most cases. Maybe there are considerations about 0-length bitfields or other members? Or something related to MSVC emulation of packing pragmas?

Also, if I try your example on GCC (5.4.0) or Clang (3.8.0), I get errors about "requested alignment is not a positive power of 2". We sometimes recommend trying to compile the code (with enabled warnings, if possible) using GCC and/or Clang, before giving it to Frama-C, since there are known cases where syntactically invalid programs may end up being accepted by Frama-C. This is rare, but possible.

Anyway, the behavior you reported will be fixed, but if there is a special semantics for aligned(0), we may try to take it into account. Otherwise, we will consider GCC's behavior and report it as an error.


maroneze (administrator)

I found some mentions to #pragma pack(0), which apparently would have meant "disable packing" in the past. Since Frama-C translates such pragmas into __aligned__ attributes, it could make sense to allow them (and therefore aligned(0)) in such cases.

However, the official up-to-date documentations I found for both GCC and MSVC no longer indicate this. MSVC explicitly says that 1, 2, 4, 8 and 16 are the only valid values. And because GCC and Clang both reject aligned(0), we are going to emit a warning and ignore the attribute in Frama-C. Idem for #pragma pack(0).

Should someone need it in the future we might consider changing it, but for now this solution seems the best one.


Jochen (reporter)

The code was generated due to a "#pragma pack(0)", as I now realized. Use e.g. "frama-c -val aaa2.c -print" on the newly attached program.

In the original version, I used a Frama-C option "-cpp-command 'gcc -C -E -D... -I...'", but the effect is the same: it generates "__attribute__((__packed__, __aligned__(0)))". However, running "gcc -C -E aaa2.c" alone does not generate any attribute. So it appears that Frama-C actually has a problem with "#pragma pack(0)".

Running "gcc -C -O9 -Wall aaa2.c" gives just one warning, viz. "return type of ‘main’ is not ‘int’", so "#pragma pack(0)" seams to be good C, although I don't understand its meaning.


maroneze (administrator)

Indeed, GCC accepts `#pragma pack(0)` even though MSVC itself emits a warning.

Since the GCC doc does not mention it explicitly, a bug has been opened to understand if this is intentional (and if so, what is the expected behavior) or not, and we will follow their behavior.

There are indeed some known issues with the translation of #pragma pack into aligned attributes, and this is why the fixes are more complex than it seems at first sight. Note that this is not how GCC operates (hence why gcc -E does not show it), but because Frama-C has a source merging stage that is different from GCC's (you can see it as similar to linking in a compiler, but Frama-C is not a compiler, so some things are slightly different), we use this transformation. Still, in the end, the Frama-C code should behave exactly like GCC's. This is currently not true for #pragma pack(0), so we will fix it.


maroneze (administrator)

In the absence of replies in GCC's bugzilla (either confirming or denying it as a bug), we opted for the following behavior: `#pragma pack(0)` is accepted in GCC mode, and it disables packing, to emulate GCC's current behavior (as inferred from tests). However, because the behavior is not documented, Frama-C emits a warning. This should avoid silent unexpected behavior, but without preventing some programs from parsing, and thus seems a good compromise.

Fix committed to post-Silicon master, will be available in Phosporus.


yakobowski (manager)

Fixed in Frama-C Silicon.

-Issue History
Date Modified Username Field Change
2016-10-13 17:24 Jochen New Issue
2016-10-13 17:24 Jochen Status new => assigned
2016-10-13 17:24 Jochen Assigned To => yakobowski
2016-10-13 17:24 Jochen File Added: aaa.c
2016-10-13 18:07 maroneze Note Added: 0006270
2016-10-13 18:07 maroneze Assigned To yakobowski => maroneze
2016-10-13 18:07 maroneze Status assigned => confirmed
2016-10-13 19:33 yakobowski Category Plug-in > value analysis => Kernel
2016-10-14 11:28 maroneze Note Added: 0006274
2016-10-17 11:59 Jochen File Added: aaa2.c
2016-10-17 12:12 Jochen Note Added: 0006278
2016-10-17 13:44 maroneze Note Added: 0006279
2016-11-17 22:07 maroneze Note Added: 0006286
2016-11-17 22:07 maroneze Status confirmed => resolved
2016-11-17 22:07 maroneze Fixed in Version => Frama-C GIT, precise the release id
2016-11-17 22:07 maroneze Resolution open => fixed
2016-12-05 20:30 yakobowski Status resolved => closed
2016-12-05 20:30 yakobowski Note Added: 0006298
+Issue History