Begin dynamic partitionning ; CORRECT BUG IN unpass_cycle !!

1 files changed, 34 insertions, 11 deletions

diff --git a/main.ml b/main.ml
index e114554..339a433 100644
--- a/main.ml
+++ b/main.ml
@@ -7,6 +7,7 @@ open Nonrelational
 open Apron_domain
 
 open Enum_domain_edd
+open Abs_interp_dynpart
 
 module Interpret = Interpret.I
 
@@ -18,6 +19,9 @@ 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)
 
+module AI_S_Itv_DP = Abs_interp_dynpart.I
+      (Enum_domain.MultiValuation)(ItvND)
+
 (* command line options *)
 let times = ref false
 let dump = ref false
@@ -28,6 +32,7 @@ let ai_itv = ref false
 let ai_rel = ref false
 let ai_itv_edd = ref false
 let ai_rel_edd = ref false
+let ai_s_itv_dp = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
@@ -40,22 +45,35 @@ let ifile = ref ""
 let usage = "usage: analyzer [options] file.scade"
 
 let options = [
-    "--exec-times", Arg.Set times, "Show time spent in each function of the analyzer, for some functions";
+    "--exec-times", Arg.Set times,
+        "Show time spent in each function of the analyzer, for some functions";
     "--dump", Arg.Set dump, "Dump program source.";
     "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
     "--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
     "--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-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-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
-    "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)";
-    "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
-    "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
-    "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis.";
-    "--disj", Arg.Set_string ai_disj_v, "Variables for which to introduce a disjunction.";
-    "--init", Arg.Set_string ai_init_scopes, "Scopes for which to introduce a 'init' variable in analysis.";
+    "--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-s-itv-dp", Arg.Set ai_s_itv_dp,
+        "Do abstract analysis using dynamic partitionning method, "^
+        "with intervals and valuation domain for enums.";
+    "--ai-vci", Arg.Set ai_vci,
+        "Verbose chaotic iterations (show state at each iteration)";
+    "--ai-vvci", Arg.Set ai_vvci,
+        "Very verbose chaotic iterations (show everything all the time)";
+    "--wd", Arg.Set_int ai_widen_delay,
+        "Widening delay in abstract analysis of loops (default: 3).";
+    "--root", Arg.Set_string ai_root,
+        "Root node for abstract analysis (default: test).";
+    "--no-time", Arg.Set_string ai_no_time_scopes,
+        "Scopes for which not to introduce a 'time' variable in analysis.";
+    "--disj", Arg.Set_string ai_disj_v,
+        "Variables for which to introduce a disjunction.";
+    "--init", Arg.Set_string ai_init_scopes,
+        "Scopes for which to introduce a 'init' variable in analysis.";
 ]
 
 let do_test_interpret prog verbose =
@@ -106,7 +124,10 @@ 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 then begin
+      if !ai_itv || !ai_rel
+          || !ai_itv_edd || !ai_rel_edd
+          || !ai_s_itv_dp then
+      begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
               if x = "all" then
@@ -138,6 +159,8 @@ let () =
           
           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_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true