[variadic] Add a state to store the association between original and replaced functions

src/plugins/variadic/Makefile.in

@@ -37,7 +37,7 @@ PLUGIN_DIR ?= .
 PLUGIN_ENABLE := @ENABLE_VARIADIC@
 PLUGIN_NAME := Variadic
 PLUGIN_CMI := format_types va_types
-PLUGIN_CMO := options extends va_build environment \
+PLUGIN_CMO := options extends va_build environment replacements \
               format_string format_pprint format_typer format_parser \
               generic standard classify translate \
               register

src/plugins/variadic/replacements.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* State to store the association between a replaced function and the original
+   function. *)
+module Replacements =
+  Cil_state_builder.Varinfo_hashtbl
+    (Cil_datatype.Varinfo)
+    (struct
+      let size = 17
+      let name = "replacements"
+      let dependencies = [ Options.Enabled.self; Options.Strict.self ]
+    end)
+
+let add new_vi old_vi =
+  Replacements.add new_vi old_vi
+
+let find new_vi =
+  Replacements.find new_vi
+
+let mem new_vi =
+  Replacements.mem new_vi

src/plugins/variadic/replacements.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Cil_types
+
+val add: varinfo -> varinfo -> unit
+(** [add replaced original] stores the association of the original and the
+    replaced functions in a project state. *)
+
+val find: varinfo -> varinfo
+(* [find fct] returns the original function for [fct] from the project state if
+   it has been replaced. Raise [Not_found] if no original function exists. *)
+
+val mem: varinfo -> bool
+(* [mem fct] returns true if an original function exists for [fct], false
+   otherwise. *)