Minor corrections.

- Use correect clock scope in typing
- De-activate multi-valuated domain for enumerate vars + var couples.
- Add comment explaining why it doesn't work

4 files changed, 14 insertions, 4 deletions

diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 2353049..d216276 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -268,6 +268,15 @@ end
     Complicated domain : a set of values for each variables, plus some
     constraints on couples of variables
       (eg. (x, y) in [ tt, tt ; ff, ff ]
+
+    WARNING : This domain is not proved to be safe. In particular, it may represent
+    a set of contraints that imply Bot (ie that are impossible) without raising the
+    Bot exception. (there is potentially exponential cost in the checking that all
+    the constraints are coherent, and I have no idea of an algorithm for doing that
+    check.)
+
+    Therefore, do not use this domain unless you know what you are doing (which is
+    probably not the case anyway).
 *)
 
 module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct
diff --git a/abstract/transform.ml b/abstract/transform.ml
index 4a13e18..d9b20d8 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -475,3 +475,4 @@ and guarantees_of_prog rp =
     } in
 
     g_of_scope td rp.root_scope "" (BConst true)
+
diff --git a/frontend/typing.ml b/frontend/typing.ml
index 167caea..9fe2c8f 100644
--- a/frontend/typing.ml
+++ b/frontend/typing.ml
@@ -121,14 +121,14 @@ let node_vars p f nid =
 *)
 let clock_vars rp (node, prefix, _) =
     let v =
-      if not (rp.no_time_scope (node^"/"))
+      if not (rp.no_time_scope (node^"/"^prefix))
       then
         [
           false, node^"/"^prefix^"time", TInt;
           false, "N"^node^"/"^prefix^"time", TInt]
       else [] in
     let v =
-      if rp.init_scope (node^"/")
+      if rp.init_scope (node^"/"^prefix)
         then
           (false, node^"/"^prefix^"init", bool_type)::
           (false, "N"^node^"/"^prefix^"init", bool_type)::v
diff --git a/main.ml b/main.ml
index 5956b9e..d526a76 100644
--- a/main.ml
+++ b/main.ml
@@ -9,8 +9,8 @@ module Interpret = Interpret.I
 
 module ItvND = Nonrelational.ND(Intervals_domain.VD)
 
-module AI_Itv = Abs_interp.I(Enum_domain.MultiValuationCCons)(ItvND)
-module AI_Rel = Abs_interp.I(Enum_domain.MultiValuationCCons)(Apron_domain.ND)
+module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
+module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
 
 (*
 module AI_Itv_EDD = Abs_interp_edd.I(ItvND)