Skip to content
Snippets Groups Projects
Commit f62cdd0b authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Warn on missing RTE guards

parent d405e0dd
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment