From 3e2b3f9d4e3463866c48746e20ce6c4a873dba4d Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 21 Mar 2022 18:50:56 +0100
Subject: [PATCH] [kernel] ast diff look for a kf only if varinfo has function
type
---
src/kernel_services/ast_queries/ast_diff.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 2c220cf12db..e3c02629f07 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1322,7 +1322,7 @@ and enumitem_correspondance ?loc:_loc ei _env = Enumitem.find ei
and gvar_correspondance ?loc vi env =
let add vi =
match find_candidate_varinfo ?loc vi Cil_types.VGlobal with
- | None ->
+ | None when Cil.isFunctionType vi.vtype ->
begin
match gfun_correspondance ?loc vi env with
| `Same kf' -> `Same (Kf.get_vi kf')
@@ -1332,6 +1332,7 @@ and gvar_correspondance ?loc vi env =
`Same (Kf.get_vi kf')
| `Not_present -> `Not_present
end
+ | None -> `Not_present
| Some vi' ->
let selection = State_selection.singleton Globals.Vars.self in
let init =
--
GitLab