Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001142Frama-CPlug-in > Evapublic2012-04-04 11:192014-02-12 16:59
Reporterpherrmann 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001142: Bad AST generation ?
DescriptionSee program attached: it is accepted as correct (-check passes) but rejected later on (cf. value analysis crashes on it).

TagsNo tags attached.
Attached Filesc file icon e.c [^] (280 bytes) 2012-04-04 11:19 [Show Content]

- Relationships

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

- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker