Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001992Frama-CPlug-in > pdgpublic2014-11-25 16:362015-08-03 19:58
Reporternguenaomer 
Assigned Tomaroneze 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformX68OSLinuxOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in Version 
Summary0001992: Control dependencies between labelled instructuctions and the corresponding goto statement
DescriptionIssue1: 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 ReproduceI 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.
TagsNo tags attached.
Attached Filespng file icon pdg2.transfer_func.png [^] (370,217 bytes) 2014-11-25 16:36

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2014-11-25 16:36 nguenaomer New Issue
2014-11-25 16:36 nguenaomer Status new => assigned
2014-11-25 16:36 nguenaomer Assigned To => yakobowski
2014-11-25 16:36 nguenaomer File Added: pdg2.transfer_func.png
2015-08-03 19:58 yakobowski Assigned To yakobowski => maroneze


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker