|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002249||Frama-C||Kernel||public||2016-10-13 17:24||2016-12-05 20:30|
|Platform||Aluminium-20160501||OS||xbuntu 64bit||OS Version|
|Product Version||Frama-C Aluminium|
|Target Version||Fixed in Version||Frama-C GIT, precise the release id|
|Summary||0002249: __attribute__((aligned(0))) tacitly causes sizeof computation to fail|
|Description||Running "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.
|Tags||No tags attached.|
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.
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.
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.
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.
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.
|Fixed in Frama-C Silicon.|
|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|