diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml index 23fdfde5070f5eed16d67aeb1a4fb1a7230f7520..7c24fa9e7d9b2e6741d42ff775534390bc125ec5 100644 --- a/src/plugins/wp/ProofSession.ml +++ b/src/plugins/wp/ProofSession.ml @@ -50,7 +50,7 @@ let status wpo = try let f' = List.find Sys.file_exists (legacies wpo) in Wp_parameters.warning ~current:false - "Deprecated script for '%s'" wpo.po_sid ; + "Deprecated script for '%s' (use prover tip to upgrade)" wpo.po_sid ; Deprecated f' with Not_found -> NoScript in Hashtbl.add files f status ; status diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index 109e5141899b2d6cd96d18d673642fed92ed2c64..385a9ec8a93338844694aebefa923f94fc174c9c 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -868,9 +868,9 @@ let pp_wp_parameters fmt = then Format.pp_print_string fmt " -wp-no-prune" ; if Wp_parameters.Split.get () then Format.pp_print_string fmt " -wp-split" ; let tm = Wp_parameters.Timeout.get () in - if tm > 10 then Format.fprintf fmt " -wp-timeout %d" tm ; + if tm <> 10 then Format.fprintf fmt " -wp-timeout %d" tm ; let st = Wp_parameters.Steps.get () in - if tm > 10 then Format.fprintf fmt " -wp-steps %d" st ; + if st > 0 then Format.fprintf fmt " -wp-steps %d" st ; let dp = Wp_parameters.Depth.get () in if dp > 0 then Format.fprintf fmt " -wp-depth %d" dp ; if not (Kernel.SignedOverflow.get ()) then diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif index c71ba7beb2f0a9a659179ead3e41fb8094b15c93..08a997eaff90d308295a356aa0e4c320b5759bc9 100644 --- a/src/plugins/wp/tests/test_config_qualif +++ b/src/plugins/wp/tests/test_config_qualif @@ -1,3 +1,3 @@ -CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session @PTEST_FILE@ +CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session @PTEST_FILE@ LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json OPT: