From 8b39f0cdccbd0cce39c4ac703e519fcccf932e00 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 23 Mar 2020 18:10:52 +0100
Subject: [PATCH] [wp] fix scope of function body
---
src/plugins/wp/calculus.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index dec7620bbed..272f255fe7f 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -565,13 +565,17 @@ module Cfg (W : Mcfg.S) = struct
| Cil2cfg.VblkIn (Cil2cfg.Bfct, b) ->
let obj = get_only_succ env cfg v in
let obj = wp_scope wenv b.blocals Mcfg.SC_Block_in obj in
- wp_scope wenv formals Mcfg.SC_Function_frame obj
+ let obj = wp_scope wenv formals Mcfg.SC_Function_frame obj in
+ obj
+ | Cil2cfg.VblkOut (Cil2cfg.Bfct, b) ->
+ let obj = get_only_succ env cfg v in
+ let obj = wp_scope wenv b.blocals Mcfg.SC_Block_out obj in
+ obj
+ | Cil2cfg.VblkOut _ ->
+ get_only_succ env cfg v
| Cil2cfg.VblkIn (_, b) ->
let obj = get_only_succ env cfg v in
wp_scope wenv b.blocals Mcfg.SC_Block_in obj
- | Cil2cfg.VblkOut (_, _b) ->
- let obj = get_only_succ env cfg v in
- obj (* cf. blocks_closed_by_edge below *)
| Cil2cfg.Vstmt s ->
let obj = get_only_succ env cfg v in
wp_stmt wenv s obj
--
GitLab