From 1699baad4532e174d33b82cdd21dc7c8e3e45777 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 11 Sep 2020 14:53:57 +0200
Subject: [PATCH] [wp] ignore check loop when searching for dead annot
---
src/plugins/wp/wpReached.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index f2b7abc1387..b21fa463f9f 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -84,9 +84,9 @@ let is_dead_annot ca =
match ca.annot_content with
| APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
false && is_unrolled_completely spec
- | AAssert([],p) ->
+ | AAssert([],p)
+ | AInvariant([],_,p) ->
not p.tp_only_check && is_predicate false p.tp_statement
- | AInvariant([],_,p) -> is_predicate false p.tp_statement
| _ -> false
let is_dead_code stmt =
--
GitLab