From a415b355858c869d0823ec4c5f2504403e714837 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Mar 2022 16:44:26 +0100
Subject: [PATCH] [kernel] use proper function to find matching compinfo in ast
diff
---
src/kernel_services/ast_queries/ast_diff.ml | 10 +++++-----
tests/syntax/ast_diff_1.i | 6 ++++++
tests/syntax/ast_diff_2.i | 4 ++++
tests/syntax/oracle/ast_diff_1.res.oracle | 4 ++++
4 files changed, 19 insertions(+), 5 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 886a44ef38e..be7053cfa7f 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -352,12 +352,12 @@ let find_candidate_type ?loc:_loc ti =
let find_candidate_compinfo ?loc:_loc ci =
let su = if ci.cstruct then Logic_typing.Struct else Logic_typing.Union in
if Globals.Types.mem_type su ci.cname then begin
- match Globals.Types.global su ci.cname with
- | GCompTag (ci,_) | GCompTagDecl(ci,_) -> Some ci
- | g ->
+ match Globals.Types.find_type su ci.cname with
+ | TComp(ci', _) -> Some ci'
+ | t ->
Kernel.fatal
- "Expected aggregate definition instead of %a"
- Cil_datatype.Global.pretty g
+ "Expected compinfo instead of %a"
+ Printer.pp_typ t
end else None
let find_candidate_enuminfo ?loc:_loc ei =
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 49b8262c90e..80d699482c5 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -72,3 +72,9 @@ void local_var_use(int v, int a[][v]) {
int x;
int y [sizeof(x)];
}
+
+struct s;
+
+extern struct s s;
+
+struct s* use_s() { return &s; }
diff --git a/tests/syntax/ast_diff_2.i b/tests/syntax/ast_diff_2.i
index c1775d8d10f..bd8d7e8f1f8 100644
--- a/tests/syntax/ast_diff_2.i
+++ b/tests/syntax/ast_diff_2.i
@@ -67,3 +67,7 @@ void local_var_use(int w, int q[][w]) {
int z;
int t [sizeof(z)];
}
+
+extern struct s s;
+
+struct s* use_s() { return &s; }
diff --git a/tests/syntax/oracle/ast_diff_1.res.oracle b/tests/syntax/oracle/ast_diff_1.res.oracle
index da62e41fd42..1286ff511f9 100644
--- a/tests/syntax/oracle/ast_diff_1.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.res.oracle
@@ -7,10 +7,13 @@
[AST diff test] Variable a: => q
[AST diff test] Variable x: => z
[AST diff test] Variable y: => t
+[AST diff test] Variable s: => s
+[AST diff test] Variable use_s: => use_s
[AST diff test] Variable has_static_local_x: => has_static_local_y
[AST diff test] Variable X: => X
[AST diff test] Variable Y: N/A
[AST diff test] Variable f: => f
+[AST diff test] Variable __retres: => __retres
[AST diff test] Variable x: => x
[AST diff test] Variable g: => g
[AST diff test] Variable h: => h
@@ -23,6 +26,7 @@
[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 use_s: => use_s
[AST diff test] Function f: => f
[AST diff test] Function g: N/A
[AST diff test] Function h: -> h (body changed)
--
GitLab