Skip to content
Snippets Groups Projects
Commit a8f203f2 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix RTE generation

parent 7df8d089
No related branches found
No related tags found
No related merge requests found
......@@ -46,14 +46,17 @@ let empty () = {
(* -------------------------------------------------------------------------- *)
let get_kf_infos model kf ?bhv ?prop () =
if WpRTE.missing_guards model kf then
Wp_parameters.warning ~current:false ~once:true "Missing RTE guards"
else if Wp_parameters.RTE.get () then
let missing = WpRTE.missing_guards model kf in
if missing && Wp_parameters.RTE.get () then
WpRTE.generate model kf ;
let smoking =
Wp_parameters.SmokeTests.get () &&
Wp_parameters.SmokeDeadcode.get () in
CfgInfos.get kf ~smoking ?bhv ?prop ()
let infos = CfgInfos.get kf ~smoking ?bhv ?prop () in
(*TODO: print warning first *)
if missing then
Wp_parameters.warning ~current:false ~once:true "Missing RTE guards" ;
infos
let empty_default_behavior : funbehavior = {
b_name = Cil.default_behavior_name ;
......
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