From 6b199a8f0442fcaffd79e314304311a29204a8d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 9 Dec 2019 17:51:37 +0100
Subject: [PATCH] [wp/why3] fix context wrt tasks
---
src/plugins/wp/ProverWhy3.ml | 84 ++++++++++++++++++------------------
1 file changed, 41 insertions(+), 43 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index e3f3b6659e4..f18f8fc0509 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1311,50 +1311,48 @@ let is_trivial (t : Why3.Task.task) =
let build_proof_task ?timeout ?steplimit ~prover wpo () =
try
- WpContext.on_context (Wpo.get_context wpo)
- begin fun () ->
- (* Always generate common task *)
- let task = task_of_wpo wpo in
- if Wp_parameters.Check.get ()
- then Task.return VCS.checked (* Why3 tasks are type-checked *)
- else
- if Wp_parameters.Generate.get ()
- then Task.return VCS.no_result (* Only generate *)
- else
- let drv , config , task = prover_task prover task in
- if is_trivial task then
- Task.return VCS.valid
- else
- let mode = get_mode () in
- match mode with
- | NoCache ->
- call_prover ~timeout ~steplimit drv prover config task
- | Offline ->
- let hash = task_hash wpo drv prover task in
- let result = get_cache_result ~mode hash |> VCS.cached in
- if VCS.is_verdict result then incr hits else incr miss ;
+ (* Always generate common task *)
+ let context = Wpo.get_context wpo in
+ let task = WpContext.on_context context task_of_wpo wpo in
+ if Wp_parameters.Check.get ()
+ then Task.return VCS.checked (* Why3 tasks are type-checked *)
+ else
+ if Wp_parameters.Generate.get ()
+ then Task.return VCS.no_result (* Only generate *)
+ else
+ let drv , config , task = prover_task prover task in
+ if is_trivial task then
+ Task.return VCS.valid
+ else
+ let mode = get_mode () in
+ match mode with
+ | NoCache ->
+ call_prover ~timeout ~steplimit drv prover config task
+ | Offline ->
+ let hash = task_hash wpo drv prover task in
+ let result = get_cache_result ~mode hash |> VCS.cached in
+ if VCS.is_verdict result then incr hits else incr miss ;
+ Task.return result
+ | Update | Replay | Rebuild | Cleanup ->
+ let hash = task_hash wpo drv prover task in
+ let result =
+ get_cache_result ~mode hash
+ |> promote ~timeout ~steplimit |> VCS.cached in
+ if VCS.is_verdict result
+ then
+ begin
+ incr hits ;
Task.return result
- | Update | Replay | Rebuild | Cleanup ->
- let hash = task_hash wpo drv prover task in
- let result =
- get_cache_result ~mode hash
- |> promote ~timeout ~steplimit |> VCS.cached in
- if VCS.is_verdict result
- then
- begin
- incr hits ;
- Task.return result
- end
- else
- Task.finally
- (call_prover ~timeout ~steplimit drv prover config task)
- begin function
- | Task.Result result when VCS.is_verdict result ->
- incr miss ;
- set_cache_result ~mode hash prover result
- | _ -> ()
- end
- end ()
+ end
+ else
+ Task.finally
+ (call_prover ~timeout ~steplimit drv prover config task)
+ begin function
+ | Task.Result result when VCS.is_verdict result ->
+ incr miss ;
+ set_cache_result ~mode hash prover result
+ | _ -> ()
+ end
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
--
GitLab