imprecision in PDG when unreachable statements
ID0001194: This issue was created automatically from Mantis Issue 1194. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001194 | Frama-C | Plug-in > scope | public | 2012-06-11 | 2012-09-19 |
| Reporter | Anne | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
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