From f62cdd0b9901806f0460021170c80e4e42f27c2d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jan 2021 14:46:53 +0100
Subject: [PATCH] [wp] Warn on missing RTE guards
---
src/plugins/wp/cfgGenerator.ml | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index 8c109303a4d..2276eb131fd 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -187,6 +187,8 @@ struct
WpContext.on_context (model,WpContext.Kf mode.kf)
begin fun () ->
LogicUsage.iter_lemmas VCG.register_lemma ;
+ if WpRTE.missing_guards model mode.kf then
+ warning ~current:false ~once:true "Missing RTE guards" ;
let bhv =
if Cil.is_default_behavior mode.bhv then None
else Some mode.bhv.b_name in
--
GitLab