From a65f17c7ff559b3f7bc33c17852902fdb765d044 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 11 Sep 2019 14:04:08 +0200
Subject: [PATCH] [wp/cache] change tests limits
---
src/plugins/wp/ProofSession.ml | 2 +-
src/plugins/wp/register.ml | 4 ++--
src/plugins/wp/tests/test_config_qualif | 2 +-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 23fdfde5070..7c24fa9e7d9 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 109e5141899..385a9ec8a93 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 c71ba7beb2f..08a997eaff9 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:
--
GitLab