diff --git a/src/plugins/variadic/Makefile.in b/src/plugins/variadic/Makefile.in
index f4d26f31399440bec477c702582c03b69c5a07b8..09aa6cf0ce8edd403a348c7589fba305bcfa2e99 100644
--- a/src/plugins/variadic/Makefile.in
+++ b/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
diff --git a/src/plugins/variadic/replacements.ml b/src/plugins/variadic/replacements.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ff16032054668bb851749277de87c1587f946a07
--- /dev/null
+++ b/src/plugins/variadic/replacements.ml
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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
diff --git a/src/plugins/variadic/replacements.mli b/src/plugins/variadic/replacements.mli
new file mode 100644
index 0000000000000000000000000000000000000000..09539a4ab346b9dcc539cb77787ce186b32abb0e
--- /dev/null
+++ b/src/plugins/variadic/replacements.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  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. *)