From e91f90a2002b663b6b92571cf5eeb157af9f81c9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 Feb 2021 19:11:02 +0100
Subject: [PATCH] [wp] fix spurius specs
---
src/plugins/wp/cfgInfos.ml | 15 ++++++++++-----
1 file changed, 10 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 69477a06938..e736dba02bd 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -104,10 +104,13 @@ let selected_requires ~prop (b : Cil_types.funbehavior) =
let selected_call ~bhv ~prop kf =
bhv = [] && List.exists (selected_requires ~prop) (Annotations.behaviors kf)
-let selected_disjoint_complete ~bhv ~prop =
+let selected_clause ~prop name getter kf =
+ getter kf <> [] && selected_name ~prop name
+
+let selected_disjoint_complete kf ~bhv ~prop =
selected_default ~bhv &&
- ( selected_name ~prop "@disjoint_behaviors" ||
- selected_name ~prop "@disjoint_behaviors" )
+ ( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
+ selected_clause ~prop "@disjoint_behaviors" Annotations.disjoint kf )
let selected_bhv ~bhv ~prop (b : Cil_types.funbehavior) =
(bhv = [] || List.mem b.b_name bhv) &&
@@ -189,8 +192,10 @@ let compile Key.{ kf ; bhv ; prop } =
let v0 = cfg.entry_point in
Vhash.add infos.unreachable v0 false ;
(* Spec Iteration *)
- if selected_disjoint_complete ~bhv ~prop ||
- List.exists (selected_bhv ~bhv ~prop) (Annotations.behaviors kf)
+ if selected_disjoint_complete kf ~bhv ~prop ||
+ List.exists
+ (selected_bhv ~bhv ~prop)
+ (Annotations.behaviors kf)
then infos.annots <- true ;
(* Stmt Iteration *)
Shash.iter
--
GitLab