2020-12-05 00:13 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001364Frama-CPlug-in > Evapublic2013-02-12 11:182014-02-12 16:53
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001364: strange warning "extracting bits of a pointer"
DescriptionRunning "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.
TagsNo tags attached.
Attached Files
  • c file icon ftest.c (137 bytes) 2013-02-12 11:18 - 
    struct _s {
	int   a;
        char *b;
};

void foo(struct _s s) {
}

extern struct _s s;

void main(void) {
	foo(s);
}
    c file icon ftest.c (137 bytes) 2013-02-12 11:18 +

-Relationships
+Relationships

-Notes

~0003690

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.

~0003691

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.
+Notes

-Issue History
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
+Issue History