diff options
Diffstat (limited to 'abstract/abs_domain.ml')
| -rw-r--r-- | abstract/abs_domain.ml | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index 64eefc7..d6ff489 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -131,7 +131,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct if i > 0 then Format.fprintf fmt ",@ "; Format.fprintf fmt "%a" Formula_printer.print_id id) ids; - Format.fprintf fmt " = %s@]" v) + Format.fprintf fmt " ≡ %s@]" v) sbl; Format.fprintf fmt " }@]" @@ -171,16 +171,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let strict value = VMap.filter (fun _ v -> not (ND.is_bot v)) value - let add_case x (enum, num) = + let add_case_w widen x (enum, num) = let value = x.value in let enum = VarMap.filter (fun k v -> not (List.mem k x.nodisj_v)) enum in let v = - if VMap.exists (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) value || ND.is_bot num then + if VMap.exists + (fun e0 n0 -> Valuation.subset enum e0 && ND.subset num n0) + value + || ND.is_bot num + then value else - try VMap.add enum (ND.join num (VMap.find enum value)) value + try VMap.add enum + ((if widen then ND.widen else ND.join) (VMap.find enum value) num) + value with Not_found -> VMap.add enum num value in { x with value = v } + let add_case = add_case_w false let addvar x id ty = match ty with | TInt | TReal -> @@ -252,18 +259,18 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let join x y = VMap.fold (fun enum num value -> add_case value (enum, num)) - x.value - y + y.value + x let meet x y = not_implemented "meet for enum+num domain" let widen x y = - { x with - value = VMap.merge - (fun _ a b -> match a, b with - | None, Some a -> Some a - | Some a, None -> Some a - | Some a, Some b -> Some (ND.widen a b) - | _ -> assert false) - x.value y.value } + let value = VMap.merge + (fun _ a b -> match a, b with + | Some x, None -> Some x + | None, Some y -> Some y + | Some x, Some y -> Some (ND.widen x y) + | _ -> None) + x.value y.value + in { x with value = value } (* Some cases of subset/equality not detected *) let subset a b = @@ -281,13 +288,9 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct VMap.fold (fun enum num value -> match a, b with - | EItem x, EItem y -> - if (x = y && op = E_EQ) || (x <> y && op = E_NE) - then add_case value (enum, num) - else value - | EItem u, EIdent i | EIdent i, EItem u -> - begin try let y = VarMap.find i enum in - if (u = y && op = E_EQ) || (u <> y && op = E_NE) + | i, EItem u -> + begin try let v = VarMap.find i enum in + if (if op = E_EQ then u = v else u <> v) then add_case value (enum, num) else value with Not_found -> @@ -300,11 +303,11 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct value (List.filter ((<>) u) (List.assoc i x.evars)) end - | EIdent i, EIdent j -> + | i, EIdent j -> begin try let x = VarMap.find i enum in try let y = VarMap.find j enum in - if (x = y && op = E_EQ) || (x <> y && op = E_NE) + if (if op = E_EQ then x = y else x <> y) then add_case value (enum, num) else value with Not_found (* J not found *) -> |