From a7f9cc56cbddddb9e39f9680925a650c5124f549 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Sat, 16 Jan 2021 13:23:53 +0100
Subject: [PATCH] [wp] fix loop contract ordering
---
src/plugins/wp/wpAnnot.ml | 26 +++++++++++++++++++-------
1 file changed, 19 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 3afb903f313..61871bf069d 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -203,24 +203,36 @@ type loop_contract = {
loop_assigns: WpPropId.assigns_full_info list;
}
-let get_loop_contract kf stmt =
+let reverse_loop_contract l = {
+ loop_established = List.rev l.loop_established ;
+ loop_invariants = List.rev l.loop_invariants ;
+ loop_preserved = List.rev l.loop_preserved ;
+ loop_assigns = List.rev l.loop_assigns ;
+}
+
+let get_loop_contract kf stmt : loop_contract =
let labels = NormAtLabels.labels_loop stmt in
let normalize_pred p = NormAtLabels.preproc_annot labels p in
let normalize_annot (i,p) = i, normalize_pred p in
let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
+ reverse_loop_contract @@
Annotations.fold_code_annot
begin fun _emitter ca l ->
match ca.annot_content with
| AInvariant(_,true,inv) ->
let p = normalize_pred inv.tp_statement in
- let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
let g_est = WpPropId.mk_loop_inv_id kf stmt ~established:true ca in
let g_ind = WpPropId.mk_loop_inv_id kf stmt ~established:false ca in
- { l with
- loop_established = (g_est,p) :: l.loop_established ;
- loop_invariants = (g_hyp,p) :: l.loop_invariants ;
- loop_preserved = (g_ind,p) :: l.loop_preserved ;
- }
+ if inv.tp_only_check then
+ { l with
+ loop_established = (g_est,p) :: l.loop_established ;
+ loop_preserved = (g_ind,p) :: l.loop_preserved }
+ else
+ let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
+ { l with
+ loop_established = (g_est,p) :: l.loop_established ;
+ loop_invariants = (g_hyp,p) :: l.loop_invariants ;
+ loop_preserved = (g_ind,p) :: l.loop_preserved }
| AVariant(term, None) ->
let vpos , vdec = WpStrategy.mk_variant_properties kf stmt ca term in
{ l with loop_preserved =
--
GitLab