From 2cbaba6f00d40d5c6c9659678d0156f14b7e3780 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 11:10:13 +0200 Subject: Use LAST instead of NEXT (only EDD implementation works at the moment) --- main.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'main.ml') diff --git a/main.ml b/main.ml index 5e9f087..a02820c 100644 --- a/main.ml +++ b/main.ml @@ -1,16 +1,19 @@ +open Cmdline + open Ast open Num_domain open Nonrelational open Apron_domain -open Abs_interp module Interpret = Interpret.I module ItvND = Nonrelational.ND(Intervals_domain.VD) +(* module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND) module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND) +*) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) @@ -123,8 +126,10 @@ let () = vverbose_ci = !ai_vvci; } in + (* if !ai_itv then AI_Itv.do_prog opt rp; if !ai_rel then AI_Rel.do_prog opt rp; + *) if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp; -- cgit v1.2.3 From b1cdf90995c8f70e4a450b3319a136f0d50515d0 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 16:21:45 +0200 Subject: New example ; minor fixes. --- main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'main.ml') diff --git a/main.ml b/main.ml index a02820c..6cb2c50 100644 --- a/main.ml +++ b/main.ml @@ -29,7 +29,7 @@ let ai_rel = ref false let ai_itv_edd = ref false let ai_rel_edd = ref false let ai_root = ref "test" -let ai_widen_delay = ref 3 +let ai_widen_delay = ref 5 let ai_no_time_scopes = ref "" let ai_init_scopes = ref "" let ai_disj_v = ref "" -- cgit v1.2.3 From 108f38029404e8eb4b37c8892345917edfb3cac7 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 17:20:51 +0200 Subject: Adapt domain with non-EDD disjunctions ; it doesn't work very well ! --- main.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'main.ml') diff --git a/main.ml b/main.ml index 6cb2c50..2995e24 100644 --- a/main.ml +++ b/main.ml @@ -10,10 +10,8 @@ module Interpret = Interpret.I module ItvND = Nonrelational.ND(Intervals_domain.VD) -(* module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND) module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND) -*) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) @@ -109,9 +107,16 @@ let () = if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin let comma_split = Str.split (Str.regexp ",") in let select_f x = - if x = "all" - then (fun _ -> true) - else (fun i -> List.mem i (comma_split x)) + if x = "all" then + (fun _ -> true) + else if x = "last" then + (fun i -> i.[0] = 'L') + else if String.length x > 5 && String.sub x 0 5 = "last+" then + let psl = comma_split + (String.sub x 5 (String.length x - 5)) in + (fun i -> i.[0] = 'L' || List.mem i psl) + else + (fun i -> List.mem i (comma_split x)) in let rp = Typing.root_prog prog !ai_root (select_f !ai_no_time_scopes) @@ -126,10 +131,8 @@ let () = vverbose_ci = !ai_vvci; } in - (* if !ai_itv then AI_Itv.do_prog opt rp; if !ai_rel then AI_Rel.do_prog opt rp; - *) if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; if !ai_rel_edd then AI_Rel_EDD.do_prog opt rp; -- cgit v1.2.3