From 35d6e2da2d13c098a2242e985600e5803af552ea Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 4 May 2021 08:48:32 +0200
Subject: [PATCH] [wp] Simpler pre normalization
---
src/plugins/wp/cfgAnnot.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index c2190cc487b..2629c793465 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -75,9 +75,9 @@ let normalize_pre ~goal kf bhv ?assumes ip =
let module L = NormAtLabels in
let labels = L.labels_fct_pre in
let id = WpPropId.mk_pre_id kf Kglobal bhv ip in
- let p = L.preproc_annot labels ip.ip_content.tp_statement in
+ let pre = ip.ip_content.tp_statement in
let assumes = Option.map normalize_assumes assumes in
- Some (id, implies ?assumes p)
+ Some (id, L.preproc_annot labels @@ implies ?assumes pre)
else None
let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
--
GitLab