From 389923a14667801c9720283e6517895b7c6e7b6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 2 May 2022 10:47:52 +0200
Subject: [PATCH] [kernel] Ast_diff: checks the type of corresponding global
variables.
---
src/kernel_services/ast_queries/ast_diff.ml | 19 ++++++++++---------
1 file changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 56025255e45..a468dbdc3c7 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1249,8 +1249,6 @@ and is_same_fundec f f' env: body_correspondance =
| `Body_changed -> ());
res
-(* only for locals and formals. Globals are treated by
- gvar_correspondance below. *)
and is_same_varinfo vi vi' env =
is_same_type vi.vtype vi'.vtype env &&
Cil_datatype.Attributes.equal vi.vattr vi'.vattr
@@ -1373,13 +1371,16 @@ and gvar_correspondance ?loc vi env =
end
| None -> `Not_present
| Some vi' ->
- let selection = State_selection.singleton Globals.Vars.self in
- let init =
- Project.on ~selection (Orig_project.get()) Globals.Vars.find vi
- in
- let init' = Globals.Vars.find vi' in
- let res = is_same_initinfo init init' empty_env in
- if res then `Same vi' else `Not_present
+ if is_same_varinfo vi vi' env
+ then
+ let selection = State_selection.singleton Globals.Vars.self in
+ let init =
+ Project.on ~selection (Orig_project.get()) Globals.Vars.find vi
+ in
+ let init' = Globals.Vars.find vi' in
+ let res = is_same_initinfo init init' empty_env in
+ if res then `Same vi' else `Not_present
+ else `Not_present
in
Varinfo.memo add vi
--
GitLab