DP locations defined by abstract values and not by formula.

1 files changed, 9 insertions, 0 deletions

diff --git a/main.ml b/main.ml
index 303723d..f85f6fb 100644
--- a/main.ml
+++ b/main.ml
@@ -47,6 +47,8 @@ let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
 let ai_init_scopes = ref "all"
 let ai_disj_v = ref ""
+let ai_max_dp_depth = ref 10
+let ai_max_dp_width = ref 100
 let ai_vci = ref false
 let ai_vvci = ref false
 let ifile = ref ""
@@ -91,6 +93,11 @@ let options = [
     "--ai-wd", Arg.Set_int ai_widen_delay,
         "Widening delay in abstract analysis of loops (default: 3).";
 
+    "--ai-max-dp-depth", Arg.Set_int ai_max_dp_depth,
+        "Maximum depth in the dynamic partitionning tree.";
+    "--ai-max-dp-width", Arg.Set_int ai_max_dp_width,
+        "Maximum number of dynamically partitionned locations.";
+
     "--root", Arg.Set_string ai_root,
         "Root node for abstract analysis (default: test).";
     "--no-time", Arg.Set_string ai_no_time_scopes,
@@ -178,6 +185,8 @@ let () =
               disjunct = disj;
               verbose_ci = !ai_vci;
               vverbose_ci = !ai_vvci;
+              max_dp_width = !ai_max_dp_width;
+              max_dp_depth = !ai_max_dp_depth;
           } in
           
           if !ai_itv then AI_Itv.do_prog opt rp;