Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001194Frama-CPlug-in > scopepublic2012-06-11 12:092012-09-19 17:16
ReporterAnne 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001194: imprecision in PDG when unreachable statements
DescriptionThe PDG computation propagates a state that roughly maps zones to PDG nodes. It uses a Lmap_bitwise.Location_map_bitwise. After an unreachable statement, the state is said to be "empty" instead of "bottom", which leads to some imprecision when merging with another state because instead of having:
{ x --> XXX } U bottom = { x --> XXX }
we get :
{ x --> XXX } U { } = { x --> XXX or SELF }

Please, ask if you need more information to fix it.
Additional InformationCan see the problem with the enclosed script :
and pdg_pb.c :

int main (void) {
  int x = 0;
  char * name = get_name ();
  if (x > 0) {
    x ++;
  }
  f (name);
  return x;
}


$ frama-c pdg_pb.c -load-script pdg_pb.ml
TagsNo tags attached.
Relationships
Attached Files? pdg_pb.ml (1,196) 2012-06-11 12:09
https://bts.frama-c.com/file_download.php?file_id=394&type=bug

Notes
(0003101)
Anne   
2012-06-11 12:23   
I thing that the easiest fix would be to have a option type in PdgTypes.t_data_state to be able to encode bottom as None and to adapt Pdg_state accordingly.
(0003104)
yakobowski   
2012-06-12 11:10   
Nicely spotted, thanks.

Do you have an example where one of the plugins derived from the PDG (slicing or scope?) are less precise than they should because of this?
(0003105)
Anne   
2012-06-12 11:15   
I don't have any at the moment since I have seen this in my development, but I can build one as soon as I have a moment (this afternoon I think).
(0003106)
Anne   
2012-06-12 14:26   
Here is an example :
$ frama-c -slice-assert f ex.c -slice-print
int Y;
void f (void) {
  int x = 0;
  Y = input ();
  if (x > 0) {
    Y ++;
  }
  //@ assert Y > 0;
}
void main (void) {
  Y = 3;
  f ();
  return 0;
}
The statement Y=3 in 'main' is kept and it shouldn't.
(Notice that if you remove the dead code in 'f', it isn't).
If you need more explanation, please ask.
(0003107)
yakobowski   
2012-06-12 15:19   
Thanks. There were no differences after adding dummy affectations to 'name' before the call to 'get_name', and I wasn't sure there was a real impact. Moreover, Scope/Defs seems to be happy, although I'm not completely sure why.

I believe I have a fix directly inside Lmap_bitwise. This would be more general then a change to pdg_state, and would also improve the precision of some From computations. Thus, this is likely to get fixed for Oxygen.
(0003108)
Anne   
2012-06-12 15:51   
I don't think that the problem comes from Lmap_bitwise !
{ x --> XXX } U { } = { x --> XXX or SELF }
is correct since x is mapped to XXX in one branch and to nothing in the other.
Exemple :
void f (void) {
  if (c) x = 2;
  y = x;
}
You are really interested by 'x' value before calls to 'f'.


The bug is really in PDG because it uses 'empty' instead of 'bottom' for unreachable statements..
(0003111)
yakobowski   
2012-06-12 17:57   
Fixed in revision 18807

Issue History
Date ModifiedUsernameFieldChange
2012-06-11 12:09AnneNew Issue
2012-06-11 12:09AnneStatusnew => assigned
2012-06-11 12:09AnneAssigned To => yakobowski
2012-06-11 12:09AnneFile Added: pdg_pb.ml
2012-06-11 12:23AnneNote Added: 0003101
2012-06-12 11:10yakobowskiNote Added: 0003104
2012-06-12 11:15AnneNote Added: 0003105
2012-06-12 14:26AnneNote Added: 0003106
2012-06-12 15:19yakobowskiNote Added: 0003107
2012-06-12 15:51AnneNote Added: 0003108
2012-06-12 17:57yakobowskiNote Added: 0003111
2012-06-12 17:57yakobowskiStatusassigned => resolved
2012-06-12 17:57yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed