From 77bbf5484ec72c601ca2c85ae1538d25113b39d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 15 Mar 2022 11:54:34 +0100
Subject: [PATCH] [kernel] Ast diff: fixes the computation of correspondances
between logic_info.
---
src/kernel_services/ast_queries/ast_diff.ml | 38 ++++++++-------------
1 file changed, 14 insertions(+), 24 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index ce895a7c9d6..2c220cf12db 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -1240,18 +1240,11 @@ and find_candidate_logic_var ?loc:_loc lv env =
and find_candidate_logic_info ?loc:_loc li env =
let candidates = Logic_env.find_all_logic_functions li.l_var_info.lv_name in
let find_one li' =
- is_same_list is_same_logic_var li.l_profile li'.l_profile env
+ let res, env = logic_type_vars_env li.l_tparams li'.l_tparams env in
+ res && is_same_list is_same_logic_var li.l_profile li'.l_profile env
+ && is_same_opt is_same_logic_type li.l_type li'.l_type env
in
- let rec extract l =
- match l with
- | [] -> None
- | li' :: tl -> if find_one li' then Some li' else extract tl
- in
- match extract candidates with
- | None -> None
- | Some li' ->
- let res = is_same_opt is_same_logic_type li.l_type li'.l_type env in
- if res then Some li' else None
+ List.find_opt find_one candidates
and find_candidate_model_info ?loc:_loc mi env =
let candidates = Logic_env.find_all_model_fields mi.mi_name in
@@ -1422,19 +1415,16 @@ and logic_info_correspondance ?loc li env =
match find_candidate_logic_info ?loc li env with
| None -> `Not_present
| Some li' ->
- if is_same_list is_same_logic_var li.l_profile li'.l_profile env then
- begin
- let env = add_logic_prms li.l_profile li'.l_profile env in
- let env =
- { env with
- logic_info=Cil_datatype.Logic_info.Map.add li li' env.logic_info }
- in
- let res = is_same_logic_info li li' env in
- if res then begin
- logic_prms_correspondance li.l_profile li'.l_profile;
- `Same li'
- end else `Not_present
- end else `Not_present
+ let env = add_logic_prms li.l_profile li'.l_profile env in
+ let env =
+ { env with
+ logic_info=Cil_datatype.Logic_info.Map.add li li' env.logic_info }
+ in
+ let res = is_same_logic_info li li' env in
+ if res then begin
+ logic_prms_correspondance li.l_profile li'.l_profile;
+ `Same li'
+ end else `Not_present
in
match Cil_datatype.Logic_info.Map.find_opt li env.logic_info with
| Some li' -> `Same li'
--
GitLab