From 5a4165f55002876033c718303f86e9e1b7417745 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 18 Jun 2014 17:53:11 +0200 Subject: Nice view of guarantees ; add half test, proved. --- main.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'main.ml') 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 -- cgit v1.2.3