diff --git a/src/plugins/wp/tests/test_config b/src/plugins/wp/tests/test_config index ebf3f27c26f9ec910cfdb25e281a6141d841198d..51675fdbc52d819cf3c99c4480b3130bd0fa64f3 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 82ac23797226aae576338c46106f95e16f40b717..f5f56f99251f2a4100444ab7bb74b0abc2128e07 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 59e26712f6995c7046c95bbf23a93f892c4c334e..807a50f5053ba69291bc3408ccd85bad69fb88a7 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 81b49ed20d473590181d159b37f404a4564e5395..fd0dd051a717b1544e9f13d4c0be5d06f2c410fa 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 65e8988e572951b8de7ff768207b7c4e88fdfa86..f41d80662719bdfed9a22dd9405c62bee91a106a 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 36003c91eeff9b752b08515c756f5e0268465e56..57d4ae071a433f4d3cecca0d8a218c0557f02e6d 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 544dae3b38c163cf97bf18d231031964ab6bc82e..8e908e8b69636dbd586fb832035975253a0cb13f 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 66c93e7d3a8fb3ec726efdd2efa913a36d46b1ba..baf66eaa6b7c65976cc5218477b20cb503d4d012 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 */