From 6dec5b2fae34f4be8e57745e3b1a7063a62e1fc4 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Fri, 20 Jun 2014 17:26:10 +0200
Subject: Not much. Still does not work very well.

---
 main.ml | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

(limited to 'main.ml')

diff --git a/main.ml b/main.ml
index 72c43b0..3cef6bd 100644
--- a/main.ml
+++ b/main.ml
@@ -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;
-- 
cgit v1.2.3