Control dependencies between labelled instructuctions and the corresponding goto statement
ID0001992: This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001992 | Frama-C | Plug-in > pdg | public | 2014-11-25 | 2015-08-03 |
| Reporter | nguenaomer | Assigned To | maroneze | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | X68 | OS | Linux | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | - |
Description :
Issue1: Does the pdg of frama-c include the transitive closure of standard control and data dependency relation?
Issue2: I think that there is an error in the PDG (or only the dot version). The PDG of the function below states that the "while_0_break" statement control the "goto while_0_break" when using the -simplify-cfg option. To me, it should be the converse. The same with Neon.
Note that Issue1 and Issue2 are related.
Steps To Reproduce :
I executed the following commamds with the C code below $frama-c -pdg example2.c -main transfer_func -pdg-dot pdg2 -simplify-cfg $dot -Tpng -o pdg2.transfer_func.png pdg2.transfer_func.dot
int x1,x2 ; void transfer_func(int time) { int prod =1 ; int k =1 ; while (k<=10) { if (time/k > prod) break ; prod *= k; k++ ; } x1++; x2++; }
Enclosed is the pdg.
