Allow non-void types for RichVarinfo

goblint · Mar 15, 2024 · 932ac3b · 932ac3b
1 parent a10c973
commit 932ac3b
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 10 deletions.
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -951,7 +951,7 @@ struct
   (* sync: M -> (2^M -> (G -> D)) *)
   include AbstractLockCenteredBase (ThreadMap) (LockCenteredBase.CPA)
 
-  let global_init_thread = RichVarinfo.single ~name:"global_init"
+  let global_init_thread = RichVarinfo.single ~name:"global_init" ~typ:GoblintCil.voidType
   let current_thread (ask: Q.ask): Thread.t =
     if !AnalysisState.global_initialization then
       ThreadIdDomain.Thread.threadinit (global_init_thread ()) ~multiple:false

diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml
@@ -144,6 +144,8 @@ module MallocWrapper : MCPSpec = struct
           Format.dprintf "@tid:%s" (ThreadLifted.show t)
       in
       Format.asprintf "(alloc@sid:%s%t%t)" (Node.show_id node) tid uniq_count
+
+    let typ _ = GoblintCil.voidType
   end
 
   module NodeVarinfoMap = RichVarinfo.BiVarinfoMap.Make(ThreadNode)

diff --git a/src/common/util/richVarinfo.ml b/src/common/util/richVarinfo.ml
@@ -1,9 +1,9 @@
 open GoblintCil
 
-let create_var name = Cilfacade.create_var @@ makeGlobalVar name voidType
+let create_var name typ = Cilfacade.create_var @@ makeGlobalVar name typ
 
-let single ~name =
-  let vi = lazy (create_var name) in
+let single ~name ~typ =
+  let vi = lazy (create_var name typ) in
   fun () ->
     Lazy.force vi
 
@@ -21,6 +21,7 @@ module type G =
 sig
   include Hashtbl.HashedType
   val name_varinfo: t -> string
+  val typ: t -> typ
 end
 
 module type H =
@@ -47,7 +48,7 @@ struct
     try
       XH.find !xh x
     with Not_found ->
-      let vi = create_var (X.name_varinfo x) in
+      let vi = create_var (X.name_varinfo x) (X.typ x) in
       store_f x vi;
       vi
 

diff --git a/src/common/util/richVarinfo.mli b/src/common/util/richVarinfo.mli
@@ -2,7 +2,7 @@
 
 open GoblintCil
 
-val single: name:string -> (unit -> varinfo)
+val single: name:string -> typ:typ -> (unit -> varinfo)
 
 module type VarinfoMap =
 sig
@@ -18,6 +18,7 @@ module type G =
 sig
   include Hashtbl.HashedType
   val name_varinfo: t -> string
+  val typ: t -> typ
 end
 
 module type H =

diff --git a/src/witness/witnessGhost.ml b/src/witness/witnessGhost.ml
@@ -11,9 +11,7 @@ struct
     | Locked l -> LockDomain.Addr.show l ^ "_locked" (* TODO: valid C name *)
     | Multithreaded -> "multithreaded"
 
-  (* TODO: define correct types *)
-
-  let type_ = function
+  let typ = function
     | Locked _ -> GoblintCil.intType
     | Multithreaded -> GoblintCil.intType
 
@@ -30,7 +28,7 @@ include Map
 
 let variable_entry ~task x =
   let variable = name_varinfo x in
-  let type_ = String.trim (CilType.Typ.show (type_ x)) in (* CIL printer puts space at the end of some types *)
+  let type_ = String.trim (CilType.Typ.show (typ x)) in (* CIL printer puts space at the end of some types *)
   let initial = CilType.Exp.show (initial x) in
   YamlWitness.Entry.ghost_variable ~task ~variable ~type_ ~initial