From 23c8069765ee298e782add564c745e8d6f1790bc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jan 2022 17:51:33 +0100
Subject: [PATCH] [kernel] Optimizes undefined_sequence visitor: only visits
function definitions.
---
src/kernel_services/analysis/undefined_sequence.ml | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/kernel_services/analysis/undefined_sequence.ml b/src/kernel_services/analysis/undefined_sequence.ml
index 049492f80f2..39e7f83db25 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
--
GitLab