diff --git a/tests/cil/cpu_a.c b/tests/cil/cpu_a.c index cdcf2b854dff9f9ce226a0733ed091b20094d678..ceca6e498ad810bbb2c38d0bb3fbde00e419a0df 100644 --- a/tests/cil/cpu_a.c +++ b/tests/cil/cpu_a.c @@ -1,5 +1,5 @@ /* run.config - OPT: cpu_b.c -machdep x86_16 -print + OPT: %{dep:cpu_b.c} -machdep x86_16 -print */ typedef unsigned short DWORD ; diff --git a/tests/cil/merge.c b/tests/cil/merge.c index 6c20a48a3a7d09c4db4d4b942c7674e4ee7924b5..e8df7eb815b4a56967f5e2777be862fedd1f5e7d 100644 --- a/tests/cil/merge.c +++ b/tests/cil/merge.c @@ -1,4 +1,4 @@ /* run.config - OPT: merge2.c -print + OPT: %{dep:merge2.c} -print */ int x; diff --git a/tests/cil/merge2.c b/tests/cil/merge2.c index fa57eb5c8c0c4aa36f62bb9a0a03bbd43dc203a7..3fde680c426d2c7a1edc50c6646ad3d446c510f9 100644 --- a/tests/cil/merge2.c +++ b/tests/cil/merge2.c @@ -1,4 +1,4 @@ /* run.config - OPT: merge.c -print + OPT: %{dep:merge.c} -print */ int x =2; diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c index e4690c3aa39e85a66b1d11be0880117ae1c40e28..724ddbbe03acd7913008983a0e9b2253c12d5bab 100644 --- a/tests/idct/ieee_1180_1990.c +++ b/tests/idct/ieee_1180_1990.c @@ -1,6 +1,6 @@ /* run.config* GCC: - STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow idct.c -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" + STDOPT: +"-eva-msg-key=summary -load-module report,scope,variadic -float-normal -no-warn-signed-overflow %{dep:idct.c} -remove-redundant-alarms -eva-memexec -eva-builtin sqrt:Frama_C_sqrt,cos:Frama_C_cos -then -report -report-print-properties" */ /* IEEE_1180_1990: a testbed for IDCT accuracy * Copyright (C) 2001 Renaud Pacalet diff --git a/tests/spec/first.c b/tests/spec/first.c index 1aa3f9c6084e6d043f050f7fb7235a024832a9f9..cb2b53247eb91eb8b42980dcea8cae91a5264376 100644 --- a/tests/spec/first.c +++ b/tests/spec/first.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print third.c second.c -journal-disable + OPT: -print %{dep:third.c} %{dep:second.c} -journal-disable */ /*@ behavior b: requires \valid(first); diff --git a/tests/spec/merge_logic_globals_1.c b/tests/spec/merge_logic_globals_1.c index a8da203173372acc1cb00e21f0a41252b38ab551..ff35654fd72fd521a84cc9a0fab5abf7d080cdae 100644 --- a/tests/spec/merge_logic_globals_1.c +++ b/tests/spec/merge_logic_globals_1.c @@ -1,5 +1,6 @@ /* run.config -OPT: -print @PTEST_DIR@/merge_logic_globals_2.c -cpp-extra-args="-I@PTEST_DIR@" +DEPS: merge_logic_globals.h +OPT: -print %{dep:merge_logic_globals_2.c} -cpp-extra-args="-I@PTEST_DIR@" */ #include "merge_logic_globals.h" diff --git a/tests/spec/model1.c b/tests/spec/model1.c index 054e75ebadcf68e5a96b704488d59f88541fdd3d..9dc7cfbdabe3973a242dbe53570922f952c16a8c 100644 --- a/tests/spec/model1.c +++ b/tests/spec/model1.c @@ -1,7 +1,7 @@ /* run.config -STDOPT: +"model2.c" +DEPS: model1.h +STDOPT: +"%{dep:model2.c}" */ - #include "model1.h" void main () { diff --git a/tests/spec/multiple_decl_def_1.c b/tests/spec/multiple_decl_def_1.c index 3deb71b988c2549c826dc7913013620279d81a00..3ca910a501ec52c5b3edaec743c5bc15ab54d6fd 100644 --- a/tests/spec/multiple_decl_def_1.c +++ b/tests/spec/multiple_decl_def_1.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print multiple_decl_def_2.c -journal-disable + OPT: -print %{dep:multiple_decl_def_2.c} -journal-disable */ /* see bug #43 && #128 */ diff --git a/tests/spec/multiple_file_1.c b/tests/spec/multiple_file_1.c index 82bc735d3264bae96bc5f326d10d23a1b4f52b67..0f4879e8a5ee8c676e9eff8de7fddd3df135a9a5 100644 --- a/tests/spec/multiple_file_1.c +++ b/tests/spec/multiple_file_1.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print multiple_file_2.c -journal-disable + OPT: -print %{dep:multiple_file_2.c} -journal-disable */ /* see bug #43 */ diff --git a/tests/spec/multiple_include_2.c b/tests/spec/multiple_include_2.c index bf0d286ea0781033541d117eff77214cc495e39c..df671ee8502515edb72d1317290ce9406a22d992 100644 --- a/tests/spec/multiple_include_2.c +++ b/tests/spec/multiple_include_2.c @@ -1,7 +1,7 @@ /* run.config - OPT: -kernel-warn-key=annot-error=active -print multiple_include_1.c -journal-disable + DEPS: multiple_include.h + OPT: -kernel-warn-key=annot-error=active -print %{dep:multiple_include_1.c} -journal-disable */ #include "multiple_include.h" - /*@ requires p(x); */ void bar(int x) { i+=x; return; } diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c index 64b0e62aeec278a03dfd822ddc33e5f539566b1f..bbe04e56572f5d979c00b1cb85766b0db75b5f79 100644 --- a/tests/spec/preprocess.c +++ b/tests/spec/preprocess.c @@ -1,7 +1,7 @@ /* run.config + DEPS: preprocess.h OPT: -eva @EVA_CONFIG@ -journal-disable -print */ - // see bts 1357 #define assert(x) (x)?1:0 diff --git a/tests/spec/source_annot.c b/tests/spec/source_annot.c index ad85f6c8dc7eb874e30fe2478ca9a6dbbd8478ba..edcff9c183da817b31696f0783bbe8bbdcb2ab90 100644 --- a/tests/spec/source_annot.c +++ b/tests/spec/source_annot.c @@ -1,4 +1,5 @@ /* run.config + DEPS: prec_i.h DONTRUN: static local variables & specifications */ typedef int INTEGER; diff --git a/tests/spec/use.c b/tests/spec/use.c index 327496a599e5c107a8d38ca3b850ea6c9f2f647d..ed96fb0f9bc7487c112b1b01c5b82d191c5dddd1 100644 --- a/tests/spec/use.c +++ b/tests/spec/use.c @@ -1,5 +1,6 @@ /* run.config - STDOPT: +"use2.c" + DEPS: dec.h + STDOPT: +"%{dep:use2.c}" */ // BTS 0887 diff --git a/tests/spec/volatile.c b/tests/spec/volatile.c index 25dc52728ef08d36ab68636f53506b9aca33548c..6a07753368078aa1cceebf5eb72b933e4c628c4d 100644 --- a/tests/spec/volatile.c +++ b/tests/spec/volatile.c @@ -1,7 +1,7 @@ /* run.config - OPT: volatile_aux.c -print -copy + DEPS: volatile.h + OPT: %{dep:volatile_aux.c} -print -copy */ - #include "volatile.h" //@volatile x,y writes w ;