--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on September 2009 ---
Nikos Anastopoulos wrote : > I would like to have an in-depth look into the algorithm(s) that frama-c > uses for backward slicing. Could you provide some resources (e.g. > papers) regarding this? Sorry for this late answer, but there is no paper describing precisely how the slicing module works. To better understand some particular points, maybe you can have a look at the PDG (Program Dependence Graph) results. To see them, yo can for instance run : frama-c -fct-pdg f file.c It will show you a textual representation of the dependencies between function [f] statements of the file [file.c]. It you want to have a graphical representation, run : frama-c -fct-pdg f -dot-pdg xxx file.c that will generate xxx.f.dot which uses the dot language (see http://www.graphviz.org/). The PDG uses the value analysis results for handle the aliases, and the -deps option results to process the function calls. The slicing mostly uses these dependencies backward. I am sorry that I cannot provide a description of the algorithms, but if you have precise questions, I can try to answer... Hope this helps... -- Anne Pacalet.