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] About the slicing plugin. (slicing speed on slicing zones)

Le 23/09/2013 04:31, David Yang a ?crit :
> Dear all,
>
> What is the slicing algorithm for slicing zones in frama-c?
>
> Currently, I am using frama-c to perform program slicing. I am not 
> very sure about the slicing algorithm for slicing zones in frama-c.
>
> Firstly, I select zones (Locations.Zone.t) related to a function by 
> using : Db.Slicing.select_func_zone
> Then, I apply the slicing request by using: 
> !Db.Slicing.Request.apply_all prj ~propagate_to_callers:false;
  Setting propagate_to_callers to false gives partial results.

> But this is very slow, even the function is less than 20 source lines 
> of code.
The slicing relies on the results of the value analysis plugins and the 
PDG plugins.
These analysis can also take some time to be performed since they are 
done on the whole program.
>
> I guess the slicing plugin perform a slicing task in the following :
> 1. Apply slicing request for each zone respectively
> 2. Combine those slices related to each zone.
>
> Am I right?
>
> In addition,  any suggestion on how to improve speed for this kind of 
> slicing task?
Could you identify which part of the analysis is slow using some debug 
level ?

Patrick.
-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? nettoy?e...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130923/98dccfe3/attachment.html>