--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on September 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Slicing in Frama-C



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.