diff options
| -rw-r--r-- | abstract/enum_domain.ml | 9 | ||||
| -rw-r--r-- | abstract/transform.ml | 1 | ||||
| -rw-r--r-- | frontend/typing.ml | 4 | ||||
| -rw-r--r-- | main.ml | 4 |
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 @@ -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) |