diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index f53bf4685640ed645803b0b785f35dfc1fde7293..f02f3d926210636721764f725c32f6155842ffe7 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -121,7 +121,7 @@ class visitor = object(self)
     Error.cannot_check_ghost_call ~source ~current:true ~once:true kf
 
   method! vglob_aux = function
-    | GFunDecl(_, vi, _) ->
+    | GFunDecl(_, vi, _) when vi.vghost ->
       self#prefer_loc (Log.get_current_source ()) ;
       let post g = self#reset_loc() ; g in
 
@@ -136,7 +136,11 @@ class visitor = object(self)
         if is_empty_funspec spec then self#bad_ghost_function kf
       end ;
       Cil.DoChildrenPost post
-    | _ -> Cil.DoChildren
+    (* Optimization: only visits ghost globals or globals that may contain
+       ghost code. *)
+    | GVarDecl (vi, _) when vi.vghost -> Cil.DoChildren
+    | GVar _ | GFun _ -> Cil.DoChildren
+    | _ -> Cil.SkipChildren
 
   method! vvdec v =
     let current, source =