Rename single_vf -> top and empty -> bot

src/analyses/regionNonEscape.ml

@@ -107,7 +107,7 @@ struct
       begin match Reg.eval_exp ptc_arg with
         | Some (deref_y, y) when not (Reg.is_global y) ->
           (* Variable escapes if used as an argument when spawning a new thread *)
-          Reg.add_set (RS.join RS.single_vf (RegMap.find y reg)) [y] reg
+          Reg.add_set (RS.join (RS.top ()) (RegMap.find y reg)) [y] reg
         | _ -> reg
       end
     | _ -> reg

src/cdomains/regionNonEscapeDomain.ml

@@ -4,13 +4,13 @@ open GoblintCil
 
 module RS : sig
   include Lattice.S
-  val single_vf : t
-  val single_bullet : t
+  val bot : unit -> t
+  val single_bullet : unit -> t
+  val top : unit -> t
   val remove_bullet : t -> t
-  val empty : unit -> t
   val has_bullet : t -> bool
   val is_single_bullet : t -> bool
-  val is_empty : t -> bool
+  val is_bot : t -> bool
 end = struct
   module Bullet =
   struct
@@ -22,13 +22,14 @@ end = struct
       | _ -> failwith "Invalid Bullet value"
   end
   include Lattice.Chain (Bullet)
-  let single_vf = 2
-  let single_bullet = 1
+  let bot () = 0
+  let single_bullet () = 1
+  let top () = 2
   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
+  let is_bot n = n = 0
 end
 
 module RegMap =
@@ -84,15 +85,15 @@ struct
       | Some (deref_x,x), Some (deref_y,y) -> begin
           match is_global x, deref_x, is_global y with
           | false, false, true  ->
-            RegMap.add x RS.single_vf reg
+            RegMap.add x (RS.top ()) reg
           | false, false, false ->
             RegMap.add x (RegMap.find y reg) reg
           | false, true , true  ->
-            add_set (RS.join (RegMap.find x reg) RS.single_vf) [x] reg (* Variable escapes when it is assigned a value from a global variable *)
+            add_set (RS.join (RegMap.find x reg) (RS.top ())) [x] reg (* Variable escapes when it is assigned a value from a global variable *)
           | false, true , false ->
             add_set (RS.join (RegMap.find x reg) (RegMap.find y reg)) [x;y] reg
           | true , _    , false ->
-            add_set (RS.join RS.single_vf (RegMap.find y reg)) [y] reg (* Variable escapes when assigned to global variable *)
+            add_set (RS.join (RS.top ()) (RegMap.find y reg)) [y] reg (* Variable escapes when assigned to global variable *)
           | true , _    , true  ->
             reg
         end
@@ -105,15 +106,15 @@ struct
 
   let assign_bullet lval m: t =
     match eval_exp (Lval lval) with
-    | Some (_, x) -> RegMap.add x RS.single_bullet m
+    | Some (_, x) -> RegMap.add x (RS.single_bullet ()) m
     | _ -> m
 
   let related_globals deref_vfd m =
     match deref_vfd with
-    | Some (_, vfd) when is_global vfd -> RS.single_vf
+    | Some (_, vfd) when is_global vfd -> RS.top ()
     | Some (true, vfd) -> RegMap.find vfd m
-    | Some (false, vfd) -> RS.empty ()
-    | None -> Messages.info ~category:Unsound "Access to unknown address could be global"; RS.empty ()
+    | Some (false, vfd) -> RS.bot ()
+    | None -> Messages.info ~category:Unsound "Access to unknown address could be global"; RS.bot ()
 end
 
 module RegionDom = RegMap