diff --git a/tests/jcdb/jbdb.c b/tests/jcdb/jbdb.c index d73218424429882a7b66ede7d3b67bb6c920f0d3..0180348922d95cc1d0a01879fe2819e718552c54 100644 --- a/tests/jcdb/jbdb.c +++ b/tests/jcdb/jbdb.c @@ -1,5 +1,5 @@ /* run.config -OPT: -json-compilation-database @PTEST_DIR@/build_commands.json -print +OPT: -json-compilation-database %{dep:@PTEST_DIR@/build_commands.json} -print */ int f2 () { diff --git a/tests/jcdb/jbdb2.c b/tests/jcdb/jbdb2.c index db89a97f607bda7804244e621acd67adbf107bd1..90ff3d399fe2690611dcec388ce0a79c9d4e3687 100644 --- a/tests/jcdb/jbdb2.c +++ b/tests/jcdb/jbdb2.c @@ -1,5 +1,5 @@ /* run.config -OPT: -json-compilation-database @PTEST_DIR@/build_commands.json -print +OPT: -json-compilation-database %{dep:@PTEST_DIR@/build_commands.json} -print */ int f1 () { diff --git a/tests/misc/audit.c b/tests/misc/audit.c index 40a9e6b9f1b3e13039be451f6027cd259e0c055e..f9111560e09ba541fdef93e09f563fc2b75d5707 100644 --- a/tests/misc/audit.c +++ b/tests/misc/audit.c @@ -1,7 +1,7 @@ /* run.config PLUGIN: @EVA_PLUGINS@ LOG: audit-out.json - STDOPT: #"-audit-check @PTEST_DIR@/audit-in.json -audit-prepare @PTEST_RESULT@/audit-out.json -kernel-warn-key audit=active" + STDOPT: #"-audit-check %{dep:@PTEST_DIR@/audit-in.json} -audit-prepare @PTEST_RESULT@/audit-out.json -kernel-warn-key audit=active" */ #include "audit_included.h" #include "audit_included_but_not_listed.h" diff --git a/tests/misc/bts0525-2.i b/tests/misc/bts0525-2.i index 6949e4d4d03de0004dab77e105a68ca5dda49772..f7d39a9f57803091070a53dfcdae4e6baaa27a7b 100644 --- a/tests/misc/bts0525-2.i +++ b/tests/misc/bts0525-2.i @@ -1,5 +1,5 @@ /* run.config - OPT: -typecheck @PTEST_DIR@/bts0525.i + OPT: -typecheck %{dep:@PTEST_DIR@/bts0525.i} */ typedef enum {E1=2, E2} T_EN1 ; diff --git a/tests/misc/bts0525.i b/tests/misc/bts0525.i index 3869382c8c01316e2b4b917cc2c7149a0ea87646..bfbff38d31f30ec505a543eaf9f799ff1294e20c 100644 --- a/tests/misc/bts0525.i +++ b/tests/misc/bts0525.i @@ -1,5 +1,5 @@ /* run.config - OPT: @PTEST_DIR@/bts0525-2.i + OPT: %{dep:@PTEST_DIR@/bts0525-2.i} */ typedef enum {E3=2, E4} T_EN2 ; typedef enum {E1=2, E2} T_EN1 ; diff --git a/tests/misc/bts0990_link.i b/tests/misc/bts0990_link.i index 667ab3eb1add0ca9eebd65c5f739e16ae75fc749..df2e45884e74332e8003a84b8cc3a784d0f2aa5e 100644 --- a/tests/misc/bts0990_link.i +++ b/tests/misc/bts0990_link.i @@ -3,7 +3,7 @@ OPT: %{dep:@PTEST_DIR@/bts0990_link_1.i} */ // NB: This test is meant to return an error, as s is declared as an array in -// @PTEST_DIR@/bts0990_link_1.i +// %{dep:@PTEST_DIR@/bts0990_link_1.i} char *s; diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i index 46a2d3bb568d4de20543ce39eed1043264de1101..77ea1dfabb166e240936c70641fe093b769db756 100644 --- a/tests/misc/global_decl_loc2.i +++ b/tests/misc/global_decl_loc2.i @@ -1,8 +1,8 @@ /* run.config* COMMENT: with dune, the LIBS directive must be replaced by a MODULE directive (see also ./test_config file) + LIBS: global_decl_loc - DEPS: @PTEST_DIR@/global_decl_loc.i - OPT: @PTEST_DIR@/global_decl_loc.i + OPT: %{dep:@PTEST_DIR@/global_decl_loc.i} */ extern int g; diff --git a/tests/misc/mergestruct3.i b/tests/misc/mergestruct3.i index ecc825733c72bf679555e4ff0ea258493179c930..3a8943a8d8f8a892ad78f6c89deab5c7cfca55d9 100644 --- a/tests/misc/mergestruct3.i +++ b/tests/misc/mergestruct3.i @@ -1,6 +1,6 @@ /* run.config - OPT: -print @PTEST_DIR@/mergestruct1.i @PTEST_DIR@/mergestruct2.i - OPT: -print @PTEST_DIR@/mergestruct2.i @PTEST_DIR@/mergestruct1.i + OPT: -print %{dep:@PTEST_DIR@/mergestruct1.i} %{dep:@PTEST_DIR@/mergestruct2.i} + OPT: -print %{dep:@PTEST_DIR@/mergestruct2.i} %{dep:@PTEST_DIR@/mergestruct1.i} */ struct s { float a; } s2; diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json index cacd9f1deac9573453ddd26f1d5a2b18c478aebb..7d27051ffcff51321c18805e28cfc5a392ad16ec 100644 --- a/tests/misc/oracle/audit-out.json +++ b/tests/misc/oracle/audit-out.json @@ -71,7 +71,7 @@ } }, "sources": { - "tests/misc/audit.c": "f94ce1c8f5e5911260931783495e2c88", + "tests/misc/audit.c": "849a5c434063ac353bc07ba7e8ca7109", "tests/misc/audit_included.h": "c2cc488143a476f69cf2ed04c3439e6e", "tests/misc/audit_included_but_not_listed.h": "c2cc488143a476f69cf2ed04c3439e6e" diff --git a/tests/misc/oracle/audit.res.oracle b/tests/misc/oracle/audit.res.oracle index 59fb1e210c6a0f1e678b471f0fe48402d763f4ba..040c0629cdf7834af8207a62ba3d96e361136a7b 100644 --- a/tests/misc/oracle/audit.res.oracle +++ b/tests/misc/oracle/audit.res.oracle @@ -1,5 +1,5 @@ [kernel:audit] Warning: - different hashes for tests/misc/audit.c: got f94ce1c8f5e5911260931783495e2c88, expected 01010101010101010101010101010101 + different hashes for tests/misc/audit.c: got 849a5c434063ac353bc07ba7e8ca7109, expected 01010101010101010101010101010101 [kernel:audit] Warning: different hashes for tests/misc/audit_included_but_not_listed.h: got c2cc488143a476f69cf2ed04c3439e6e, expected <none> (not in list) [kernel:audit] Warning: diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c index 6101341838697f0bb957216bd1d532fa31e9fc68..9a6998b45669fd11ade75b2fd03ebebfc3d86545 100644 --- a/tests/saveload/bool.c +++ b/tests/saveload/bool.c @@ -1,5 +1,5 @@ /* run.config - EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save @PTEST_RESULT@/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ @PTEST_DIR@/bool.c > @PTEST_RESULT@/bool_sav.res 2> @PTEST_RESULT@/bool_sav.err + EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save @PTEST_RESULT@/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ %{dep:@PTEST_DIR@/bool.c} > @PTEST_RESULT@/bool_sav.res 2> @PTEST_RESULT@/bool_sav.err STDOPT: +"-load @PTEST_RESULT@/bool.sav -out -input -deps" STDOPT: +"-load @PTEST_RESULT@/bool.sav -eva @EVA_OPTIONS@" */ diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i index 31080cb964bc2de06d93c43bd6e278a695cd7666..8abbddfbc06147fbb8d6a6d8c31094cca00061bc 100644 --- a/tests/saveload/callbacks.i +++ b/tests/saveload/callbacks.i @@ -1,5 +1,5 @@ /* run.config - EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ @PTEST_DIR@/callbacks.i -out -calldeps -eva-show-progress -main main1 -save @PTEST_RESULT@/callbacks.sav > @PTEST_RESULT@/callbacks_initial.res 2> @PTEST_RESULT@/callbacks_initial.err + EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ %{dep:@PTEST_DIR@/callbacks.i} -out -calldeps -eva-show-progress -main main1 -save @PTEST_RESULT@/callbacks.sav > @PTEST_RESULT@/callbacks_initial.res 2> @PTEST_RESULT@/callbacks_initial.err STDOPT: +"-load @PTEST_RESULT@/callbacks.sav -main main2 -then -main main3" */ diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c index 26c3f18e1fc8a7c0627f9dcc29bfc678ddb0b2d4..514aaedef34ed26e9a8de8360f9784163103918c 100644 --- a/tests/saveload/isset.c +++ b/tests/saveload/isset.c @@ -1,5 +1,5 @@ /* run.config - EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_RESULT@/isset.sav @PTEST_DIR@/isset.c > @PTEST_RESULT@/isset_sav.res 2> @PTEST_RESULT@/isset_sav.err + EXECNOW: LOG isset_sav.res LOG isset_sav.err BIN isset.sav @frama-c@ -quiet -eva @EVA_OPTIONS@ -save @PTEST_RESULT@/isset.sav %{dep:@PTEST_DIR@/isset.c} > @PTEST_RESULT@/isset_sav.res 2> @PTEST_RESULT@/isset_sav.err STDOPT: +"-quiet -load @PTEST_RESULT@/isset.sav" STDOPT: +"-load @PTEST_RESULT@/isset.sav" STDOPT: +"-eva @EVA_OPTIONS@ -load @PTEST_RESULT@/isset.sav" diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i index 31038cd694580d3273716dcd1e44736f2970aa30..0ff25f71380a217a5bd7032c501ec64dc99a31f7 100644 --- a/tests/saveload/sparecode.i +++ b/tests/saveload/sparecode.i @@ -1,6 +1,6 @@ /* run.config PLUGIN: @EVA_PLUGINS@ slicing - EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save @PTEST_RESULT@/sparecode.sav @PTEST_DIR@/sparecode.i -then-on 'Slicing export' -print > @PTEST_RESULT@/sparecode_sav.res 2> @PTEST_RESULT@/sparecode_sav.err + EXECNOW: BIN sparecode.sav LOG sparecode_sav.res LOG sparecode_sav.err @frama-c@ -slicing-level 2 -slice-return main -eva-show-progress -save @PTEST_RESULT@/sparecode.sav %{dep:@PTEST_DIR@/sparecode.i} -then-on 'Slicing export' -print > @PTEST_RESULT@/sparecode_sav.res 2> @PTEST_RESULT@/sparecode_sav.err STDOPT: +"-load @PTEST_RESULT@/sparecode.sav" */ int G; diff --git a/tests/scope/bts383.c b/tests/scope/bts383.c index 5014bf4e04504b965daec5f1c06c025a3b91a6f4..580c77decc059486c564a436fe0f26465e3744b5 100644 --- a/tests/scope/bts383.c +++ b/tests/scope/bts383.c @@ -1,13 +1,13 @@ /* run.config OPT: -eva @EVA_CONFIG@ -print -scope-verbose 1 -eva-remove-redundant-alarms -eva-context-width 3 */ -/* +/* echo '!Db.Scope.check_asserts();;' \ - | bin/toplevel.top -eva @PTEST_DIR@/bts383.c + | bin/toplevel.top -eva bts383.c */ int v; void if1 (int * p) { - if (*p > 0) + if (*p > 0) v = *p; } int if2 (int c, int * p) { diff --git a/tests/spec/first.c b/tests/spec/first.c index d0a021fbefb80deb01d75b8f8b5cf12bbb6c9ca3..4578e7d6f984cfaa7abb9a1cee5707b6049fa6e0 100644 --- a/tests/spec/first.c +++ b/tests/spec/first.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print @PTEST_DIR@/third.c @PTEST_DIR@/second.c + OPT: -print %{dep:@PTEST_DIR@/third.c} %{dep:@PTEST_DIR@/second.c} */ /*@ behavior b: requires \valid(first); diff --git a/tests/spec/model2.c b/tests/spec/model2.c index c079e4fafb9f6e0274b07b1c10b82e9b878fb571..dc4f5691904734059de7b2c53d69ee9b4321202b 100644 --- a/tests/spec/model2.c +++ b/tests/spec/model2.c @@ -1,5 +1,5 @@ /* run.config -DONTRUN: main test is in @PTEST_DIR@/model1.c +DONTRUN: main test is in %{dep:@PTEST_DIR@/model1.c} */ #include "model1.h" diff --git a/tests/spec/multi_axiomatic_1.i b/tests/spec/multi_axiomatic_1.i index cfe295495cc769ee756d766794a22dc1902790ea..0687661447a6ad579c257d193727dc636d90bea6 100644 --- a/tests/spec/multi_axiomatic_1.i +++ b/tests/spec/multi_axiomatic_1.i @@ -1,5 +1,5 @@ /* run.config -OPT: @PTEST_DIR@/multi_axiomatic_2.i -print +OPT: %{dep:@PTEST_DIR@/multi_axiomatic_2.i} -print */ /*@ diff --git a/tests/spec/multi_axiomatic_2.i b/tests/spec/multi_axiomatic_2.i index d1d8f406ec9815894239b8f8a544798b08e0b894..2d99bea95e3e95d69959df8a159d8999c3d095be 100644 --- a/tests/spec/multi_axiomatic_2.i +++ b/tests/spec/multi_axiomatic_2.i @@ -1,5 +1,5 @@ /* run.config -DONTRUN: main configuration in @PTEST_DIR@/multi_axiomatic_1.i +DONTRUN: main configuration in %{dep:@PTEST_DIR@/multi_axiomatic_1.i} */ /*@ axiomatic ax { logic int Acc(int m); } diff --git a/tests/spec/multiple_decl_def_1.c b/tests/spec/multiple_decl_def_1.c index 02ca904b8ceeda28a0dc91e1eae925b884fc6f4e..936d427c415a4059975cb0c244298d35f3024a22 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 @PTEST_DIR@/multiple_decl_def_2.c + OPT: -print %{dep:@PTEST_DIR@/multiple_decl_def_2.c} */ /* see bug #43 && #128 */ diff --git a/tests/spec/multiple_file_1.c b/tests/spec/multiple_file_1.c index f31326e8aea1df3e8be3c0d6f7b0751623258f9a..63dc0cab6214d17b5231ee092fca59c9f4056c7c 100644 --- a/tests/spec/multiple_file_1.c +++ b/tests/spec/multiple_file_1.c @@ -1,5 +1,5 @@ /* run.config - OPT: -print @PTEST_DIR@/multiple_file_2.c + OPT: -print %{dep:@PTEST_DIR@/multiple_file_2.c} */ /* see bug #43 */ diff --git a/tests/syntax/merge_inline_1.c b/tests/syntax/merge_inline_1.c index 325b55a258c7a1b113a0f03752435b801c6826e0..ec465fac50903da73ae1f0e6cb88d9cfe5e75541 100644 --- a/tests/syntax/merge_inline_1.c +++ b/tests/syntax/merge_inline_1.c @@ -1,5 +1,5 @@ /* run.config -OPT: @PTEST_DIR@/merge_inline_2.c -aggressive-merging -print +OPT: %{dep:@PTEST_DIR@/merge_inline_2.c} -aggressive-merging -print */ /* Test that we rename properly inlines even if they have prototypes and diff --git a/tests/syntax/typedef_multi_2.c b/tests/syntax/typedef_multi_2.c index 3dfefa3de8e7f251465b75053d6ab37da8bb9947..24bbeae93e5a08033e732d1dd1948b38c0fdbc0d 100644 --- a/tests/syntax/typedef_multi_2.c +++ b/tests/syntax/typedef_multi_2.c @@ -1,5 +1,5 @@ /* run.config -DONTRUN: main test is at @PTEST_DIR@/typedef_multi_1.c +DONTRUN: main test is at %{dep:@PTEST_DIR@/typedef_multi_1.c} */ #include "typedef_multi.h"