strange warning "extracting bits of a pointer"
ID0001364: This issue was created automatically from Mantis Issue 1364. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001364 | Frama-C | Plug-in > Eva | public | 2013-02-12 | 2014-02-12 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Oxygen-20120901 | Target Version | - | Fixed in Version | Frama-C Fluorine-20130401 |
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.