From 7267399bc1175eefa94c5686abea8a59572a81dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 17 Sep 2019 10:54:52 +0200
Subject: [PATCH] [wp/debug] fix builtins dump
---
src/plugins/wp/register.ml | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 29f760ae9ee..a02ddbecf0e 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -748,14 +748,15 @@ let cmdline_run () =
RefUsage.compute ();
RefUsage.dump ();
end ;
- if Wp_parameters.has_dkey dkey_builtins then
- begin
- LogicBuiltins.dump ();
- end ;
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)
+ LogicBuiltins.dump ();
+ end ;
Generator.compute_selection computer ~fct ~bhv ~prop ()
in
match Wp_parameters.job () with
--
GitLab