From 346ed802df8d60e1f4bce123611735e97a4b123f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Mar 2022 15:06:44 +0100
Subject: [PATCH] [kernel] ast diff can compare varinfos stemming from global
functions
it turns out that not all global varinfos are stored in Globals.Vars...
---
src/kernel_services/ast_queries/ast_diff.ml | 17 +++++++++++++----
tests/syntax/ast_diff_1.i | 4 ++++
tests/syntax/ast_diff_2.i | 2 ++
tests/syntax/oracle/ast_diff_1.res.oracle | 5 +++--
4 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 5041723291b..886a44ef38e 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -992,7 +992,7 @@ and is_same_lhost h h' env =
and is_matching_varinfo vi vi' env =
if vi.vglob then begin
- match gvar_correspondance vi with
+ match gvar_correspondance vi env with
| `Not_present -> false
| `Same vi'' -> Cil_datatype.Varinfo.equal vi' vi''
end else begin
@@ -1326,10 +1326,19 @@ and enuminfo_correspondance ?loc ei env =
and enumitem_correspondance ?loc:_loc ei _env = Enumitem.find ei
-and gvar_correspondance ?loc vi =
+and gvar_correspondance ?loc vi env =
let add vi =
match find_candidate_varinfo ?loc vi Cil_types.VGlobal with
- | None -> `Not_present
+ | None ->
+ begin
+ match gfun_correspondance ?loc vi env with
+ | `Same kf' -> `Same (Kf.get_vi kf')
+ | `Partial(kf',_) ->
+ (* a partial match at kf level is still the
+ identity for the underlying varinfo *)
+ `Same (Kf.get_vi kf')
+ | `Not_present -> `Not_present
+ end
| Some vi' ->
let selection = State_selection.singleton Globals.Vars.self in
let init =
@@ -1519,7 +1528,7 @@ let global_correspondance g =
| GEnumTag(ei,loc) | GEnumTagDecl(ei,loc) ->
ignore (enuminfo_correspondance ~loc ei empty_env)
| GVar(vi,_,loc) | GVarDecl(vi,loc) ->
- ignore (gvar_correspondance ~loc vi)
+ ignore (gvar_correspondance ~loc vi empty_env)
| GFunDecl(_,vi,loc) -> ignore (gfun_correspondance ~loc vi empty_env)
| GFun(f,loc) -> ignore (gfun_correspondance ~loc f.svar empty_env)
| GAnnot (g,_) -> gannot_correspondance g
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 4858468ec5f..49b8262c90e 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -55,8 +55,12 @@ int decl() {
return used_in_decl;
}
+void (*ptr_func)(void);
+
extern void i(void);
+void (*ptr_func)(void) = &i;
+
/*@ type nat = Zero | Succ(nat); */
/*@ logic nat succ(nat n) = Succ(n); */
diff --git a/tests/syntax/ast_diff_2.i b/tests/syntax/ast_diff_2.i
index 094bee8d12c..c1775d8d10f 100644
--- a/tests/syntax/ast_diff_2.i
+++ b/tests/syntax/ast_diff_2.i
@@ -54,6 +54,8 @@ int decl() {
extern void i(void);
+void (*ptr_func)(void) = &i;
+
/*@ type nat = Zero | Succ(nat); */
/*@ logic nat succ(nat n) = Succ(n); */
diff --git a/tests/syntax/oracle/ast_diff_1.res.oracle b/tests/syntax/oracle/ast_diff_1.res.oracle
index 976c046d272..da62e41fd42 100644
--- a/tests/syntax/oracle/ast_diff_1.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.res.oracle
@@ -1,6 +1,7 @@
[kernel] Parsing ast_diff_1.i (no preprocessing)
[kernel] Parsing ast_diff_2.i (no preprocessing)
[AST diff test] Showing correspondances between orig_default and default
+[AST diff test] Variable i: => i
[AST diff test] Variable local_var_use: => local_var_use
[AST diff test] Variable v: => w
[AST diff test] Variable a: => q
@@ -19,7 +20,8 @@
[AST diff test] Variable has_static_local: => has_static_local
[AST diff test] Variable decl: => decl
[AST diff test] Variable used_in_decl: => used_in_decl
-[AST diff test] Variable i: => i
+[AST diff test] Variable ptr_func: => ptr_func
+[AST diff test] Function i: => i
[AST diff test] Function local_var_use: => local_var_use
[AST diff test] Function f: => f
[AST diff test] Function g: N/A
@@ -27,4 +29,3 @@
[AST diff test] Function use_logic_builtin: => use_logic_builtin
[AST diff test] Function has_static_local: => has_static_local
[AST diff test] Function decl: => decl
-[AST diff test] Function i: => i
--
GitLab