summaryrefslogtreecommitdiff
path: root/main.ml
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-18 18:21:18 +0200
commit4d59f3a805d0cca882caab353ac8ec0dd4c04f73 (patch)
treeada69c3799c7fbb0d0cb6100bff2f4c649907edb /main.ml
parent9714afeb275360110161c870b50627128fda75a0 (diff)
downloadSemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.tar.gz
SemVerif-Projet-4d59f3a805d0cca882caab353ac8ec0dd4c04f73.zip
Begin work on interface with Apron
Diffstat (limited to 'main.ml')
-rw-r--r--main.ml10
1 files changed, 7 insertions, 3 deletions
diff --git a/main.ml b/main.ml
index 8f33d2d..937180e 100644
--- a/main.ml
+++ b/main.ml
@@ -19,15 +19,19 @@ module Interp_const = Interpret.Make(Env_dom_const)
module Env_dom_interv = Nonrelational.NonRelational(Intervals_domain.Intervals)
module Interp_interv = Interpret.Make(Env_dom_interv)
+module Interp_rel = Interpret.Make(Relational_apron.RelationalDomain)
+
(* option parsing *)
let dump = ref false
let const_interp = ref false
let interv_interp = ref false
-let poly_interp = ref false
+let rel_interp = ref false
let get_interp () =
if !interv_interp
then Interp_interv.interpret
- else Interp_const.interpret
+ else if !rel_interp
+ then Interp_rel.interpret
+ else Interp_const.interpret
let ifile = ref ""
let set_var v s = v := s
@@ -38,7 +42,7 @@ let options = [
"--dump", Arg.Set dump, "Dump program source.";
"--const-interp", Arg.Set const_interp, "Use constant lattice interpreter.";
"--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter.";
- "--poly-interp", Arg.Set poly_interp, "Use polyhedra lattice interpreter.";
+ "--rel-interp", Arg.Set rel_interp, "Use relationnal (Apron) lattice.";
]
(* parse and print filename *)