From 36104e935eb38f231ae36415797d610b1f80b89f 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:29:40 +0100
Subject: [PATCH] [wp] fix duplicated block in
---
src/plugins/wp/calculus.ml | 5 +----
src/plugins/wp/cil2cfg.ml | 6 +++++-
2 files changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 272f255fe7f..2f3c5e7e07f 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -571,11 +571,8 @@ module Cfg (W : Mcfg.S) = struct
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 _ ->
+ | Cil2cfg.VblkOut _ | Cil2cfg.VblkIn _ ->
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.Vstmt s ->
let obj = get_only_succ env cfg v in
wp_stmt wenv s obj
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index 8a8402eb871..0afef00829b 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -653,7 +653,11 @@ let block_scope_for_edge cfg e =
| None -> no_scope
| Some s' -> block_scope s s'
end
- | _ -> (* TODO ? *) no_scope
+ | VblkIn(Bstmt _,b) -> { b_opened=[b] ; b_closed=[] }
+ | Vcall _
+ | VblkIn _ | VblkOut _ | Vtest(false,_,_)
+ | VfctIn | VfctOut | Vstart | Vend | Vexit | Vloop2 _ ->
+ no_scope
let has_exit cfg =
try
--
GitLab