__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.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002249 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| Reporter | Jochen | Assigned To | maroneze | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | always |
| 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 |
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.