From 1f8e73f204e2b1d80b7f87e2f6f74899d83db869 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 25 Jan 2021 09:42:38 +0100
Subject: [PATCH] [wp] filter empty scopes
---
src/plugins/wp/cfgCalculus.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 1142f94be4a..be0a373cd90 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -231,6 +231,7 @@ struct
match edge.edge_transition with
| Skip -> p
| Return(r,s) -> W.return env.we s r p
+ | Enter { blocals=[] } | Leave { blocals=[] } -> p
| Enter { blocals=xs } -> W.scope env.we xs SC_Block_in p
| Leave { blocals=xs } -> W.scope env.we xs SC_Block_out p
| Instr (i,s) -> instr env s i p
--
GitLab