--- layout: fc_discuss_archives title: Message 124 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)



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 
> <mailto: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 list
> Frama-c-discuss at lists.gforge.inria.fr
> http://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

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