From fae56db83d5ccc2e3c72c68e04c9ba92d76edfb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Feb 2021 12:20:41 +0100
Subject: [PATCH] [wp] warning for terminates
---
src/plugins/wp/cfgInfos.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index a6e1ad306a0..50ce82a8271 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -108,6 +108,14 @@ let selected_call ~bhv ~prop kf =
let selected_clause ~prop name getter kf =
getter kf <> [] && selected_name ~prop name
+let selected_terminates kf =
+ match Annotations.terminates kf with
+ | None -> ()
+ | Some ip ->
+ let loc = ip.ip_content.tp_statement.pred_loc in
+ Wp_parameters.warning ~source:(fst loc)
+ "Terminates not implemented yet (skipped)."
+
let selected_disjoint_complete kf ~bhv ~prop =
selected_default ~bhv &&
( selected_clause ~prop "@complete_behaviors" Annotations.complete kf ||
@@ -247,6 +255,7 @@ let compile Key.{ kf ; smoking ; bhv ; prop } =
Option.iter
begin fun (cfg : Cfg.automaton) ->
(* Spec Iteration *)
+ selected_terminates kf ;
if selected_disjoint_complete kf ~bhv ~prop ||
(List.exists (selected_bhv ~smoking ~bhv ~prop) behaviors)
then infos.annots <- true ;
--
GitLab