[eacsl] Function to retrieve the RTL replacement of a libc function

src/plugins/e-acsl/src/project_initializer/rtl.ml

@@ -55,6 +55,7 @@ module Symbols: sig
   val mem_vi: string -> bool
   exception Unregistered of string
   val find_vi: string -> varinfo (* may raise Unregistered *)
+  val libc_replacement: varinfo -> varinfo
   (*  val debug: unit -> unit*)
 end = struct
 
@@ -77,6 +78,16 @@ end = struct
     try Datatype.String.Hashtbl.find vars s
     with Not_found -> raise (Unregistered s)
 
+  let libc_replacement fvi =
+    let name = Functions.RTL.libc_replacement_name fvi.vname in
+    try
+      find_vi name
+    with Unregistered _ ->
+      Options.fatal
+        "Unable to find RTL function '%s' to replace libc function '%s'"
+        name
+        fvi.vname
+
 (*
   let debug () =
     Global.Hashtbl.iter

src/plugins/e-acsl/src/project_initializer/rtl.mli

@@ -39,6 +39,9 @@ module Symbols: sig
   val find_vi: string -> varinfo
   (** @raise Unregistered if the given name is not part of the RTL. *)
 
+  val libc_replacement: varinfo -> varinfo
+  (** Given the varinfo of a C library function with an RTL replacement, return
+      the varinfo of the RTL function that replaces it. *)
 end
 
 (*