From cfda0d115b7551363da306afcea74c30a7e9130a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 17 Apr 2024 17:05:18 +0200
Subject: [PATCH] [kernel] Handle extension in code annotations
---
src/kernel_services/ast_queries/ast_diff.ml | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index a0e7883231d..2528fc011f3 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -707,9 +707,6 @@ and is_same_behavior b b' env =
is_same_allocation b.b_allocation b'.b_allocation env &&
is_same_list is_same_acsl_extension b.b_extended b'.b_extended env
-(* TODO: also consider ACSL extensions, with the help of the plugins
- that handle them. *)
-
and is_same_variant (v,m) (v',m') env =
is_same_term v v' env && is_same_opt is_matching_logic_info m m' env
@@ -775,7 +772,10 @@ and is_same_code_annotation a a' env =
| AAllocation(bhvs, a), AAllocation(bhvs',a') ->
is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
| APragma p, APragma p' -> is_same_pragma p p' env
- | AExtended _, AExtended _ -> true (*TODO: checks also for extended clauses*)
+ | AExtended (bhvs, is_next, ext),
+ AExtended (bhvs', is_next', ext') ->
+ is_same_behavior_set bhvs bhvs' && is_next = is_next' &&
+ is_same_acsl_extension ext ext' env
| (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
| AAllocation _ | APragma _ | AExtended _), _ -> false
@@ -1550,9 +1550,8 @@ let rec gannot_correspondence =
ignore (logic_info_correspondence ~loc li empty_env)
| Dmodel_annot (mi,loc) ->
ignore (model_info_correspondence ~loc mi)
- | Dextended _ -> ()
-(* TODO: provide mechanism for extension themselves
- to give relevant information. *)
+ | Dextended _ -> () (* TODO: as for lemmas, we don't really have a structure
+ where to look for a matching extended annotation. *)
let global_correspondence g =
match g with
--
GitLab