diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index efa30dd..ed029da 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -5,9 +5,11 @@ open Ast open Value_domain open Num_domain -let debug = false +(* + Implementation of a nonrelationnal domain for numerical values. -(* Restricted domain, only support integers *) + Restricted implementation, only support integers. +*) module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t @@ -160,11 +162,6 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct | AST_LT -> let u, _ = V.leq v1 (V.sub v2 (V.const 1)) in u | AST_GT -> let _, v = V.leq (V.add v2 (V.const 1)) v1 in v in - if debug then Format.printf - "restrict %s %s @[<hv>%a@] : %s %s -> %s@." i - (Formula_printer.string_of_binary_rel op) - Formula_printer.print_num_expr expr - (V.to_string v1) (V.to_string v2) (V.to_string v1'); Env (VarMap.add i v1' env)) env in |