Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.