diff options
Diffstat (limited to 'abstract/value_domain.ml')
| -rw-r--r-- | abstract/value_domain.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index bb27126..0a421f7 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -10,6 +10,7 @@ let string_of_itv = function | Bot -> "⊥" | Itv(a, b) -> "[" ^ (string_of_bound a) ^ "; " ^ (string_of_bound b) ^ "]" + module type VALUE_DOMAIN = sig type t @@ -17,7 +18,7 @@ module type VALUE_DOMAIN = sig val top : t val bottom : t val const : int -> t - val rand : int -> int -> t + val itv : int -> int -> t val to_itv : t -> itv val as_const : t -> int option @@ -37,8 +38,8 @@ module type VALUE_DOMAIN = sig val div : t -> t -> t val rem : t -> t -> t - (* boolean test *) - val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) + (* restrict two values considering that the first is smaller than the second *) + val leq : t -> t -> t * t (* pretty-printing *) val to_string : t -> string |