diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-20 17:26:10 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-20 17:26:10 +0200 |
commit | 6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4 (patch) | |
tree | 82f15798a28e557538b061bb90e37644b51261e5 /main.ml | |
parent | dd7b7d30adddfa0258aa5b3819a0a58d6b5d8705 (diff) | |
download | scade-analyzer-6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4.tar.gz scade-analyzer-6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4.zip |
Not much. Still does not work very well.
Diffstat (limited to 'main.ml')
-rw-r--r-- | main.ml | 25 |
1 files changed, 18 insertions, 7 deletions
@@ -19,6 +19,8 @@ let ai_itv = ref false let ai_rel = ref false let ai_root = ref "test" let ai_widen_delay = ref 3 +let ai_no_time_scopes = ref "" +let ai_init_scopes = ref "" let ifile = ref "" let usage = "usage: analyzer [options] file.scade" @@ -26,16 +28,18 @@ let usage = "usage: analyzer [options] file.scade" let options = [ "--dump", Arg.Set dump, "Dump program source."; "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; - "--vtest", Arg.Set vtest, "Verbose testing."; - "--test", Arg.Set test, "Simple testing."; + "--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-root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test)."; - "--ai-wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3)."; + "--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."; + "--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 s0 = Interpret.init_state (Typing.root_prog prog "test" [] []) in if verbose then begin Format.printf "Init state:@."; Interpret.print_state Format.std_formatter s0; @@ -79,8 +83,15 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - if !ai_itv then AI_Itv.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); - if !ai_rel then AI_Rel.do_prog !ai_widen_delay (Typing.root_prog prog !ai_root); + if !ai_itv || !ai_rel then begin + let comma_split = Str.split (Str.regexp ",") in + let rp = Typing.root_prog prog !ai_root + (comma_split !ai_no_time_scopes) + (comma_split !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; + end; if !vtest then do_test_interpret prog true else if !test then do_test_interpret prog false; |