diff options
Diffstat (limited to 'abstract/enum_domain.ml')
| -rw-r--r-- | abstract/enum_domain.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml index 68b04f5..b035cc0 100644 --- a/abstract/enum_domain.ml +++ b/abstract/enum_domain.ml @@ -26,6 +26,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig val bottom : (id * item list) list -> t val vtop : t -> t (* top with same vars *) val is_bot : t -> bool + val is_top : t -> bool (* variable management *) val vars : t -> (id * item list) list @@ -67,6 +68,7 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct let vtop x = { x with value = VarMap.empty } let bottom vars = raise Bot (* we don't represent Bot *) let is_bot x = false + let is_top x = VarMap.is_empty x.value let vars x = x.vars @@ -197,6 +199,11 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct let vtop x = { x with value = VarMap.empty } let bottom vars = raise Bot (* we don't represent Bot *) let is_bot x = false + let is_top x = + VarMap.for_all + (fun k v -> List.for_all (fun vv -> List.mem vv v) + (List.assoc k x.vars)) + x.value let vars x = x.vars |