From 338f50290448f60e38897b048f30f1608def378f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 27 Sep 2021 16:09:32 +0200
Subject: [PATCH] [wp] Do not reverse loop contracts
---
src/plugins/wp/cfgAnnot.ml | 10 ----------
1 file changed, 10 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 0f78e501ffe..af3c08ce96e 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -482,15 +482,6 @@ type loop_contract = {
loop_assigns: WpPropId.assigns_full_info list;
}
-let reverse_loop_contract l = {
- loop_terminates = l.loop_terminates ;
- 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 ;
- loop_smoke = List.rev l.loop_smoke ;
-}
-
let default_assigns stmt l =
{ l with
loop_assigns =
@@ -508,7 +499,6 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
let normalize_annot (i,p) = i, normalize_pred p in
let normalize_assigns w = NormAtLabels.preproc_assigns labels w in
default_assigns stmt @@
- reverse_loop_contract @@
Annotations.fold_code_annot
begin fun _emitter ca l ->
match ca.annot_content with
--
GitLab