From f2e883b55a309f6ccef95bc4e8cd0015bfbef1d9 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Mar 2022 14:22:43 +0100
Subject: [PATCH] [kernel] \exit_status is a special case for ast diff
---
src/kernel_services/ast_queries/ast_diff.ml | 25 ++++++++++++++++++++-
tests/syntax/ast_diff_1.i | 1 +
tests/syntax/ast_diff_2.i | 1 +
3 files changed, 26 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 1f4c46afdf4..5041723291b 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -646,9 +646,22 @@ and is_matching_logic_var lv lv' env =
| None ->
(match Logic_var.find lv with
| `Not_present -> false
- | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''))
+ | `Same lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+ | exception Not_found ->
+ if lv.lv_name = "\\exit_status" && lv'.lv_name = "\\exit_status"
+ then begin Logic_var.add lv (`Same lv'); true end
+ else begin
+ match logic_var_correspondance lv env with
+ | None -> false
+ | Some lv'' -> Cil_datatype.Logic_var.equal lv' lv''
+ end))
| _ -> false
+and logic_var_correspondance lv env =
+ match find_candidate_logic_var lv env with
+ | None -> None
+ | Some lv' -> Logic_var.add lv (`Same lv'); Some lv'
+
and is_same_term_offset lo lo' env =
match lo, lo' with
| TNoOffset, TNoOffset -> true
@@ -1212,6 +1225,16 @@ and logic_vars_env l l' env =
else
false, env
+and find_candidate_logic_var ?loc:_loc lv env =
+ let candidates = Logic_env.find_all_logic_functions lv.lv_name in
+ match List.find_opt (fun li -> li.l_profile = []) candidates with
+ | None -> Format.printf "No such var@."; None
+ | Some li ->
+ Format.printf "Found something@.";
+ if is_same_logic_var lv li.l_var_info env then
+ Some li.l_var_info
+ else None
+
(* because of overloading, we have to check for a corresponding profile,
leading to potentially recursive calls to is_same_* functions. *)
and find_candidate_logic_info ?loc:_loc li env =
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 039e389d5e2..4858468ec5f 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -45,6 +45,7 @@ int has_static_local(void) {
return x;
}
+/*@ exits \exit_status == 1; */
int decl(void);
int used_in_decl;
diff --git a/tests/syntax/ast_diff_2.i b/tests/syntax/ast_diff_2.i
index 3f9558f852f..094bee8d12c 100644
--- a/tests/syntax/ast_diff_2.i
+++ b/tests/syntax/ast_diff_2.i
@@ -46,6 +46,7 @@ int has_static_local(void) {
int used_in_decl;
+/*@ exits \exit_status == 1; */
int decl() {
used_in_decl++;
return used_in_decl;
--
GitLab