diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 89a968608b2a78b896d95282b0a0d3ec1f4569ae..a411a59c7f2477ed91b34528a3d97a5272e97d9f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2971,8 +2971,14 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
       Kernel.debug ~dkey:Kernel.dkey_typing_global
         "makeGlobalVarinfo isadef=%B vi.vname=%s(%d), vreferenced=%B"
         isadef vi.vname vi.vid vi.vreferenced;
-      (* This may throw an exception Not_found *)
-      let oldvi, oldloc = lookupGlobalVar vi.vghost vi.vname in
+      (* This may throw an exception Not_found
+         Note that we always search in all the context, including ghost *)
+      let oldvi, oldloc = lookupGlobalVar true vi.vname in
+      if oldvi.vghost <> vi.vghost then
+        abort_context "Inconsistent ghost specification for %s.@ \
+                       Previous declaration was at: %a"
+          vi.vname Cil_datatype.Location.pretty oldloc ;
+
       Kernel.debug ~dkey:Kernel.dkey_typing_global
         "  %s(%d) already in the env at loc %a"
         vi.vname oldvi.vid Cil_printer.pp_location oldloc;
diff --git a/tests/syntax/inconsistent_global_ghost_spec.c b/tests/syntax/inconsistent_global_ghost_spec.c
new file mode 100644
index 0000000000000000000000000000000000000000..8a3aa44011c7c8c8bfa1693b57631cdc8f5b5f1a
--- /dev/null
+++ b/tests/syntax/inconsistent_global_ghost_spec.c
@@ -0,0 +1,50 @@
+/* run.config
+OPT: -cpp-extra-args="-DNON_GHOST_DECL_GHOST_DEF"
+OPT: -cpp-extra-args="-DGHOST_DECL_NON_GHOST_DEF"
+OPT: -cpp-extra-args="-DGHOST_DEF_NON_GHOST_DECL"
+OPT: -cpp-extra-args="-DNON_GHOST_DEF_GHOST_DECL"
+*/
+
+#ifdef NON_GHOST_DECL_GHOST_DEF
+
+void function(void) ;
+/*@ ghost void function(void){ } */
+
+void user(void){
+  function();
+}
+
+#endif
+
+#ifdef GHOST_DECL_NON_GHOST_DEF
+
+/*@ ghost void function(void) ; */
+void function(void){ }
+
+void user(void){
+  function();
+}
+
+#endif
+
+#ifdef GHOST_DEF_NON_GHOST_DECL
+
+/*@ ghost void function(void){ } */
+void function(void) ;
+
+void user(void){
+  function();
+}
+
+#endif
+
+#ifdef NON_GHOST_DEF_GHOST_DECL
+
+void function(void){ }
+/*@ ghost void function(void) ; */
+
+void user(void){
+  function();
+}
+
+#endif
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1a6ff7363d29f6dc41109ee9f63bf417d1cd00bd
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.0.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:11: User Error: 
+  Inconsistent ghost specification for function.
+  Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:10
+  9     
+  10    void function(void) ;
+  11    /*@ ghost void function(void){ } */
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  12    
+  13    void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+  errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f44d69202405c7ad9edec60736f181877f8dc38d
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.1.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:22: User Error: 
+  Inconsistent ghost specification for function.
+  Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:21
+  20    
+  21    /*@ ghost void function(void) ; */
+  22    void function(void){ }
+        ^^^^^^^^^^^^^^^^^^^^^^
+  23    
+  24    void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+  errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ce9a25fb88246f4983f60c6aff87c3dc00ddd89c
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.2.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:33: User Error: 
+  Inconsistent ghost specification for function.
+  Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:32
+  31    
+  32    /*@ ghost void function(void){ } */
+  33    void function(void) ;
+        ^^^^^^^^^^^^^^^^^^^^^
+  34    
+  35    void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+  errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..70bc963d684bac791353879db43ce3a7d2421e1a
--- /dev/null
+++ b/tests/syntax/oracle/inconsistent_global_ghost_spec.3.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/inconsistent_global_ghost_spec.c (with preprocessing)
+[kernel] tests/syntax/inconsistent_global_ghost_spec.c:44: User Error: 
+  Inconsistent ghost specification for function.
+  Previous declaration was at: tests/syntax/inconsistent_global_ghost_spec.c:43
+  42    
+  43    void function(void){ }
+  44    /*@ ghost void function(void) ; */
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+  45    
+  46    void user(void){
+[kernel] User Error: stopping on file "tests/syntax/inconsistent_global_ghost_spec.c" that has
+  errors. Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.