__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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information