0001142: Bad AST generation ? - Frama-C Bug Tracking System

Issue History
Date Modified	Username	Field	Change
2012-04-04 11:19	pherrmann	New Issue
2012-04-04 11:19	pherrmann	File Added: e.c
2012-04-04 14:32	signoles	Status	new => assigned
2012-04-04 14:32	signoles	Assigned To	=> virgile
2012-04-06 20:29	virgile	Assigned To	virgile => yakobowski
2012-04-06 20:32	virgile	Note Added: 0002847
2012-04-06 20:33	virgile	Category	Kernel => Plug-in > value analysis
2012-04-06 21:18	yakobowski	Note Added: 0002848
2012-04-06 21:19	yakobowski	Note Added: 0002849
2012-04-06 21:20	yakobowski	Status	assigned => feedback
2012-04-06 21:37	yakobowski	Note Edited: 0002849
2012-04-09 16:59	svn	Checkin
2012-04-09 16:59	svn	Status	feedback => resolved
2012-04-09 16:59	svn	Resolution	open => fixed
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed
2014-02-12 16:59		Note Added: 0004703
2014-02-12 16:59		Status	closed => resolved
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva

Notes
(0002847) virgile (developer) 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 (manager) 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 (manager) 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.

Relationships