diff options
Diffstat (limited to 'abstract/abs_domain.ml')
| -rw-r--r-- | abstract/abs_domain.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml index a30713a..64eefc7 100644 --- a/abstract/abs_domain.ml +++ b/abstract/abs_domain.ml @@ -223,8 +223,23 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct let var_itv x id = if List.mem_assoc id x.nvars - then IN (VMap.map (fun v -> ND.var_itv v id) x.value) - else not_implemented "var_itv for enum variable" + then + let x = List.fold_left + (fun x (v, _) -> + if v.[0] = 'N' || (String.length v > 3 && String.sub v 0 3 = "pre") + then forgetvar x v else x) + x x.evars in + IN (VMap.map (fun v -> ND.var_itv v id) x.value) + else + let all = List.fold_left (fun a b -> SSet.add b a) SSet.empty + (List.assoc id x.evars) in + IE + (VMap.fold + (fun enum _ s -> + try SSet.add (VarMap.find id enum) s + with Not_found -> all) + x.value + SSet.empty) let set_disjunct x id p = { x with @@ -356,7 +371,7 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct { x with value = VMap.empty } let print_all fmt x = - Format.fprintf fmt "@[<v 0>"; + Format.fprintf fmt "@[<v>"; VMap.iter (fun enum num -> Format.fprintf fmt "@[<hv 2>{ %a ∧@ %a }@]@ " |