Add support for octagons.

1 files changed, 22 insertions, 13 deletions

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;