From 4196809ae108270e73b9abc65acc34db9206b27b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 10 Sep 2019 15:19:50 +0200
Subject: [PATCH] [wp/cache] generate task for type-check
---
src/plugins/wp/ProverWhy3.ml | 19 ++++++++-----------
1 file changed, 8 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index c13cc803cce..3375e04b614 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1000,9 +1000,8 @@ let task_of_wpo wpo =
(* --- Prover Task --- *)
(* -------------------------------------------------------------------------- *)
-let prover_task prover wpo =
+let prover_task prover task =
let env = get_why3_env () in
- let task = task_of_wpo wpo in
let config = Why3Provers.config () in
let prover_config = Why3.Whyconf.get_prover_config config prover in
let drv = Why3.Whyconf.load_driver (Why3.Whyconf.get_main config)
@@ -1217,17 +1216,15 @@ let prove ?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 if Wp_parameters.Check.get ()
- then Task.return VCS.checked
- else Task.return VCS.no_result
+ then Task.return VCS.no_result (* Only generate *)
else
- let drv , config , task = prover_task prover wpo in
- if Wp_parameters.Check.get ()
- then
- (* Why3 typed checked the task during its build *)
- Task.return VCS.checked
- else
+ let drv , config , task = prover_task prover task in
if false && is_trivial task then
Task.return VCS.valid
else
--
GitLab