[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

@@ -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

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); */

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); */

tests/syntax/oracle/ast_diff_1.res.oracle

 [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