View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001194 | Frama-C | Plug-in > scope | public | 2012-06-11 12:09 | 2012-09-19 17:16 | ||||
Reporter | Anne | ||||||||
Assigned To | yakobowski | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Nitrogen-20111001 | ||||||||
Target Version | Fixed in Version | Frama-C Oxygen-20120901 | |||||||
Summary | 0001194: imprecision in PDG when unreachable statements | ||||||||
Description | The 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 Information | Can 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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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. |
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? |
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). |
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. |
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. |
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.. |
yakobowski (manager) 2012-06-12 17:57 |
Fixed in revision 18807 |
![]() |
|||
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 |