Frama-C Bug Tracking System - Frama-C
View Issue Details
0001992Frama-CPlug-in > pdgpublic2014-11-25 16:362015-08-03 19:58
nguenaomer 
maroneze 
normalminoralways
assignedopen 
X68Linux
Frama-C Fluorine-20130601 
 
0001992: Control dependencies between labelled instructuctions and the corresponding goto statement
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.
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.
No tags attached.
png pdg2.transfer_func.png (370,217) 2014-11-25 16:36
https://bts.frama-c.com/file_download.php?file_id=901&type=bug
Issue History
2014-11-25 16:36nguenaomerNew Issue
2014-11-25 16:36nguenaomerStatusnew => assigned
2014-11-25 16:36nguenaomerAssigned To => yakobowski
2014-11-25 16:36nguenaomerFile Added: pdg2.transfer_func.png
2015-08-03 19:58yakobowskiAssigned Toyakobowski => maroneze

There are no notes attached to this issue.