From 8f061a06a089d75917c04476321bc693cf403201 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 24 Jan 2022 21:18:13 +0100
Subject: [PATCH] [kernel] Cfg: optimizes a visitor: skip some parts of the
visit.
---
src/kernel_internals/typing/cfg.ml | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index d9cb57f9193..d0e7b4da779 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -307,6 +307,13 @@ let forallStmts todo (fd : fundec) =
let vis = object
inherit nopCilVisitor
method! vstmt stmt = ignore (todo stmt); DoChildren
+ method! vinst _ = SkipChildren
+ method! vexpr _ = SkipChildren
+ method! vlval _ = SkipChildren
+ method! vtype _ = SkipChildren
+ method! vspec _ = SkipChildren
+ method! vcode_annot _ = SkipChildren
+ method! vattr _ = SkipChildren
end
in
ignore (visitCilFunction vis fd)
@@ -744,6 +751,7 @@ class registerLabelsVisitor : cilVisitor = object
method! vexpr _ = SkipChildren
method! vtype _ = SkipChildren
method! vinst _ = SkipChildren
+ method! vspec _ = SkipChildren
method! vcode_annot _ = SkipChildren (* via Loop stmt *)
method! vlval _ = SkipChildren (* via UnspecifiedSequence stmt *)
method! vattr _ = SkipChildren (* via block stmt *)
--
GitLab