More verbosity ; adapt rfollow so that it can be proved

1 files changed, 4 insertions, 1 deletions

diff --git a/main.ml b/main.ml
index f38a484..5e9f087 100644
--- a/main.ml
+++ b/main.ml
@@ -31,6 +31,7 @@ let ai_no_time_scopes = ref ""
 let ai_init_scopes = ref ""
 let ai_disj_v = ref ""
 let ai_vci = ref false
+let ai_vvci = ref false
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -46,6 +47,7 @@ let options = [
     "--ai-itv-edd", Arg.Set ai_itv_edd, "Do abstract analysis using intervals and EDD disjunction domain.";
     "--ai-rel-edd", Arg.Set ai_rel_edd, "Do abstract analysis using Apron and EDD disjunction domain.";
     "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
+    "--ai-vvci", Arg.Set ai_vvci, "Very verbose chaotic iterations (show everything all the time)";
     "--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.";
@@ -117,7 +119,8 @@ let () =
           let opt = {
               widen_delay = !ai_widen_delay;
               disjunct = disj;
-              verbose_ci = !ai_vci
+              verbose_ci = !ai_vci;
+              vverbose_ci = !ai_vvci;
           } in
           
           if !ai_itv then AI_Itv.do_prog opt rp;