From 090f1338dffbe34daf2ec898f3280b1ed9dadeeb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 22 Oct 2019 23:49:40 +0200
Subject: [PATCH] [wp/why3] delayed task building and error report
---
src/plugins/wp/ProverWhy3.ml | 15 +++--
.../tests/wp_bts/oracle/bts_2110.res.oracle | 24 ++++----
.../tests/wp_plugin/oracle/model.res.oracle | 60 +++++++++----------
3 files changed, 52 insertions(+), 47 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 195645368a1..5226caf506d 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1269,7 +1269,7 @@ let is_trivial (t : Why3.Task.task) =
(* --- Prove WPO --- *)
(* -------------------------------------------------------------------------- *)
-let prove ?timeout ?steplimit ~prover wpo =
+let build_proof_task ?timeout ?steplimit ~prover wpo () =
try
WpContext.on_context (Wpo.get_context wpo)
begin fun () ->
@@ -1316,9 +1316,14 @@ let prove ?timeout ?steplimit ~prover wpo =
end
end ()
with exn ->
- let bt = Printexc.get_raw_backtrace () in
- Wp_parameters.fatal "Error in why3:%a@.%s@."
- Why3.Exn_printer.exn_printer exn
- (Printexc.raw_backtrace_to_string bt)
+ if Wp_parameters.has_dkey dkey_api then
+ Wp_parameters.fatal "[Why3 Error] %a@\n%s"
+ Why3.Exn_printer.exn_printer exn
+ Printexc.(raw_backtrace_to_string @@ get_raw_backtrace ())
+ else
+ Task.failed "[Why3 Error] %a" Why3.Exn_printer.exn_printer exn
+
+let prove ?timeout ?steplimit ~prover wpo =
+ Task.later (build_proof_task ?timeout ?steplimit ~prover wpo) ()
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
index 54d45f3925f..632e1429bf1 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts_2110.res.oracle
@@ -96,16 +96,16 @@ end
(* use frama_c_wp.memory.Memory *)
- (* use S2_A *)
-
(* use Compound *)
goal wp_goal :
- forall t:addr -> int, t1:addr -> int, a:addr, a1:addr.
- let a2 = Load_S2_A a t in
- let a3 = Load_S2_A a (havoc t1 t a 1) in
+ forall t:int -> int, t1:addr -> int, a:addr, a1:addr, i:int.
+ let a2 = shiftfield_F1_FD_pos a1 in
+ let x = get t1 a2 in
+ not x = i ->
region (base a1) <= 0 ->
- region (base a) <= 0 -> IsS2_A a2 -> IsS2_A a3 -> EqS2_A a3 a2
+ region (base a) <= 0 ->
+ linked t -> is_sint32 i -> is_sint32 x -> not invalid t a2 1 -> a2 = a
end
[wp:print-generated]
theory WP1
@@ -125,15 +125,15 @@ end
(* use frama_c_wp.memory.Memory *)
+ (* use S2_A *)
+
(* use Compound *)
goal wp_goal :
- forall t:int -> int, t1:addr -> int, a:addr, a1:addr, i:int.
- let a2 = shiftfield_F1_FD_pos a1 in
- let x = get t1 a2 in
- not x = i ->
+ forall t:addr -> int, t1:addr -> int, a:addr, a1:addr.
+ let a2 = Load_S2_A a t in
+ let a3 = Load_S2_A a (havoc t1 t a 1) in
region (base a1) <= 0 ->
- region (base a) <= 0 ->
- linked t -> is_sint32 i -> is_sint32 x -> not invalid t a2 1 -> a2 = a
+ region (base a) <= 0 -> IsS2_A a2 -> IsS2_A a3 -> EqS2_A a3 a2
end
[wp] 2 goals generated
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 32436320567..55375f62ab7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -94,35 +94,6 @@ Prove: P_P(x).
------------------------------------------------------------
[wp] Running WP plugin...
[wp] 2 goals scheduled
-[wp:print-generated]
- theory WP1
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use frama_c_wp.memory.Memory *)
-
- (* use frama_c_wp.cint.Cint *)
-
- (* use Compound *)
-
- (* use Axiomatic *)
-
- goal wp_goal :
- forall t:addr -> int, i:int, a:addr.
- let x = get t (shift_sint32 a i) in
- region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
- end
---------------------------------------------
--- Context 'typed_ref_f' Cluster 'Compound'
---------------------------------------------
@@ -166,7 +137,7 @@ theory Axiomatic1
predicate P_P1 int
end
[wp:print-generated]
- theory WP2
+ theory WP1
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool1 *)
@@ -194,6 +165,35 @@ end
let x = get1 t (shift_sint321 a i) in
region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
end
+[wp:print-generated]
+ theory WP2
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ (* use Compound *)
+
+ (* use Axiomatic *)
+
+ goal wp_goal :
+ forall t:addr -> int, i:int, a:addr.
+ let x = get t (shift_sint32 a i) in
+ region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
+ end
[wp] 2 goals generated
------------------------------------------------------------
Function f
--
GitLab