From 94f2f7cc842a058623a59740a549899eef37b11a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Feb 2021 15:27:40 +0100
Subject: [PATCH] [wp] Add default behavior when it is missing
---
src/plugins/wp/cfgGenerator.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 89109971805..9ee671a9729 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -78,9 +78,10 @@ let apply task ~kf ?bhvs ?prop () =
let bhvs = match bhvs with
| Some bhvs -> bhvs
| None ->
- match Annotations.behaviors kf with
- | [] -> [empty_default_behavior]
- | bhvs -> bhvs in
+ let bhvs = Annotations.behaviors kf in
+ if List.exists (Cil.is_default_behavior) bhvs then bhvs
+ else empty_default_behavior :: bhvs
+ in
let add_mode kf m =
let modes =
match KFmap.find_opt kf task.modes with
--
GitLab