From e9e0f8f2bec60f9c4bfeb8315325737986bef7a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 24 Jan 2022 11:35:05 +0100
Subject: [PATCH] [kernel] Optimizes the "ghost access checking" code
transformation.
Only visits globals that are ghost or may contain ghost code.
---
src/kernel_internals/typing/ghost_accesses.ml | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index f53bf468564..f02f3d92621 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 =
--
GitLab