Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Related Changesets ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001364Frama-CPlug-in > Evapublic2013-02-12 11:182014-02-12 16:53
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon ftest.c [^] (137 bytes) 2013-02-12 11:18 [Show Content]

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

- 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 Checkin
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
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker