diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-09 18:06:43 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-09 18:06:43 +0200 |
| commit | e06a4102e5b2a81c7b1c24323cafc863eefbc0cb (patch) | |
| tree | b151ddc7ee1e37c161889f1342aead47e5b9c44a /main.ml | |
| parent | bc9ad2280839677bb46acfd846ff05bb37719b6e (diff) | |
| download | scade-analyzer-e06a4102e5b2a81c7b1c24323cafc863eefbc0cb.tar.gz scade-analyzer-e06a4102e5b2a81c7b1c24323cafc863eefbc0cb.zip | |
Now it's starting to work...
Diffstat (limited to 'main.ml')
| -rw-r--r-- | main.ml | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -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 |