From ddd1c41f2681a9266069b4de583e6356a85980e7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 May 2023 13:04:13 +0200
Subject: [PATCH] [wp] fix double assumes normalization
---
src/plugins/wp/cfgAnnot.ml | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 1e6485daec5..5eb9442a2b6 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -59,8 +59,7 @@ type behavior = {
let normalize_assumes h =
let module L = NormAtLabels in
- let labels = L.labels_fct_pre in
- L.preproc_annot labels h
+ L.preproc_annot L.labels_fct_pre h
let implies ?assumes p =
match assumes with None -> p | Some h -> Logic_const.pimplies (h,p)
@@ -77,7 +76,8 @@ let normalize_pre ~goal kf bhv ?assumes ip =
let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
let pre = ip.ip_content.tp_statement in
let assumes = Option.map normalize_assumes assumes in
- Some (id, L.preproc_annot labels @@ implies ?assumes pre)
+ let precond = L.preproc_annot labels pre in
+ Some (id, implies ?assumes precond)
else None
let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
@@ -87,8 +87,8 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
let assumes = Option.map (fun p -> normalize_assumes @@ at_pre p) assumes in
let labels = L.labels_fct_post ~exit:(tk=Exits) in
let id = WpPropId.mk_post_id kf Kglobal bhv (tk,ip) in
- let p = L.preproc_annot labels ip.ip_content.tp_statement in
- Some (id , implies ?assumes p)
+ let post = L.preproc_annot labels ip.ip_content.tp_statement in
+ Some (id , implies ?assumes post)
else None
let normalize_decreases (d, li) =
--
GitLab