diff options
Diffstat (limited to 'main.ml')
-rw-r--r-- | main.ml | 45 |
1 files changed, 34 insertions, 11 deletions
@@ -7,6 +7,7 @@ open Nonrelational open Apron_domain open Enum_domain_edd +open Abs_interp_dynpart module Interpret = Interpret.I @@ -18,6 +19,9 @@ module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND) module AI_Itv_EDD = Abs_interp_edd.I(ItvND) module AI_Rel_EDD = Abs_interp_edd.I(Apron_domain.ND) +module AI_S_Itv_DP = Abs_interp_dynpart.I + (Enum_domain.MultiValuation)(ItvND) + (* command line options *) let times = ref false let dump = ref false @@ -28,6 +32,7 @@ let ai_itv = ref false 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_root = ref "test" let ai_widen_delay = ref 5 let ai_no_time_scopes = ref "all" @@ -40,22 +45,35 @@ let ifile = ref "" let usage = "usage: analyzer [options] file.scade" let options = [ - "--exec-times", Arg.Set times, "Show time spent in each function of the analyzer, for some functions"; + "--exec-times", Arg.Set times, + "Show time spent in each function of the analyzer, for some functions"; "--dump", Arg.Set dump, "Dump program source."; "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; "--vtest", Arg.Set vtest, "Verbose testing (direct interpret)."; "--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-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain."; - "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)"; - "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)"; - "--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."; + "--ai-itv-edd", Arg.Set ai_itv_edd, + "Do abstract analysis using intervals and EDD disjunction domain."; + "--ai-rel-edd", Arg.Set ai_rel_edd, + "Do abstract analysis using Apron and EDD disjunction domain."; + "--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-vci", Arg.Set ai_vci, + "Verbose chaotic iterations (show state at each iteration)"; + "--ai-vvci", Arg.Set ai_vvci, + "Very verbose chaotic iterations (show everything all the time)"; + "--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 = @@ -106,7 +124,10 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv || !ai_rel || !ai_itv_edd || !ai_rel_edd then begin + if !ai_itv || !ai_rel + || !ai_itv_edd || !ai_rel_edd + || !ai_s_itv_dp then + begin let comma_split = Str.split (Str.regexp ",") in let select_f x = if x = "all" then @@ -138,6 +159,8 @@ let () = if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp; 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; end; if !vtest then do_test_interpret prog true |