From 7e1cf88f181aa0596361b5b5d784f8e4b9b19266 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 22 Jul 2014 09:04:13 +0200 Subject: Add support for octagons. --- main.ml | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) (limited to 'main.ml') diff --git a/main.ml b/main.ml index 55a3837..08ec36a 100644 --- a/main.ml +++ b/main.ml @@ -16,19 +16,21 @@ 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_Poly = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Poly) +module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND_Oct) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) -module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) +module AI_Poly_EDD = Abs_interp_edd.I(Apron_domain.ND_Poly) +module AI_Oct_EDD = Abs_interp_edd.I(Apron_domain.ND_Oct) module AI_S_Itv_DP = Abs_interp_dynpart.I (Enum_domain.MultiValuation)(ItvND) module AI_S_Rel_DP = Abs_interp_dynpart.I - (Enum_domain.MultiValuation)(Apron_domain.ND) + (Enum_domain.MultiValuation)(Apron_domain.ND_Poly) module AI_EDD_Itv_DP = Abs_interp_dynpart.I (Enum_domain_edd.EDD)(ItvND) module AI_EDD_Rel_DP = Abs_interp_dynpart.I - (Enum_domain_edd.EDD)(Apron_domain.ND) + (Enum_domain_edd.EDD)(Apron_domain.ND_Poly) (* command line options *) let times = ref false @@ -37,9 +39,11 @@ let dumprn = ref false let test = ref false let vtest = ref false let ai_itv = ref false -let ai_rel = ref false +let ai_poly = ref false +let ai_oct = ref false let ai_itv_edd = ref false -let ai_rel_edd = ref false +let ai_poly_edd = ref false +let ai_oct_edd = ref false let ai_s_itv_dp = ref false let ai_s_rel_dp = ref false let ai_edd_itv_dp = ref false @@ -68,12 +72,15 @@ let options = [ "--test", Arg.Set test, "Simple testing (direct interpret)."; "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals."; - "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron."; + "--ai-poly", Arg.Set ai_poly, "Do abstract analysis using Apron polyhedra domain."; + "--ai-oct", Arg.Set ai_oct, "Do abstract analysis using Apron octagon domain."; "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain."; - "--ai-rel-edd", Arg.Set ai_rel_edd, - "Do abstract analysis using Apron and EDD disjunction domain."; + "--ai-poly-edd", Arg.Set ai_poly_edd, + "Do abstract analysis using Apron polyhedra domain and EDD disjunction domain."; + "--ai-oct-edd", Arg.Set ai_oct_edd, + "Do abstract analysis using Apron octagon domain and EDD disjunction domain."; "--ai-s-itv-dp", Arg.Set ai_s_itv_dp, "Do abstract analysis using dynamic partitionning method, "^ @@ -172,8 +179,8 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv || !ai_rel - || !ai_itv_edd || !ai_rel_edd + if !ai_itv || !ai_poly || !ai_oct + || !ai_itv_edd || !ai_poly_edd || !ai_oct_edd || !ai_s_itv_dp || !ai_s_rel_dp || !ai_edd_itv_dp || !ai_edd_rel_dp then begin @@ -206,10 +213,12 @@ let () = } in if !ai_itv then AI_Itv.do_prog opt rp; - if !ai_rel then AI_Rel.do_prog opt rp; + if !ai_poly then AI_Poly.do_prog opt rp; + if !ai_oct then AI_Oct.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; + if !ai_poly_edd then AI_Poly_EDD.do_prog opt rp; + if !ai_oct_edd then AI_Oct_EDD.do_prog opt rp; if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp; if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp; -- cgit v1.2.3