summaryrefslogtreecommitdiff
path: root/main.ml
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 17:53:11 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 17:53:11 +0200
commit5a4165f55002876033c718303f86e9e1b7417745 (patch)
treeaa17967d9b952b3df9a6b6fce215997ea2c9f7e5 /main.ml
parent96753a375e814be6bde6c41cfdfa4b4cc06bd28e (diff)
downloadscade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.tar.gz
scade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.zip
Nice view of guarantees ; add half test, proved.
Diffstat (limited to 'main.ml')
-rw-r--r--main.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/main.ml b/main.ml
index 0ddf91c..e98dd5f 100644
--- a/main.ml
+++ b/main.ml
@@ -2,8 +2,8 @@ open Ast
module Interpret = Interpret.I
-module IntD = Nonrelational.D(Intervals_domain.VD)
-module AI_Int = Abs_interp.I(IntD)
+module ItvD = Nonrelational.D(Intervals_domain.VD)
+module AI_Itv = Abs_interp.I(ItvD)
module AI_Rel = Abs_interp.I(Apron_domain.D)
(* command line options *)
@@ -11,7 +11,7 @@ let dump = ref false
let dumprn = ref false
let test = ref false
let vtest = ref false
-let ai_int = ref false
+let ai_itv = ref false
let ai_rel = ref false
let ai_root = ref "test"
let ai_widen_delay = ref 3
@@ -24,7 +24,7 @@ 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-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).";
@@ -75,7 +75,7 @@ let () =
let prog = Rename.rename_prog prog in
if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
- if !ai_int then AI_Int.do_prog !ai_widen_delay prog !ai_root;
+ if !ai_itv then AI_Itv.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