diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-25 16:55:43 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-25 16:55:43 +0200 |
| commit | e16f965b88efa1ba7872ced9fed627361c5c2c9e (patch) | |
| tree | 2beafe42b393b2d02ee94cb393ff736b4db33935 /main.ml | |
| parent | 255ec4a98d329d021dbc86ca81a59d562efaa8d1 (diff) | |
| download | scade-analyzer-e16f965b88efa1ba7872ced9fed627361c5c2c9e.tar.gz scade-analyzer-e16f965b88efa1ba7872ced9fed627361c5c2c9e.zip | |
Begin implementation of EDD ; SCA implemented.
Diffstat (limited to 'main.ml')
| -rw-r--r-- | main.ml | 9 |
1 files changed, 8 insertions, 1 deletions
@@ -12,6 +12,8 @@ module ItvND = Nonrelational.ND(Intervals_domain.VD) module AI_Itv = Abs_interp.I(Enum_domain.Valuation)(ItvND) module AI_Rel = Abs_interp.I(Enum_domain.Valuation)(Apron_domain.ND) +module AI_Itv_EDD = Abs_interp_edd.I(ItvND) + (* command line options *) let dump = ref false let dumprn = ref false @@ -19,6 +21,7 @@ let test = ref false let vtest = ref false let ai_itv = ref false let ai_rel = ref false +let ai_itv_edd = ref false let ai_root = ref "test" let ai_widen_delay = ref 3 let ai_no_time_scopes = ref "" @@ -36,6 +39,7 @@ let options = [ "--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-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)"; "--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)."; @@ -78,6 +82,8 @@ let do_test_interpret prog verbose = let () = Arg.parse options (fun f -> ifile := f) usage; + AI_Itv_EDD.test (); + if !ifile = "" then begin Format.eprintf "No input file...@."; exit 1 @@ -90,7 +96,7 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv || !ai_rel then begin + if !ai_itv || !ai_rel || !ai_itv_edd then begin let comma_split = Str.split (Str.regexp ",") in let select_f x = if x = "all" @@ -111,6 +117,7 @@ let () = if !ai_itv then AI_Itv.do_prog opt rp; if !ai_rel then AI_Rel.do_prog opt rp; + if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; end; if !vtest then do_test_interpret prog true |