strange warning "extracting bits of a pointer"
ID0001364: This issue was created automatically from Mantis Issue 1364. Further discussion may take place here.
|ID0001364||Frama-C||Plug-in > Eva||public||2013-02-12||2014-02-12|
|Product Version||Frama-C Oxygen-20120901||Target Version||-||Fixed in Version||Frama-C Fluorine-20130401|
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.