Change RS domain from Lattice.Prod to Lattice.Chain

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 =