diff options
Diffstat (limited to 'abstract/nonrelational.ml')
| -rw-r--r-- | abstract/nonrelational.ml | 21 |
1 files changed, 5 insertions, 16 deletions
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 855f970..492b547 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -3,13 +3,13 @@ open Util open Ast open Value_domain -open Environment_domain +open Num_domain let debug = false (* Restricted domain, only support integers *) -module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct +module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct type env = V.t VarMap.t type t = Env of env | Bot @@ -167,20 +167,9 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct List.fold_left restrict_var env (extract_var (expr, zop, NIntConst 0)) - let rec apply_cl x (cons, rest) = match rest with - | CLTrue -> - let apply_cl_l x = List.fold_left apply_cons x cons in - fix eq apply_cl_l x - | CLFalse -> vbottom x - | CLAnd(a, b) -> - let y = apply_cl x (cons, a) in - apply_cl y (cons, b) - | CLOr((ca, ra), (cb, rb)) -> - let y = apply_cl x (cons@ca, ra) in - let z = apply_cl x (cons@cb, rb) in - join y z - - let apply_f x f = apply_cl x (conslist_of_f f) + let apply_ncl x cl = + let f x = List.fold_left apply_cons x cl in + fix eq f x (* Assignment *) let assign x exprs = |