Add gilbreath suite ; booleans are not represented in a good way.

1 files changed, 12 insertions, 2 deletions

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;