2021-01-15 15:10 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001142Frama-CPlug-in > Evapublic2012-04-04 11:192014-02-12 16:59
Reporterpherrmann 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon e.c (280 bytes) 2012-04-04 11:19 - 
    struct P {
  int val[2][2];
};

int main() {
  struct P* pp;
  struct P p;
  pp = &p;
  *(pp->val);
}

/*
struct P {
   int val[2][2] ;
};
int main(void)
{
  int __retres;
  struct P *pp;
  struct P p;
  pp = & p;
  if (pp->val[0]) {  }
  __retres = 0;
  return (__retres);
}
*/
    c file icon e.c (280 bytes) 2012-04-04 11:19 +

-Relationships
+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

Last edited: 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.
+Notes

-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
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
2013-12-19 01:12 Source_changeset_attached => framac master 4af7d25a
2014-02-12 16:54 Source_changeset_attached => framac stable/neon 4af7d25a
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
+Issue History