Frama-C Bug Tracking System - Frama-C
View Issue Details
0001142Frama-CPlug-in > Evapublic2012-04-04 11:192014-02-12 16:59
pherrmann 
yakobowski 
normalminoralways
closedfixed 
 
Frama-C Oxygen-20120901 
0001142: Bad AST generation ?
See program attached: it is accepted as correct (-check passes) but rejected later on (cf. value analysis crashes on it).
No tags attached.
c e.c (280) 2012-04-04 11:19
https://bts.frama-c.com/file_download.php?file_id=365&type=bug
Issue History
2012-04-04 11:19pherrmannNew Issue
2012-04-04 11:19pherrmannFile Added: e.c
2012-04-04 14:32signolesStatusnew => assigned
2012-04-04 14:32signolesAssigned To => virgile
2012-04-06 20:29virgileAssigned Tovirgile => yakobowski
2012-04-06 20:32virgileNote Added: 0002847
2012-04-06 20:33virgileCategoryKernel => Plug-in > value analysis
2012-04-06 21:18yakobowskiNote Added: 0002848
2012-04-06 21:19yakobowskiNote Added: 0002849
2012-04-06 21:20yakobowskiStatusassigned => feedback
2012-04-06 21:37yakobowskiNote Edited: 0002849
2012-04-09 16:59svnCheckin
2012-04-09 16:59svnStatusfeedback => resolved
2012-04-09 16:59svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004703
2014-02-12 16:59Statusclosed => resolved
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002847)
virgile   
2012-04-06 20:32   
Actually, the kernel seems to do the right thing here, i.e. generating StartOf(Mem pp, Field(val, Index (0, NoOffset)), that indicates the address of the array pp->val[0].
(0002848)
yakobowski   
2012-04-06 21:18   
Hum, on this code struct P { int val[2][2]; }; struct P* pp; struct P p; void main() { *(p.val); } I do not get a StartOf, but a Lval.
(0002849)
yakobowski   
2012-04-06 21:19   
(edited on: 2012-04-06 21:37)
Notice that the code above is pretty-printed as void main(void) { if (p.val[0]) { } return; } which itself gets re-parsed as a StartOf.
(0004703)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.