From 57271f4c7738a1a7ef01899ea8dbe85d5033b497 Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Tue, 29 Sep 2020 15:20:47 +0200 Subject: [PATCH] adds misc (cont.) --- tests/misc/add_assigns.i | 3 ++- tests/misc/bts0990_link.i | 2 +- tests/misc/bts1347.i | 1 + tests/misc/cpp-extra-args-per-file1.c | 2 +- tests/misc/global_decl_loc.i | 2 +- tests/misc/log_twice.i | 2 +- tests/misc/long_ident.c | 2 +- tests/misc/mergestruct2.i | 2 +- tests/misc/obfuscate.c | 2 +- tests/misc/pragma-pack.c | 2 +- tests/misc/visitor_creates_func_bts_1349.i | 2 +- tests/pdg/sets.c | 2 +- 12 files changed, 13 insertions(+), 11 deletions(-) diff --git a/tests/misc/add_assigns.i b/tests/misc/add_assigns.i index 8165be2e42b..d35203787a0 100644 --- a/tests/misc/add_assigns.i +++ b/tests/misc/add_assigns.i @@ -1,6 +1,7 @@ /* run.config +PLUGIN: report CMXS: @PTEST_NAME@ -OPT: -no-autoload-plugins -load-module report,@PTEST_DIR@/@PTEST_NAME@.cmxs -then -report -then -print +OPT: -load-module %{dep:@PTEST_NAME@.cmxs} -then -report -then -print */ /*@ assigns *x; */ diff --git a/tests/misc/bts0990_link.i b/tests/misc/bts0990_link.i index 188afa885fd..8558ed15a61 100644 --- a/tests/misc/bts0990_link.i +++ b/tests/misc/bts0990_link.i @@ -1,5 +1,5 @@ /* run.config - OPT: bts0990_link_1.i + OPT: %{dep:bts0990_link_1.i} */ // NB: This test is meant to return an error, as s is declared as an array in diff --git a/tests/misc/bts1347.i b/tests/misc/bts1347.i index 235b3db280d..9aa5ec357bb 100644 --- a/tests/misc/bts1347.i +++ b/tests/misc/bts1347.i @@ -1,4 +1,5 @@ /* run.config + PLUGIN: report CMXS: @PTEST_NAME@ OPT: @EVA_OPTIONS@ -load-module %{dep:@PTEST_NAME@.cmxs} -then -report */ diff --git a/tests/misc/cpp-extra-args-per-file1.c b/tests/misc/cpp-extra-args-per-file1.c index a1f58ee5494..1bc31a4d14c 100644 --- a/tests/misc/cpp-extra-args-per-file1.c +++ b/tests/misc/cpp-extra-args-per-file1.c @@ -1,5 +1,5 @@ /* run.config - OPT: -no-autoload-plugins -cpp-extra-args="-DGLOBAL" -cpp-extra-args-per-file @PTEST_DIR@/cpp-extra-args-per-file1.c:'-DFILE1 -DMACRO_WITH_QUOTES="\"hello world"\"',@PTEST_DIR@/cpp-extra-args-per-file2.c:"-DFILE2" -print -then @PTEST_DIR@/cpp-extra-args-per-file2.c -no-print + OPT: -cpp-extra-args="-DGLOBAL" -cpp-extra-args-per-file @PTEST_DIR@/cpp-extra-args-per-file1.c:'-DFILE1 -DMACRO_WITH_QUOTES="\"hello world"\"',@PTEST_DIR@/cpp-extra-args-per-file2.c:"-DFILE2" -print -then %{dep:cpp-extra-args-per-file2.c} -no-print */ #ifndef GLOBAL diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i index 779289768eb..704292f3104 100644 --- a/tests/misc/global_decl_loc.i +++ b/tests/misc/global_decl_loc.i @@ -1,5 +1,5 @@ /* run.config CMXS: global_decl_loc - OPT: @PTEST_DIR@/global_decl_loc2.i -no-autoload-plugins -load-module %{dep:@PTEST_NAME@.cmxs} + OPT: %{dep:global_decl_loc2.i} -load-module %{dep:@PTEST_NAME@.cmxs} */ int g; diff --git a/tests/misc/log_twice.i b/tests/misc/log_twice.i index 014cd7f075d..b4095c43f19 100644 --- a/tests/misc/log_twice.i +++ b/tests/misc/log_twice.i @@ -1,6 +1,6 @@ /* run.config CMXS: @PTEST_NAME@ - OPT: @EVA_CONFIG@ -load-module @PTEST_NAME@ + OPT: @EVA_CONFIG@ -load-module %{dep:@PTEST_NAME@.cmxs} */ int* f() { diff --git a/tests/misc/long_ident.c b/tests/misc/long_ident.c index e0ebb31439a..6e3ea10e4d9 100644 --- a/tests/misc/long_ident.c +++ b/tests/misc/long_ident.c @@ -1,7 +1,7 @@ /* run.config + PLUGIN: obfuscator OPT: -obfuscate -journal-disable */ - /*@ ensures \valid(q); // <-- obfuscation error [bts#404] */ int f(int *q) ; diff --git a/tests/misc/mergestruct2.i b/tests/misc/mergestruct2.i index 2a80dd274dc..10ab9882fda 100644 --- a/tests/misc/mergestruct2.i +++ b/tests/misc/mergestruct2.i @@ -1,5 +1,5 @@ /* run.config - OPT: -print -journal-disable mergestruct3.i mergestruct1.i + OPT: -print -journal-disable %{dep:mergestruct3.i} %{dep:mergestruct1.i} */ struct s *p; diff --git a/tests/misc/obfuscate.c b/tests/misc/obfuscate.c index f993479d0f7..2683da037cd 100644 --- a/tests/misc/obfuscate.c +++ b/tests/misc/obfuscate.c @@ -1,7 +1,7 @@ /* run.config + PLUGIN: obfuscator OPT: -obfuscate */ - int my_var = 0; /*@ global invariant I: my_var >= 0; */ diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c index 4d81f069887..4e930ec2580 100644 --- a/tests/misc/pragma-pack.c +++ b/tests/misc/pragma-pack.c @@ -1,9 +1,9 @@ /*run.config + DEPS: pragma-pack-utils.h STDOPT: #"-machdep gcc_x86_64 -kernel-msg-key typing:pragma" STDOPT: #"-cpp-command=\"gcc -E -C -I. -m32\" -cpp-frama-c-compliant" STDOPT: #"-machdep msvc_x86_64" */ - #include "pragma-pack-utils.h" #include <stdint.h> diff --git a/tests/misc/visitor_creates_func_bts_1349.i b/tests/misc/visitor_creates_func_bts_1349.i index 1ff0a2ebac6..21e906659f7 100644 --- a/tests/misc/visitor_creates_func_bts_1349.i +++ b/tests/misc/visitor_creates_func_bts_1349.i @@ -1,6 +1,6 @@ /* run.config CMXS: @PTEST_NAME@ - OPT: -load-script @PTEST_DIR@/@PTEST_NAME@ -then-on test -print + OPT: -load-script %{dep:@PTEST_NAME@.cmxs} -then-on test -print */ int a = 10; diff --git a/tests/pdg/sets.c b/tests/pdg/sets.c index 3bfb14466ce..7db13b002ea 100644 --- a/tests/pdg/sets.c +++ b/tests/pdg/sets.c @@ -1,6 +1,6 @@ /* run.config CMXS: @PTEST_NAME@ - STDOPT: +"-load-module @PTEST_NAME@ -lib-entry -main f -pdg -inout " + STDOPT: +"-load-module %{dep:@PTEST_NAME@.cmxs} -lib-entry -main f -pdg -inout " */ -- GitLab