summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
Diffstat (limited to 'abstract')
-rw-r--r--abstract/enum_domain.ml9
-rw-r--r--abstract/transform.ml1
2 files changed, 10 insertions, 0 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)
+