From f0c4778f9d154764a35d816f7f184cf3b6d2bdb9 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 17 Sep 2024 16:11:55 +0200
Subject: [PATCH] [wp] push timeouts for a few tests

---
 .../wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle     | 2 +-
 src/plugins/wp/tests/wp_acsl/simpl_is_type.i                    | 2 +-
 .../wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle      | 2 +-
 src/plugins/wp/tests/wp_typed/user_init.i                       | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
index 32a5ec5a2b6..6ed08cfe5dd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-timeout 3 [...]
 [kernel] Parsing simpl_is_type.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] [Valid] Goal check_acsl_exits (Cfg) (Unreachable)
diff --git a/src/plugins/wp/tests/wp_acsl/simpl_is_type.i b/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
index 965fe5928e6..ad3c91098eb 100644
--- a/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
+++ b/src/plugins/wp/tests/wp_acsl/simpl_is_type.i
@@ -3,7 +3,7 @@
 */
 
 /* run.config_qualif
-   OPT: -wp-simplify-is-cint -wp-prop=-ko,-lack
+   OPT: -wp-simplify-is-cint -wp-prop=-ko,-lack -wp-timeout 3
 */
 
 /** Tests the simplification of (forall x:int. P) into (forall
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index c9dc833ca04..3299adf20a9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp [...]
+# frama-c -wp -wp-timeout 4 [...]
 [kernel] Parsing user_init.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] [Valid] Goal init_exits (Cfg) (Unreachable)
diff --git a/src/plugins/wp/tests/wp_typed/user_init.i b/src/plugins/wp/tests/wp_typed/user_init.i
index aed34f4502d..37891a304ee 100644
--- a/src/plugins/wp/tests/wp_typed/user_init.i
+++ b/src/plugins/wp/tests/wp_typed/user_init.i
@@ -1,6 +1,6 @@
 /* run.config_qualif
 
-   OPT: -wp-prop=-lack,-tactic
+   OPT: -wp-prop=-lack,-tactic -wp-timeout 4
    OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,Alt-Ergo -wp-script dry
    OPT: -wp-prop=lack
  */
-- 
GitLab