Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Files? file icon pdg_pb.ml [^] (1,196 bytes) 2012-06-11 12:09 [Show Content]

- Relationships

-  Notes
(0003101)
Anne (reporter)
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 (manager)
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 (reporter)
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 (reporter)
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 (manager)
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 (reporter)
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 (manager)
2012-06-12 17:57

Fixed in revision 18807

- Issue History
Date Modified Username Field Change
2012-06-11 12:09 Anne New Issue
2012-06-11 12:09 Anne Status new => assigned
2012-06-11 12:09 Anne Assigned To => yakobowski
2012-06-11 12:09 Anne File Added: pdg_pb.ml
2012-06-11 12:23 Anne Note Added: 0003101
2012-06-12 11:10 yakobowski Note Added: 0003104
2012-06-12 11:15 Anne Note Added: 0003105
2012-06-12 14:26 Anne Note Added: 0003106
2012-06-12 15:19 yakobowski Note Added: 0003107
2012-06-12 15:51 Anne Note Added: 0003108
2012-06-12 17:57 yakobowski Note Added: 0003111
2012-06-12 17:57 yakobowski Status assigned => resolved
2012-06-12 17:57 yakobowski 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker