From 597df56fa81618a0703424d5adef050612308a8d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 6 Oct 2020 16:56:19 +0200
Subject: [PATCH] [wp] FIxes hypotheses computation for GUI
---
src/plugins/wp/GuiPanel.ml | 44 ++++++++++++++++++++++-----------
src/plugins/wp/MemoryContext.ml | 19 +++++++++++---
2 files changed, 45 insertions(+), 18 deletions(-)
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index d95fde6f349..4f29e2c3690 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/src/plugins/wp/GuiPanel.ml
@@ -63,32 +63,45 @@ let wp_rte_generated s =
not mem
else false
-let merge_scopes vcs =
- Bag.fold_left
- begin fun s vc ->
- match VC.get_scope vc with
- | WpContext.Global -> s
- | WpContext.Kf kf ->
- Kernel_function.Set.union (WpTarget.with_callees kf) s
- end
- Kernel_function.Set.empty vcs
-
-let warn_memory_context vcs =
+let with_model action kf =
let setup = Factory.parse (Wp_parameters.Model.get ()) in
let driver = Driver.load_driver () in
let model = Factory.instance setup driver in
let hypotheses_computer = WpContext.compute_hypotheses model in
let name = WpContext.MODEL.id model in
- Kernel_function.Set.iter
- (fun kf -> MemoryContext.warn kf name hypotheses_computer)
- (merge_scopes vcs)
+ action kf name hypotheses_computer
+
+let warn_memory_context kfs =
+ if Wp_parameters.MemoryContext.get () then begin
+ Kernel_function.Set.iter
+ (fun kf -> with_model MemoryContext.warn kf) kfs
+ end
+
+let populate_memory_context kfs =
+ if Wp_parameters.CheckModelHypotheses.get () then begin
+ Kernel_function.Set.iter
+ (fun kf -> with_model MemoryContext.add_behavior kf) kfs
+ end
let spawn provers vcs =
if not (Bag.is_empty vcs) then
let provers = Why3.Whyconf.Sprover.elements provers#get in
- warn_memory_context vcs ;
VC.command ~provers ~tip:true vcs
+let treat_hypotheses selection =
+ let kf = match selection with
+ | S_none -> None
+ | S_fun kf -> Some kf
+ | S_prop ip -> Property.get_kf ip
+ | S_call s -> Some (Kernel_function.find_englobing_kf s.s_stmt)
+ in
+ let kfs = match kf with
+ | Some kf -> WpTarget.with_callees kf
+ | None -> Kernel_function.Set.empty
+ in
+ warn_memory_context kfs ;
+ populate_memory_context kfs
+
let run_and_prove
(main:Design.main_window_extension_points)
(provers:GuiConfig.provers)
@@ -97,6 +110,7 @@ let run_and_prove
begin
try
begin
+ treat_hypotheses selection ;
match selection with
| S_none -> raise Stop
| S_fun kf -> spawn provers (VC.generate_kf kf)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index b325350326a..1f426154c17 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -390,7 +390,20 @@ let warn kf name hyp_computer =
let emitter =
Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
+module RegisteredHypotheses =
+ State_builder.Set_ref
+ (Cil_datatype.Kf.Set)
+ (struct
+ let name = "Wp.MemoryContext.RegisteredHypotheses"
+ let dependencies = [Ast.self]
+ end)
+
let add_behavior kf name hypotheses_computer =
- match get_behavior kf name hypotheses_computer with
- | None -> ()
- | Some bhv -> Annotations.add_behaviors emitter kf [bhv]
+ if RegisteredHypotheses.mem kf then ()
+ else begin
+ begin match get_behavior kf name hypotheses_computer with
+ | None -> ()
+ | Some bhv -> Annotations.add_behaviors emitter kf [bhv]
+ end ;
+ RegisteredHypotheses.add kf
+ end
--
GitLab