From d85df10533ddd6b187eb7eefcf09d6abb061eb01 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 9 Sep 2020 15:35:48 +0200
Subject: [PATCH] [wp] Ignore unsupported step limit
---
src/plugins/wp/ProverWhy3.ml | 20 ++++++++++++++++----
1 file changed, 16 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 2d9a6ce177b..244ed12a218 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1206,14 +1206,26 @@ let call_prover prover_config ~timeout ~steplimit drv prover task =
Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
Why3.Call_provers.limit_steps = Why3.Opt.get_def def.limit_time steps;
} in
- let command = Why3.Whyconf.get_complete_command prover_config
- ~with_steps:(steps<>None) in
+ let with_steps = match steps, prover_config.Why3.Whyconf.command_steps with
+ | None, _ -> false
+ | Some _, Some _ -> true
+ | Some _, None ->
+ Wp_parameters.warning ~once:true ~current:false
+ "%a does not support steps limit (ignored option)"
+ Why3.Whyconf.print_prover prover ;
+ false
+ in
+ let command = Why3.Whyconf.get_complete_command prover_config ~with_steps in
let call =
Why3.Driver.prove_task_prepared ~command ~limit drv task in
- Wp_parameters.debug ~dkey "Why3 run prover %a with %i timeout %i steps@."
+ let pp_steps fmt s =
+ if with_steps then Format.fprintf fmt "%i steps" (Why3.Opt.get_def (-1) s)
+ else Format.fprintf fmt ""
+ in
+ Wp_parameters.debug ~dkey "Why3 run prover %a with %i timeout %a@."
Why3.Whyconf.print_prover prover
(Why3.Opt.get_def (-1) timeout)
- (Why3.Opt.get_def (-1) steps);
+ pp_steps steps ;
let timeout = match timeout with None -> 0 | Some tlimit -> tlimit in
let pcall = {
call ; prover ;
--
GitLab