From df31b5770c171161c2cac67a76a137f2fd7413be Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 12 Oct 2020 13:42:38 +0200
Subject: [PATCH] [wp] Request all RTE at startup when needed
---
src/plugins/wp/register.ml | 4 +++-
src/plugins/wp/wpRTE.ml | 3 +++
src/plugins/wp/wpRTE.mli | 3 +++
3 files changed, 9 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index a631bda083e..8e026f7bf04 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -748,8 +748,11 @@ let cmdline_run () =
if fct <> Wp_parameters.Fct_none then
begin
Wp_parameters.feedback ~ontty:`Feedback "Running WP plugin...";
+ let computer = computer () in
Ast.compute ();
Dyncall.compute ();
+ if Wp_parameters.RTE.get () then
+ WpRTE.generate_all computer#model ;
if Wp_parameters.has_dkey dkey_logicusage then
begin
LogicUsage.compute ();
@@ -763,7 +766,6 @@ let cmdline_run () =
let bhv = Wp_parameters.Behaviors.get () in
let prop = Wp_parameters.Properties.get () in
(** TODO entry point *)
- let computer = computer () in
if Wp_parameters.has_dkey dkey_builtins then
begin
WpContext.on_context (computer#model,WpContext.Global)
diff --git a/src/plugins/wp/wpRTE.ml b/src/plugins/wp/wpRTE.ml
index 74e6fdd198f..a6bc0690c67 100644
--- a/src/plugins/wp/wpRTE.ml
+++ b/src/plugins/wp/wpRTE.ml
@@ -102,6 +102,9 @@ let generate model kf =
List.iter (configure ~update ~generate:true kf cint) generator ;
if !update then !Db.RteGen.annotate_kf kf
+let generate_all model =
+ Wp_parameters.iter_kf (generate model)
+
let missing_guards model kf =
let update = ref false in
let cint = WpContext.on_context (model,WpContext.Kf kf) Cint.current () in
diff --git a/src/plugins/wp/wpRTE.mli b/src/plugins/wp/wpRTE.mli
index 53b0fc8eb4b..86ce77c668a 100644
--- a/src/plugins/wp/wpRTE.mli
+++ b/src/plugins/wp/wpRTE.mli
@@ -24,6 +24,9 @@
for the given function and model. *)
val generate : WpContext.model -> Kernel_function.t -> unit
+(** Invoke RTE on all selected functions *)
+val generate_all : WpContext.model -> unit
+
(** Returns [true] if RTE annotations should be generated for
the given function and model (and are not generated yet). *)
val missing_guards : WpContext.model -> Kernel_function.t -> bool
--
GitLab