diff --git a/src/kernel_services/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml
index 049492f80f2a0a74e44a9aa8f104e3da2ce55d12..39e7f83db2562220bacb41352c737e1d108369ec 100644
--- a/src/kernel_services/analysis/undefined_sequence.ml
+++ b/src/kernel_services/analysis/undefined_sequence.ml
@@ -143,6 +143,18 @@ let check_sequences file =
              (my_stmt_print#without_annot my_stmt_print#stmt) s
        | _ -> ());
       Cil.DoChildren
+
+    (* Optimization: only visits function definitions. *)
+    method! vglob = function
+      | GFun _ -> Cil.DoChildren
+      | _ -> Cil.SkipChildren
+
+    method! vinst _ = SkipChildren
+    method! vexpr _ = SkipChildren
+    method! vlval _ = SkipChildren
+    method! vtype _ = SkipChildren
+    method! vspec _ = SkipChildren
+    method! vcode_annot _ = SkipChildren
   end
   in
   Cil.visitCilFileSameGlobals check_unspec file