diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml index 5041723291b7ba862146e99dfadf6a62ee9ec26e..886a44ef38eeb8469fa23b43aca546127e6a0ab3 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 4858468ec5f9cdf9344ab9dba021e730d4ad0548..49b8262c90e47133693f22218243f984059f41b1 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 094bee8d12c9c449bf49dbad7d9e79c29fd1e9a3..c1775d8d10f6c61c29c867e4e30c70905b9f0b0a 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 976c046d2727fe3bffb9ca4ca95d9363b04778e0..da62e41fd4286bacf265b9d3681d8ab57c6b1f0d 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