From c2eecb042aaa23bbfdd0e41a59660ae50e44bf63 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 Feb 2021 17:44:09 +0100
Subject: [PATCH] [wp] revert formals allocation in pre
---
src/plugins/wp/cfgCalculus.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index d886bdacd26..fd907f9e54c 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -342,15 +342,16 @@ struct
let requires_init = if init then b.bhv_requires else [] in
(* pre-state *)
W.label env.we None Clabels.pre @@
- (* frame-in *)
- W.scope env.we formals SC_Frame_in @@
(* pre-conditions *)
List.fold_right (use_property env) (default_requires env.mode kf) @@
List.fold_right (use_property env) b.bhv_assumes @@
List.fold_right (prove_property env) requires_init @@
List.fold_right (use_property env) b.bhv_requires @@
List.fold_right (prove_property env) b.bhv_smokes @@
- List.fold_right (use_property env) side_behaviors w
+ List.fold_right (use_property env) side_behaviors @@
+ (* frame-in *)
+ W.scope env.we formals SC_Frame_in w
+
let do_post env ~formals (b : CfgAnnot.behavior) w =
W.scope env.we formals SC_Frame_out @@
--
GitLab