From 30779d958b62a9bab455549bdcfcc8e01dedc934 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Feb 2021 14:44:57 +0100
Subject: [PATCH] [wp] Fixes formals scope
---
src/plugins/wp/cfgCalculus.ml | 29 ++++++++++++++---------------
1 file changed, 14 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 0b9f43b08d6..d2e8be2e49f 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -347,13 +347,6 @@ struct
if not (is_default_bhv mode) then []
else CfgAnnot.get_disjoint_behaviors kf
- let body env ~ensures ~exits w =
- let rw = List.fold_right (prove_property env) ensures w in
- let rk = List.fold_right (prove_property env) exits env.wk in
- Vhash.add env.wp env.cfg.return_point (Some rw) ;
- env.wk <- rk ;
- wp env env.cfg.entry_point
-
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
@@ -386,16 +379,22 @@ struct
(* frame-in *)
W.scope env.we xs SC_Frame_in @@
(* function body *)
- body env
- ~ensures:bhv.bhv_ensures
- ~exits:bhv.bhv_exits @@
+ begin fun w ->
+ Vhash.add env.wp env.cfg.return_point (Some w) ;
+ wp env env.cfg.entry_point
+ end @@
(* frame-out *)
- W.label env.we None Clabels.post @@
- (fun t ->
- if not has_exit then env.wk <- t
- else env.wk <- prove_assigns env bhv.bhv_exit_assigns t ;
- prove_assigns env bhv.bhv_post_assigns t) @@
W.scope env.we xs SC_Frame_out @@
+ (* Post-conds*)
+ W.label env.we None Clabels.post @@
+ begin fun w ->
+ env.wk <-
+ List.fold_right (prove_property env) bhv.bhv_exits @@
+ if not has_exit then w else prove_assigns env bhv.bhv_exit_assigns w ;
+
+ List.fold_right (prove_property env) bhv.bhv_ensures @@
+ prove_assigns env bhv.bhv_post_assigns w
+ end @@
(* wp-end *)
W.empty
--
GitLab