Merge branch 'fix/wp/issue_745' into 'master'

Do not fail when using step limit option with a prover that does not support it

Closes #745

See merge request frama-c/frama-c!2823

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 ;

src/plugins/wp/tests/wp_plugin/no_step_limit.conf

+[main]
+default_editor = "editor %f"
+magic = 14
+memlimit = 1000
+running_provers_max = 2
+timelimit = 5
+
+[prover]
+command = "alt-ergo -timelimit %t %f"
+driver = "alt_ergo_2_2_0"
+in_place = false
+interactive = false
+name = "no-steps"

src/plugins/wp/tests/wp_plugin/no_step_limit.i

+/* run.config
+  DONTRUN:
+*/
+/* run.config_qualif
+  CMD: WHY3CONFIG=@PTEST_DIR@/@PTEST_NAME@.conf @frama-c@
+  OPT: -wp -wp-prover no-steps -wp-steps 10 -wp-msg-key shell
+*/
+/*@
+  lemma truc: \false ;
+*/

src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle

+# frama-c -wp -wp-steps 10 [...]
+[kernel] Parsing tests/wp_plugin/no_step_limit.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] Warning: no-steps  does not support steps limit (ignored option)
+[wp] [no-steps] Goal typed_lemma_truc : Unsuccess
+[wp] Proved goals:    0 / 1
+  no-steps:        0  (unsuccess: 1)