summaryrefslogtreecommitdiff
path: root/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'main.ml')
-rw-r--r--main.ml9
1 files changed, 8 insertions, 1 deletions
diff --git a/main.ml b/main.ml
index 339a433..96fb95e 100644
--- a/main.ml
+++ b/main.ml
@@ -21,6 +21,8 @@ module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND)
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)
(* command line options *)
let times = ref false
@@ -33,6 +35,7 @@ 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_s_rel_dp = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 5
let ai_no_time_scopes = ref "all"
@@ -60,6 +63,9 @@ let options = [
"--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-s-rel-dp", Arg.Set ai_s_rel_dp,
+ "Do abstract analysis using dynamic partitionning method, "^
+ "with Apron 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,
@@ -126,7 +132,7 @@ let () =
if !ai_itv || !ai_rel
|| !ai_itv_edd || !ai_rel_edd
- || !ai_s_itv_dp then
+ || !ai_s_itv_dp || !ai_s_rel_dp then
begin
let comma_split = Str.split (Str.regexp ",") in
let select_f x =
@@ -161,6 +167,7 @@ let () =
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;
+ if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
end;
if !vtest then do_test_interpret prog true