Implementation of disjunction domain seems to work.

1 files changed, 21 insertions, 10 deletions

diff --git a/main.ml b/main.ml
index 3cef6bd..1de08be 100644
--- a/main.ml
+++ b/main.ml
@@ -1,14 +1,15 @@
 open Ast
 
+open Num_domain
+open Nonrelational
+open Apron_domain
+
 module Interpret = Interpret.I
 
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
-module ItvD = Abs_domain.D(ItvND)
-
-module ApronD = Abs_domain.D(Apron_domain.ND)
 
-module AI_Itv = Abs_interp.I(ItvD)
-module AI_Rel = Abs_interp.I(ApronD)
+module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND)
+module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND)
 
 (* command line options *)
 let dump = ref false
@@ -21,6 +22,7 @@ let ai_root = ref "test"
 let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
 let ai_init_scopes = ref ""
+let ai_disj_v = ref ""
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -35,11 +37,13 @@ let options = [
     "--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 =
-    let s0 = Interpret.init_state (Typing.root_prog prog "test" [] []) in
+    let f0 _ = false in
+    let s0 = Interpret.init_state (Typing.root_prog prog "test" f0 f0) in
     if verbose then begin
       Format.printf "Init state:@.";
       Interpret.print_state Format.std_formatter s0;
@@ -85,12 +89,19 @@ let () =
 
       if !ai_itv || !ai_rel then begin
           let comma_split = Str.split (Str.regexp ",") in
+          let select_f x =
+              if x = "all"
+                then (fun _ -> true)
+                else (fun i -> List.mem i (comma_split x))
+          in
           let rp = Typing.root_prog prog !ai_root
-              (comma_split !ai_no_time_scopes)
-              (comma_split !ai_init_scopes) in
+              (select_f !ai_no_time_scopes)
+              (select_f !ai_init_scopes) in
 
-          if !ai_itv then AI_Itv.do_prog !ai_widen_delay rp;
-          if !ai_rel then AI_Rel.do_prog !ai_widen_delay rp;
+          let disj = select_f !ai_disj_v in
+          
+          if !ai_itv then AI_Itv.do_prog !ai_widen_delay disj rp;
+          if !ai_rel then AI_Rel.do_prog !ai_widen_delay disj rp;
       end;
 
       if !vtest then do_test_interpret prog true