View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001364 | Frama-C | Plug-in > Eva | public | 2013-02-12 11:18 | 2014-02-12 16:53 | ||||
Reporter | Jochen | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | tweak | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Oxygen-20120901 | ||||||||
Target Version | Fixed in Version | Frama-C Fluorine-20130401 | |||||||
Summary | 0001364: strange warning "extracting bits of a pointer" | ||||||||
Description | Running "frama-c -val ftest.c" on the attached program causes a "[kernel] warning: extracting bits of a pointer" for line 13, where neither any pointer nor any bit operation is present in the code. The warning vanishes if (1) the field "int a" in line 3 is removed from the struct _s, (2) the field "char *b" in line 4 is removed from the struct _s, or (3) the "extern" is removed from the declaration of "s" in line 10. Except for (2), no such action touches any pointer or bit operation. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Jochen (reporter) 2013-02-12 11:26 |
The warning also vanishes if (4) the formal argument type of foo() is changed to "struct _s *" in line 7, and accordingly the actual argument is changed to "&s" in line 13. |
yakobowski (manager) 2013-02-12 16:52 |
This is a benign warning due to the way passing struct arguments is handled. Although the analysis is done precisely, the contents of the struct are temporarily smashed together. Here, this concerns s.a and s.b; "fusing" their contents cause the warning. This will be fixed in the next version. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2013-02-12 11:18 | Jochen | New Issue | |
2013-02-12 11:18 | Jochen | File Added: ftest.c | |
2013-02-12 11:26 | Jochen | Note Added: 0003690 | |
2013-02-12 13:20 | yakobowski | Category | Kernel => Plug-in > value analysis |
2013-02-12 13:24 | pascal | Status | new => assigned |
2013-02-12 13:24 | pascal | Assigned To | => pascal |
2013-02-12 13:26 | yakobowski | Assigned To | pascal => yakobowski |
2013-02-12 13:29 | yakobowski | Assigned To | yakobowski => pascal |
2013-02-12 16:52 | yakobowski | Note Added: 0003691 | |
2013-02-12 16:52 | yakobowski | Assigned To | pascal => yakobowski |
2013-02-12 18:28 | svn | ||
2013-02-12 18:40 | yakobowski | Status | assigned => resolved |
2013-02-12 18:40 | yakobowski | Resolution | open => fixed |
2013-04-19 11:05 | signoles | Fixed in Version | => Frama-C Fluorine |
2013-04-19 11:05 | signoles | Status | resolved => closed |
2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master 80491a79 |
2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon 80491a79 |
2018-01-12 14:26 | signoles | Category | Plug-in > value analysis => Plug-in > Eva |