From a2b3799c9b501e2e49e3dd29cf479d4f02a84a0a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 29 Sep 2020 10:53:50 +0200
Subject: [PATCH] [wp] Inactive pedantic-assigns in tests
---
src/plugins/wp/tests/test_config | 2 +-
src/plugins/wp/tests/test_config_qualif | 2 +-
src/plugins/wp/tests/wp_bts/bts_2110.i | 2 +-
src/plugins/wp/tests/wp_plugin/model.i | 2 +-
src/plugins/wp/tests/wp_plugin/rte.i | 2 +-
src/plugins/wp/tests/wp_region/test_config | 2 +-
src/plugins/wp/tests/wp_usage/save_load.i | 4 ++--
tests/spec/generalized_check.i | 2 +-
8 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config
index ebf3f27c26f..51675fdbc52 100644
--- a/src/plugins/wp/tests/test_config
+++ b/src/plugins/wp/tests/test_config
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-prover none -wp-print -wp-share ./share -wp-msg-key shell -wp-warn-key "pedantic-assigns=inactive"
OPT:
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 82ac2379722..f5f56f99251 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
OPT:
diff --git a/src/plugins/wp/tests/wp_bts/bts_2110.i b/src/plugins/wp/tests/wp_bts/bts_2110.i
index 59e26712f69..807a50f5053 100644
--- a/src/plugins/wp/tests/wp_bts/bts_2110.i
+++ b/src/plugins/wp/tests/wp_bts/bts_2110.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen -wp-share ./share
+ CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen -wp-share ./share -wp-warn-key "pedantic-assigns=inactive"
OPT:
*/
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 81b49ed20d4..fd0dd051a71 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell,print-generated -wp-prover why3
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell,print-generated -wp-prover why3 -wp-warn-key "pedantic-assigns=inactive"
OPT: -wp-model Typed -wp -wp-gen -wp-print -then -wp-model Typed+ref -wp -wp-gen -wp-print
*/
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index 65e8988e572..f41d8066271 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-prover none -wp-share ./share -wp-msg-key shell -wp-msg-key rte
+ CMD: @frama-c@ -wp -wp-prover none -wp-share ./share -wp-msg-key shell,rte -wp-warn-key "pedantic-assigns=inactive"
OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
index 36003c91eef..57d4ae071a4 100644
--- a/src/plugins/wp/tests/wp_region/test_config
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -1,3 +1,3 @@
CMD: @frama-c@ -no-autoload-plugins -load-module wp
LOG: @PTEST_NAME@/region/job.dot
-OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
+OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job
diff --git a/src/plugins/wp/tests/wp_usage/save_load.i b/src/plugins/wp/tests/wp_usage/save_load.i
index 544dae3b38c..8e908e8b696 100644
--- a/src/plugins/wp/tests/wp_usage/save_load.i
+++ b/src/plugins/wp/tests/wp_usage/save_load.i
@@ -1,6 +1,6 @@
/* run.config
- EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav
+ EXECNOW: LOG save_load.sav.res LOG save_load.sav.err BIN @PTEST_NAME@.sav @frama-c@ -no-autoload-plugins -load-module wp -wp-warn-key pedantic-assigns=inactive -wp-share ./share -wp -wp-print -wp-prover none @PTEST_FILE@ -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@.sav.err
+ CMD: @frama-c@ -no-autoload-plugins -load-module wp -load @PTEST_DIR@/@PTEST_NAME@.sav -wp-warn-key pedantic-assigns=inactive
OPT: -print
OPT: -wp -wp-prover none -wp-print
*/
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 66c93e7d3a8..baf66eaa6b7 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key shell
+OPT: -wp -wp-prover qed -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
OPT: -eva -eva-use-spec f
OPT: -print
*/
--
GitLab