diff --git a/src/cdomains/regionNonEscapeDomain.ml b/src/cdomains/regionNonEscapeDomain.ml index 145879f3cf..8950a9b4a5 100644 --- a/src/cdomains/regionNonEscapeDomain.ml +++ b/src/cdomains/regionNonEscapeDomain.ml @@ -12,14 +12,23 @@ module RS : sig val is_single_bullet : t -> bool val is_empty : t -> bool end = struct - include Lattice.Prod (BoolDomain.MayBool) (BoolDomain.MayBool) - let single_vf = (true, true) - let single_bullet = (false, true) - let remove_bullet (l, _) = (l, l) - let empty () = (false, false) - let has_bullet (_, r) = r = true - let is_single_bullet (l, r) = l = false && r = true - let is_empty (l, r) = l = false && r = false + module Bullet = + struct + let n () = 3 + let names = function + | 0 -> "Bot" + | 1 -> "Bullet" (* Non-escaped *) + | 2 -> "Top" (* Escaped *) + | _ -> failwith "Invalid Bullet value" + end + include Lattice.Chain (Bullet) + let single_vf = 2 + let single_bullet = 1 + let remove_bullet n = if n == 2 then 2 else 0 + let empty () = 0 + let has_bullet n = n > 0 + let is_single_bullet n = n = 1 + let is_empty n = n = 0 end module RegMap =