From 1bafbc1a941357fd035dec796fcbdff3ba9176bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 20 Jan 2022 20:51:42 +0100
Subject: [PATCH] [kernel] Logic_utils: optimizes the [complete_types] visitor.
Skips the visit of C codes.
---
src/kernel_services/ast_queries/logic_utils.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index d7e5d704db6..347c154d719 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2349,6 +2349,15 @@ class complete_types =
not (isLogicType Cil.isCompleteType t.term_type) ->
ChangeDoChildrenPost({ t with term_type = v.lv_type }, fun x -> x)
| _ -> DoChildrenPost self#insert_cast_term
+
+ method! vinst = function
+ | Code_annot _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
+ method! vexpr _ = Cil.SkipChildren
+ method! vlval _ = Cil.SkipChildren
+ method! vtype _ = Cil.SkipChildren
+ method! vinit _ _ _ = Cil.SkipChildren
end
let complete_types f = Cil.visitCilFile (new complete_types) f
--
GitLab