diff --git a/Makefile b/Makefile
index 0f4ac62279f4715a7f850cb5d9d89fd0c3de60d9..930b19a61c5914d898d211c20db170c7452a1d38 100644
--- a/Makefile
+++ b/Makefile
@@ -191,7 +191,7 @@ THEME_ICONS_FLAT:= \
   $(addprefix share/theme/flat/,$(THEME_ICON_NAMES))
 
 ROOT_LIBC_DIR:= share/libc
-LIBC_SUBDIRS:= sys netinet net arpa
+LIBC_SUBDIRS:= sys netinet net arpa aorai
 LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS))
 LIBC_FILES:= \
 	$(wildcard share/*.h share/*.c) \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d1b383e76b2d8a39234b67339deb1984c7ad12b3..69a036f5610cc986d402c06130367d7c7dd673b4 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -208,6 +208,7 @@ share/libc/__fc_runtime.c: CEA_LGPL
 share/libc/__fc_select.h: CEA_LGPL
 share/libc/__fc_string_axiomatic.h: CEA_LGPL
 share/libc/alloca.h: CEA_LGPL
+share/libc/aorai/aorai.h: CEA_LGPL
 share/libc/arpa/inet.h: CEA_LGPL
 share/libc/assert.c: CEA_LGPL
 share/libc/assert.h: CEA_LGPL
diff --git a/share/libc/aorai/aorai.h b/share/libc/aorai/aorai.h
new file mode 100644
index 0000000000000000000000000000000000000000..b2f5eeb733fa6beb109b4a54797214d8a201e79e
--- /dev/null
+++ b/share/libc/aorai/aorai.h
@@ -0,0 +1,33 @@
+/**************************************************************************/
+/*                                                                        */
+/*  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).            */
+/*                                                                        */
+/**************************************************************************/
+
+#ifndef __FC_AORAI
+#define __FC_AORAI
+
+/*@ ghost extern int aorai_CurStates; */
+/*@ ghost extern int aorai_StatesHistory1; */
+/*@ ghost extern int aorai_StatesHistory2; */
+/*@ ghost extern int aorai_StatesHistory3; */
+/*@ ghost extern int aorai_StatesHistory4; */
+
+
+#endif
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 274932dd15c975e3412422ae8842e1b9ff945284..14530aceb21f003485b4a74416e7455796519586 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -680,6 +680,7 @@ let add_global glob = globals_queue := glob :: !globals_queue
 let add_gvar ?init vi =
   let initinfo = {Cil_types.init} in
   vi.vghost <- true;
+  vi.vstorage <- NoStorage;
   add_global (GVar(vi,initinfo,vi.vdecl));
   Globals.Vars.add vi initinfo;
   set_varinfo vi.vname vi
@@ -688,7 +689,19 @@ let add_gvar_zeroinit vi =
   add_gvar ~init:(Cil.makeZeroInit ~loc:(CurrentLoc.get()) vi.vtype) vi
 
 let mk_gvar ?init ~ty name =
-  let vi = Cil.makeGlobalVar name ty in
+  (* See if the variable is already declared *)
+  let vi =
+    try
+      let ty' = typeAddAttributes [Attr ("ghost", [])] ty in
+      let vi = Globals.Vars.find_from_astinfo name VGlobal in
+      if not (Cil_datatype.Typ.equal vi.vtype ty') then
+        Aorai_option.abort "Global %s is declared with type %a instead of %a"
+          name Cil_printer.pp_typ vi.vtype Cil_printer.pp_typ ty';
+      Globals.Vars.remove vi;
+      vi
+    with Not_found ->
+      Cil.makeGlobalVar name ty
+  in
   add_gvar ?init vi
 
 let mk_gvar_scalar ~init ?(ty = Cil.typeOf init) name =
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index b1e1247a43669f03d504de710fa2a4b5337ce754..852a3378808b5fd9471ec06cf612b0c65da0e7eb 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -42,6 +42,7 @@ skipping share/libc/__fc_machdep_linux_shared.h
 [kernel] Parsing share/libc/__fc_select.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_string_axiomatic.h (with preprocessing)
 [kernel] Parsing share/libc/alloca.h (with preprocessing)
+[kernel] Parsing share/libc/aorai/aorai.h (with preprocessing)
 [kernel] Parsing share/libc/arpa/inet.h (with preprocessing)
 [kernel] Parsing share/libc/assert.h (with preprocessing)
 [kernel] Parsing share/libc/byteswap.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 73dac90425a73c971fb285476320f30bc36be7d1..3c89feea03b4a5c923cf5dcf11cf391b647c4a2b 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1 +1,2 @@
 #include "__fc_integer.h"
+#include "aorai/aorai.h"