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 a ?crit :
> Thank you very much for your reply, Anne!

You are welcome !

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

Yes, it is mostly that, so the smart part is mainly le PDG
(greatly helped by the value analysis) .

> Is this 
> sufficient? Also, is the PDG able to capture the inter-procedural 
> dependences?

The PDG uses the results of the -deps option to manage function calls.
For inter-procedural slicing, there are some more processing
in the slicing module since we try to specialize the called functions
(in some mode : see -slicing-level in ./frama-c -slicing-help).

Are you interested by the slicing from a user point of view ?
or maybe to use it in another plugin ?

Anyway, hope I answered you questions.
Anne Pacalet.