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

Thank you very much for your reply, Anne!

So, as far as I understand, the problem of backward slicing essentially 
reduces to the (graph) problem of pruning in the PDG all but the paths 
through which the "slice criterion node" is reachable. Is this 
sufficient? Also, is the PDG able to capture the inter-procedural 
dependences?

Thanks again,

Nikos


Anne Pacalet wrote:
> 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...
>