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

[Frama-c-discuss] About the slicing plugin. (slicing speed on slicing zones)



I am sorry for forgetting to report the results.
These two solutions are equivalent.
After rechecking my code, the low speed of slicing is caused by slicing too
many stmts.
I also find that slicing stmts is much more slower than slicing
locations.zone.

On 24 September 2013 14:06, BAUDIN Patrick <Patrick.Baudin at cea.fr> wrote:

>  These two solutions seems equivalent.
> Do you have a significant difference on the  execution time ?
>
> 23/09/2013 15:55, David Yang wrote :
>
>
>  Whether i should join those zones together before performing slicing
> request?
>
>   let slice_zones zones kf =
>      let prj = !Db.Slicing.Project.mk_project "zones slice" in
>     let mark = !Db.Slicing.Mark.make ~data:true ~addr:true ~ctrl:true in
>     let ref_sel_set = ref Db.Slicing.Select.empty_selects in
>     let rec join_zones zones =
>  if(List.length zones = 1) then List.hd zones
>  else Locations.Zone.join (List.hd zones) (join_zones (List.tl zones))
>  in
>  let azone = join_zones zones in
>  ref_sel_set := !Db.Slicing.select_func_zone !ref_sel_set mark azone;
>       !Db.Slicing.Request.add_selection prj !ref_sel_set;
>     !Db.Slicing.Request.apply_all prj ~propagate_to_callers:false;
>     !Db.Slicing.Slice.get_all prj kf;
> ;;
>
> I will try this method.
>
>  :-)
>
>
>  Best regards,
> David Yang
>    On 23 September 2013 09:10, David Yang <abiao.yang at gmail.com> wrote:
>
>> Dear all,
>> uh... The following code is my function for slicing a punch of zones.
>> let slice_zones zones kf =
>> let prj = !Db.Slicing.Project.mk_project "zones slice" in
>> let mark = !Db.Slicing.Mark.make ~data:true ~addr:true ~ctrl:true in
>> let ref_sel_set = ref Db.Slicing.Select.empty_selects in
>> List.iter
>> (fun z ->
>> ref_sel_set := !Db.Slicing.select_func_zone !ref_sel_set mark z
>> kf
>> ) zones;
>> !Db.Slicing.Request.add_selection prj !ref_sel_set;
>> !Db.Slicing.Request.apply_all prj ~propagate_to_callers:false;
>> !Db.Slicing.Slice.get_all prj kf;
>> ;;
>
>
>
>
> _______________________________________________
> Frama-c-discuss mailing listFrama-c-discuss at lists.gforge.inria.frhttp://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
> --
> Patrick Baudin, DILS/LSL, B?t. 862,
> Point Courrier n? 174
> Institut CARNOT CEA LIST,
> CEA Saclay Nano-INNOV,
> 91191 Gif-sur-Yvette cedex, France.
> tel: +33 (0)1 6908 2072
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130924/2cc33807/attachment.html>