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



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;
> ;;
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130923/213fa5cb/attachment.html>