Add command line option : verbose chaotic iterations.

1 files changed, 11 insertions, 2 deletions

diff --git a/main.ml b/main.ml
index 1de08be..2e4eb49 100644
--- a/main.ml
+++ b/main.ml
@@ -3,6 +3,7 @@ open Ast
 open Num_domain
 open Nonrelational
 open Apron_domain
+open Abs_interp
 
 module Interpret = Interpret.I
 
@@ -23,6 +24,7 @@ let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
 let ai_init_scopes = ref ""
 let ai_disj_v = ref ""
+let ai_vci = ref false
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -34,6 +36,7 @@ let options = [
     "--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-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
     "--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.";
@@ -99,9 +102,15 @@ let () =
               (select_f !ai_init_scopes) in
 
           let disj = select_f !ai_disj_v in
+
+          let opt = {
+              widen_delay = !ai_widen_delay;
+              disjunct = disj;
+              verbose_ci = !ai_vci
+          } in
           
-          if !ai_itv then AI_Itv.do_prog !ai_widen_delay disj rp;
-          if !ai_rel then AI_Rel.do_prog !ai_widen_delay disj rp;
+          if !ai_itv then AI_Itv.do_prog opt rp;
+          if !ai_rel then AI_Rel.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true