__attribute__((aligned(0))) tacitly causes sizeof computation to fail
ID0002249: This issue was created automatically from Mantis Issue 2249. Further discussion may take place here.
|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|
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.