From 853f7a1a9b498da75c591a703963f0515e2a4d1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 2 Jun 2020 16:22:50 +0200
Subject: [PATCH] [wp] force more stepouts
---
src/plugins/wp/tests/wp_plugin/float_format.i | 4 ++--
src/plugins/wp/tests/wp_plugin/math.i | 4 ++--
.../tests/wp_plugin/oracle_qualif/float_format.1.res.oracle | 2 +-
.../tests/wp_plugin/oracle_qualif/float_format.2.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle | 2 +-
6 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/float_format.i b/src/plugins/wp/tests/wp_plugin/float_format.i
index cee1e6f724b..cdca1c6d758 100644
--- a/src/plugins/wp/tests/wp_plugin/float_format.i
+++ b/src/plugins/wp/tests/wp_plugin/float_format.i
@@ -1,7 +1,7 @@
/* run.config_qualif
OPT: -wp-prover native:coq
- OPT: -wp-prover native:alt-ergo -wp-steps 50 -wp-timeout 1
- OPT: -wp-prover alt-ergo -wp-steps 50 -wp-timeout 1
+ OPT: -wp-prover native:alt-ergo -wp-steps 5 -wp-timeout 100
+ OPT: -wp-prover alt-ergo -wp-steps 5 -wp-timeout 100
*/
//@ ensures KO: \result == 0.2 + x ;
diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i
index 3fece066d5a..160d94e7bee 100644
--- a/src/plugins/wp/tests/wp_plugin/math.i
+++ b/src/plugins/wp/tests/wp_plugin/math.i
@@ -5,8 +5,8 @@
/* run.config_qualif
OPT: -wp-prover alt-ergo -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
- OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 1 -wp-steps 50
- OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 1
+ OPT: -wp-prover alt-ergo -wp-prop=ko -wp-timeout 100 -wp-steps 10
+ OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report -wp-prop=ko -wp-timeout 100 -wp-steps 10
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index 2c38f952838..fd00d9ebd5b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 1 -wp-steps 50 [...]
+# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index 0d212aebf6a..5974584a73c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 1 -wp-steps 50 [...]
+# frama-c -wp -wp-timeout 100 -wp-steps 5 [...]
[kernel] Parsing tests/wp_plugin/float_format.i (no preprocessing)
[kernel:parser:decimal-float] tests/wp_plugin/float_format.i:10: Warning:
Floating-point constant 0.2 is not represented exactly. Will use 0x1.999999999999ap-3.
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
index b3a0b092a29..6dd9859b669 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 1 -wp-steps 50 [...]
+# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index f3f9a9692df..5b07b133292 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 1 [...]
+# frama-c -wp -wp-timeout 100 -wp-steps 10 [...]
[kernel] Parsing tests/wp_plugin/math.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
--
GitLab