From 43487d3baf695875482454ade1bdbc1403bfaaf6 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 18 Jun 2014 15:31:03 +0200 Subject: Add gilbreath suite ; booleans are not represented in a good way. --- main.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'main.ml') diff --git a/main.ml b/main.ml index aa60c57..0ddf91c 100644 --- a/main.ml +++ b/main.ml @@ -3,13 +3,18 @@ open Ast module Interpret = Interpret.I module IntD = Nonrelational.D(Intervals_domain.VD) -module AI = Abs_interp.I(Apron_domain.D) +module AI_Int = Abs_interp.I(IntD) +module AI_Rel = Abs_interp.I(Apron_domain.D) (* command line options *) let dump = ref false let dumprn = ref false let test = ref false let vtest = ref false +let ai_int = ref false +let ai_rel = ref false +let ai_root = ref "test" +let ai_widen_delay = ref 3 let ifile = ref "" let usage = "usage: analyzer [options] file.scade" @@ -19,6 +24,10 @@ let options = [ "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming."; "--vtest", Arg.Set vtest, "Verbose testing."; "--test", Arg.Set test, "Simple testing."; + "--ai-int", Arg.Set ai_int, "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)."; ] let do_test_interpret prog verbose = @@ -66,7 +75,8 @@ let () = let prog = Rename.rename_prog prog in if !dumprn then Ast_printer.print_prog Format.std_formatter prog; - let () = AI.do_prog prog "test" in + if !ai_int then AI_Int.do_prog !ai_widen_delay prog !ai_root; + if !ai_rel then AI_Rel.do_prog !ai_widen_delay prog !ai_root; if !vtest then do_test_interpret prog true else if !test then do_test_interpret prog false; -- cgit v1.2.3