Frama-C Bug Tracking System - Frama-C
View Issue Details
0001364Frama-CPlug-in > Evapublic2013-02-12 11:182014-02-12 16:53
Jochen 
yakobowski 
normaltweakalways
closedfixed 
Frama-C Oxygen-20120901 
Frama-C Fluorine-20130401 
0001364: strange warning "extracting bits of a pointer"
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.
No tags attached.
c ftest.c (137) 2013-02-12 11:18
https://bts.frama-c.com/file_download.php?file_id=468&type=bug
Issue History
2013-02-12 11:18JochenNew Issue
2013-02-12 11:18JochenFile Added: ftest.c
2013-02-12 11:26JochenNote Added: 0003690
2013-02-12 13:20yakobowskiCategoryKernel => Plug-in > value analysis
2013-02-12 13:24pascalStatusnew => assigned
2013-02-12 13:24pascalAssigned To => pascal
2013-02-12 13:26yakobowskiAssigned Topascal => yakobowski
2013-02-12 13:29yakobowskiAssigned Toyakobowski => pascal
2013-02-12 16:52yakobowskiNote Added: 0003691
2013-02-12 16:52yakobowskiAssigned Topascal => yakobowski
2013-02-12 18:28svnCheckin
2013-02-12 18:40yakobowskiStatusassigned => resolved
2013-02-12 18:40yakobowskiResolutionopen => fixed
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0003690)
Jochen   
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.
(0003691)
yakobowski   
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.