diff --git a/ptests/ptests.ml b/ptests/ptests.ml index 23858ad857bdc100449fb4c8c27b09cbc2e97e86..3f7dfbc94960eaa3d214dd8b109b6c7c7129562a 100644 --- a/ptests/ptests.ml +++ b/ptests/ptests.ml @@ -592,6 +592,8 @@ module SubDir: sig val make_oracle_file: t -> string -> string val make_result_file: t -> string -> string val make_file: t -> string -> string + + val result_dirname: string end = struct type t = string @@ -1360,6 +1362,7 @@ end = struct let expand_macros = let dune_cmd_features = Str.regexp "%{[a-z][a-z-]*:\\([^}]*\\)}" in let dune_bin_features = Str.regexp "%{bin:\\([^}]*\\)}" in + let dune_bin_subst = (Filename.dirname !toplevel_path) ^ "/\\1" in fun ~defaults cmd -> let ptest_config = if !special_config = "" then "" else "_" ^ !special_config @@ -1378,7 +1381,7 @@ end = struct [ "PTEST_CONFIG", ptest_config; "PTEST_DIR", SubDir.get cmd.directory; "PTEST_RESULT", - SubDir.get cmd.directory ^ "/" ^ redefine_name "result"; + SubDir.get cmd.directory ^ "/" ^ SubDir.result_dirname; "PTEST_FILE", ptest_file; "PTEST_NAME", ptest_name; "PTEST_NUMBER", string_of_int cmd.n; @@ -1413,7 +1416,7 @@ end = struct else toplevel in let toplevel = (* removes dune feature such as %{deps:...} *) - let x = str_global_replace dune_bin_features "./bin/\\1" toplevel in + let x = str_global_replace dune_bin_features dune_bin_subst toplevel in str_global_replace dune_cmd_features "\\1" x in { cmd with diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c index 4053c83792c943b37a32bf67cd97331d0ff216ef..5fcb6f0c3ebf0907f6bf7e0c50b030beef2ce9e1 100644 --- a/src/plugins/aorai/tests/ltl/test_recursion2.c +++ b/src/plugins/aorai/tests/ltl/test_recursion2.c @@ -1,6 +1,6 @@ /* run.config* OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ - OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ + OPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch3_if.c b/src/plugins/aorai/tests/ltl/test_switch3_if.c index 77e6d89fb0e13d46cb42dc53a4f350703aaa27e9..7411887a0f2a1140d5ef3ec56bb949db7c1349e4 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3_if.c +++ b/src/plugins/aorai/tests/ltl/test_switch3_if.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ + OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/aorai/tests/ltl/test_switch3_return.c b/src/plugins/aorai/tests/ltl/test_switch3_return.c index 0835dfd7f17e661398f7f32544650cde2af8d012..f2b2c98efc5833cfe28fc5810531ada97f216fc9 100644 --- a/src/plugins/aorai/tests/ltl/test_switch3_return.c +++ b/src/plugins/aorai/tests/ltl/test_switch3_return.c @@ -1,5 +1,5 @@ /* run.config* - OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ + OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@ */ /* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */ diff --git a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle index e2656fb94612807dd7810669096e9d83aebf1549..05d54eb1b3692086427e11ac0c4312ce3b3e97ac 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/calloc.res.oracle @@ -316,7 +316,7 @@ int main(void) } -[kernel] Parsing tests/stdlib/result/calloc.c (with preprocessing) +[kernel] Parsing tests/stdlib/result/ocode_calloc.c (with preprocessing) /* Generated by Frama-C */ #include "stdlib.h" struct X { diff --git a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle index a0671fe0bc81d0cf757f8660830d2cf9ab1898c8..51554abd5d6d303f3f6fd7571c3ff2c23eafc230 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/free.res.oracle @@ -139,7 +139,7 @@ void with_incomplete(struct incomplete *t) } -[kernel] Parsing tests/stdlib/result/free.c (with preprocessing) +[kernel] Parsing tests/stdlib/result/ocode_free.c (with preprocessing) /* Generated by Frama-C */ #include "stdlib.h" struct incomplete; diff --git a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle index 5fc593cb30dbecee8f1301238a8e35148decf5a5..e887b486810379137ffe902fac83c8a44a9a4d67 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/malloc.res.oracle @@ -218,7 +218,7 @@ int main(void) } -[kernel] Parsing tests/stdlib/result/malloc.c (with preprocessing) +[kernel] Parsing tests/stdlib/result/ocode_malloc.c (with preprocessing) /* Generated by Frama-C */ #include "stdlib.h" struct X { diff --git a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle index fd611034c64ab0b4253de89eaf7e4e2453515080..6875e220214f55e820a002a08689fd68969d6461 100644 --- a/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle +++ b/src/plugins/instantiate/tests/stdlib/oracle/no_fc_stdlib.res.oracle @@ -124,7 +124,7 @@ void foo(void) } -[kernel] Parsing tests/stdlib/result/no_fc_stdlib.c (with preprocessing) +[kernel] Parsing tests/stdlib/result/ocode_no_fc_stdlib.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" /*@ ghost extern int __fc_heap_status; */ diff --git a/src/plugins/instantiate/tests/stdlib/test_config b/src/plugins/instantiate/tests/stdlib/test_config index cc295b086555e3e3854cbe0f8013b3f96f464c7d..04017483a6c7c122176673be0c389b6aa68f7148 100644 --- a/src/plugins/instantiate/tests/stdlib/test_config +++ b/src/plugins/instantiate/tests/stdlib/test_config @@ -1 +1 @@ -OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c -ocode="" -print +OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@.c -print -then -no-instantiate @PTEST_RESULT@/ocode_@PTEST_NAME@.c -ocode="" -print diff --git a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle index 7923384e2abc16bd19a39ce72904917b804c210e..b6b11b24645b9d594a3f7b6d80c740da1a9b13fa 100644 --- a/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memcmp.res.oracle @@ -181,7 +181,7 @@ void with_null_or_int(int p[10]) } -[kernel] Parsing tests/string/result/memcmp.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memcmp.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle index 994ecf230487fad2663d6d9125543bfef2d762c4..82350dffc1f04e6ffcdd50c0e6d66d4cac9a753c 100644 --- a/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memcpy.res.oracle @@ -195,7 +195,7 @@ void with_null_or_int(int p[10]) } -[kernel] Parsing tests/string/result/memcpy.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memcpy.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle index 660db18e3fa68b711fcb1904dc37b99d0519436b..d88dce37409d64f2e0c98863a0d3d603d1fe7e49 100644 --- a/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memmove.res.oracle @@ -182,7 +182,7 @@ void with_null_or_int(int p[10]) } -[kernel] Parsing tests/string/result/memmove.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memmove.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle index e38819902b0aa425449261ceb23c705ae1d4abff..47f2d1af5ddf0ac7074bbc66e68e59d255cefb77 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_0.res.oracle @@ -278,7 +278,7 @@ void with_null_or_int(void) } -[kernel] Parsing tests/string/result/memset_0.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memset_0.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle index ba73c933112f552a9ba3d74d4a72cc6d8b678c30..f9e34dfba076c08df982ad5b01180d5f2ef9fabe 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_FF.res.oracle @@ -416,7 +416,7 @@ void with_null_or_int(void) } -[kernel] Parsing tests/string/result/memset_FF.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memset_FF.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle index c99bbab555ac56acc73b2c2e68315465b5fcd36d..c75e4edc3890b1e6eda0bb72955f678c6b9e5a67 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_typedef.res.oracle @@ -34,7 +34,7 @@ void test(void) } -[kernel] Parsing tests/string/result/memset_nested_typedef.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memset_nested_typedef.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle index 7185fe7a66598d4ad182720f927ea6e5f4ed4a8b..f552f8742b468569c9f3b2d7710c6abbb1dbb18e 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_nested_union.res.oracle @@ -20,7 +20,7 @@ void test(void) } -[kernel] Parsing tests/string/result/memset_nested_union.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memset_nested_union.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle index 545f2fa144a4428e2d46374c516fa7f42092a26f..4f82f4a1d43f08612bc4e3739f39aadb40a14ad6 100644 --- a/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle +++ b/src/plugins/instantiate/tests/string/oracle/memset_value.res.oracle @@ -192,7 +192,7 @@ void with_null_or_int(int value) } -[kernel] Parsing tests/string/result/memset_value.c (with preprocessing) +[kernel] Parsing tests/string/result/ocode_memset_value.c (with preprocessing) /* Generated by Frama-C */ #include "stddef.h" #include "string.h" diff --git a/src/plugins/instantiate/tests/string/test_config b/src/plugins/instantiate/tests/string/test_config index 0bfb957513347953e1c1eb05f79e0722c5fcaa2f..04017483a6c7c122176673be0c389b6aa68f7148 100644 --- a/src/plugins/instantiate/tests/string/test_config +++ b/src/plugins/instantiate/tests/string/test_config @@ -1 +1 @@ -OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-instantiate @PTEST_DIR@/result/@PTEST_NAME@.c -ocode="" -print \ No newline at end of file +OPT: @PTEST_FILE@ -instantiate -print -check -then -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@.c -print -then -no-instantiate @PTEST_RESULT@/ocode_@PTEST_NAME@.c -ocode="" -print diff --git a/src/plugins/markdown-report/tests/md/test_config b/src/plugins/markdown-report/tests/md/test_config index a6de95a18b6e6ac762b8988ba15d90f1dd4ac8d4..39520192dd0d0c81fbff3a6294c2f39c4fb80b54 100644 --- a/src/plugins/markdown-report/tests/md/test_config +++ b/src/plugins/markdown-report/tests/md/test_config @@ -1,3 +1,3 @@ PLUGIN: eva,inout,scope markdown_report -CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.@PTEST_NUMBER@.md +CMD: @frama-c@ -eva @PTEST_FILE@ -mdr-gen md -mdr-date="now" -mdr-out @PTEST_RESULT@/@PTEST_NAME@.@PTEST_NUMBER@.md LOG: @PTEST_NAME@.@PTEST_NUMBER@.md diff --git a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i index f74c36d4c224c0f792529bc703b3560a7ac70371..7f41b168b082e3d19f3540484cd7557b03a9c276 100644 --- a/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i +++ b/src/plugins/wp/tests/wp_acsl/chunk_typing_usable.i @@ -2,7 +2,7 @@ OPT: -wp-gen -wp-rte -wp-prover why3 -wp-msg-key print-generated */ /* run.config_qualif - OPT: -wp-rte -wp-coq-script @PTEST_DIR@/chunk_typing_usable.script -wp-prover alt-ergo,native:coq + OPT: -wp-rte -wp-coq-script %{dep:@PTEST_DIR@/chunk_typing_usable.script} -wp-prover alt-ergo,native:coq */ /*@ diff --git a/src/plugins/wp/tests/wp_acsl/classify_float.c b/src/plugins/wp/tests/wp_acsl/classify_float.c index d8defa956ed43e2b5cb2093be2a5b5242f8394fd..8c4932391e6248f70ca55fb5d29ae2b59cb0d332 100644 --- a/src/plugins/wp/tests/wp_acsl/classify_float.c +++ b/src/plugins/wp/tests/wp_acsl/classify_float.c @@ -1,7 +1,7 @@ /* run.config_qualif OPT: -wp-prover alt-ergo OPT: -wp-prover native:alt-ergo - OPT: -wp-prover native:coq -wp-coq-script @PTEST_DIR@/classify_float.script + OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/classify_float.script} OPT: -wp-model real */ diff --git a/src/plugins/wp/tests/wp_acsl/tset.i b/src/plugins/wp/tests/wp_acsl/tset.i index 208066a14375f6af2567fe81ff022c91a0838628..1f7b11df21bbacb99fcbf4de995db036cac04e8d 100644 --- a/src/plugins/wp/tests/wp_acsl/tset.i +++ b/src/plugins/wp/tests/wp_acsl/tset.i @@ -1,5 +1,5 @@ /* run.config_qualif - OPT: -wp -wp-prover alt-ergo,native:coq -wp-coq-script @PTEST_DIR@/tset.s + OPT: -wp -wp-prover alt-ergo,native:coq -wp-coq-script %{dep:@PTEST_DIR@/tset.s} */ /*@ diff --git a/src/plugins/wp/tests/wp_bts/bts_1174.i b/src/plugins/wp/tests/wp_bts/bts_1174.i index f50673b933b25cf3f63ca15ff10fc7c6bef22604..ce50d9189258794e8e0292d0262e3e922e763a83 100644 --- a/src/plugins/wp/tests/wp_bts/bts_1174.i +++ b/src/plugins/wp/tests/wp_bts/bts_1174.i @@ -1,5 +1,5 @@ /* run.config_qualif - OPT: -wp -wp-prover native:coq -wp-coq-script @PTEST_DIR@/bts_1174.s -wp-model +real + OPT: -wp -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/bts_1174.s} -wp-model +real */ /*@ requires -10. <= x && x <= 10.; */ diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c index 708ae7e8df94e667940e4727247cdcaa7fa1b55e..130896edb869eda985da946cc155712452c388bb 100644 --- a/src/plugins/wp/tests/wp_gallery/euclid.c +++ b/src/plugins/wp/tests/wp_gallery/euclid.c @@ -5,7 +5,7 @@ /* run.config_qualif - OPT: -wp-rte -wp-smoke-tests -wp-driver @PTEST_DIR@/euclid.wp + OPT: -wp-rte -wp-smoke-tests -wp-driver %{dep:@PTEST_DIR@/euclid.wp} */ /*@ diff --git a/src/plugins/wp/tests/wp_plugin/region_to_coq.i b/src/plugins/wp/tests/wp_plugin/region_to_coq.i index 1559385fdb5302d5b94264553758701e6e82385e..24ca4a86019fb5939ae553d2d1b18396e78c6a47 100644 --- a/src/plugins/wp/tests/wp_plugin/region_to_coq.i +++ b/src/plugins/wp/tests/wp_plugin/region_to_coq.i @@ -2,7 +2,7 @@ DONTRUN: */ /* run.config_qualif - OPT: -wp-prover native:coq -wp-coq-script @PTEST_DIR@/region_to_coq.script + OPT: -wp-prover native:coq -wp-coq-script %{dep:@PTEST_DIR@/region_to_coq.script} */ void copy(int* a, unsigned int n, int* b) diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config index c85101d0b58d18ca145d6963a56e1163ad1a7a0e..95a1509ecb2186f18d78ff6184dc767638359d65 100644 --- a/src/plugins/wp/tests/wp_region/test_config +++ b/src/plugins/wp/tests/wp_region/test_config @@ -1,4 +1,4 @@ PLUGIN: wp,rtegen CMD: @frama-c@ LOG: @PTEST_NAME@/region/job.dot -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 +OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_RESULT@/@PTEST_NAME@ -wp-fct job 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/pretty_printing/oracle/annotations.res.oracle b/tests/pretty_printing/oracle/annotations.res.oracle index 3149bcdb238e9dcd951850f1bf69e11db605d1eb..1829c1c323ca6ed40ef7d82b06bb1c968fc1b96f 100644 --- a/tests/pretty_printing/oracle/annotations.res.oracle +++ b/tests/pretty_printing/oracle/annotations.res.oracle @@ -110,16 +110,16 @@ void reference_function(void) } -[kernel] Parsing tests/pretty_printing/result/annotations.c (with preprocessing) +[kernel] Parsing tests/pretty_printing/result/ocode_annotations.c (with preprocessing) [kernel] Parsing tests/pretty_printing/annotations.i (no preprocessing) [kernel] tests/pretty_printing/annotations.i:13: Warning: - def'n of func function_no_ghost at tests/pretty_printing/annotations.i:13 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:12 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:12. + def'n of func function_no_ghost at tests/pretty_printing/annotations.i:13 (sum 9297192) conflicts with the one at tests/pretty_printing/result/ocode_annotations.c:12 (sum 14988159); keeping the one at tests/pretty_printing/result/ocode_annotations.c:12. [kernel] tests/pretty_printing/annotations.i:43: Warning: - def'n of func function_with_ghost at tests/pretty_printing/annotations.i:43 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:38 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:38. + def'n of func function_with_ghost at tests/pretty_printing/annotations.i:43 (sum 9297192) conflicts with the one at tests/pretty_printing/result/ocode_annotations.c:38 (sum 14988159); keeping the one at tests/pretty_printing/result/ocode_annotations.c:38. [kernel] tests/pretty_printing/annotations.i:80: Warning: - def'n of func ghost_function at tests/pretty_printing/annotations.i:80 (sum 9297192) conflicts with the one at tests/pretty_printing/result/annotations.c:71 (sum 14988159); keeping the one at tests/pretty_printing/result/annotations.c:71. + def'n of func ghost_function at tests/pretty_printing/annotations.i:80 (sum 9297192) conflicts with the one at tests/pretty_printing/result/ocode_annotations.c:71 (sum 14988159); keeping the one at tests/pretty_printing/result/ocode_annotations.c:71. [kernel] tests/pretty_printing/annotations.i:114: Warning: - dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:114 in favor of that at tests/pretty_printing/result/annotations.c:105 + dropping duplicate def'n of func reference_function at tests/pretty_printing/annotations.i:114 in favor of that at tests/pretty_printing/result/ocode_annotations.c:105 /* Generated by Frama-C */ /*@ axiomatic A { predicate P(ℤ x) diff --git a/tests/pretty_printing/oracle/binary_logic_op.res.oracle b/tests/pretty_printing/oracle/binary_logic_op.res.oracle index c6b04484a0da4f5518f5139a1775d0e1385628bb..c8326c418836b2314813fd1a4186f10f985d53c1 100644 --- a/tests/pretty_printing/oracle/binary_logic_op.res.oracle +++ b/tests/pretty_printing/oracle/binary_logic_op.res.oracle @@ -22,7 +22,7 @@ predicate mixed(ℤ x, ℤ y, ℤ z, ℤ t) = /*@ logic ℠exp(℠n) = \pow(\e, n); */ -[kernel] Parsing tests/pretty_printing/result/binary_logic_op.c (with preprocessing) +[kernel] Parsing tests/pretty_printing/result/ocode_binary_logic_op.c (with preprocessing) [kernel] Parsing tests/pretty_printing/binary_logic_op.c (with preprocessing) /* Generated by Frama-C */ /*@ diff --git a/tests/pretty_printing/oracle/ghost_else.res.oracle b/tests/pretty_printing/oracle/ghost_else.res.oracle index c3b49dbcc0dea91f4ffe8d4b3498a8008d901331..38c5141a7eae2340e9afc0b95246ec3a9e844f7f 100644 --- a/tests/pretty_printing/oracle/ghost_else.res.oracle +++ b/tests/pretty_printing/oracle/ghost_else.res.oracle @@ -44,18 +44,18 @@ void ghost_else_plus_else_association(int x) /*@ ghost (int y) */ } -[kernel] Parsing tests/pretty_printing/result/ghost_else.c (with preprocessing) +[kernel] Parsing tests/pretty_printing/result/ocode_ghost_else.c (with preprocessing) [kernel] Parsing tests/pretty_printing/ghost_else.i (no preprocessing) [kernel] tests/pretty_printing/ghost_else.i:1: Warning: - dropping duplicate def'n of func if_ghost_else_one_line at tests/pretty_printing/ghost_else.i:1 in favor of that at tests/pretty_printing/result/ghost_else.c:2 + dropping duplicate def'n of func if_ghost_else_one_line at tests/pretty_printing/ghost_else.i:1 in favor of that at tests/pretty_printing/result/ocode_ghost_else.c:2 [kernel] tests/pretty_printing/ghost_else.i:7: Warning: - dropping duplicate def'n of func if_ghost_else_block at tests/pretty_printing/ghost_else.i:7 in favor of that at tests/pretty_printing/result/ghost_else.c:9 + dropping duplicate def'n of func if_ghost_else_block at tests/pretty_printing/ghost_else.i:7 in favor of that at tests/pretty_printing/result/ocode_ghost_else.c:9 [kernel] tests/pretty_printing/ghost_else.i:15: Warning: - dropping duplicate def'n of func if_ghost_else_multi_line_block at tests/pretty_printing/ghost_else.i:15 in favor of that at tests/pretty_printing/result/ghost_else.c:16 + dropping duplicate def'n of func if_ghost_else_multi_line_block at tests/pretty_printing/ghost_else.i:15 in favor of that at tests/pretty_printing/result/ocode_ghost_else.c:16 [kernel] tests/pretty_printing/ghost_else.i:25: Warning: - dropping duplicate def'n of func normal_if_ghost_else_intricated at tests/pretty_printing/ghost_else.i:25 in favor of that at tests/pretty_printing/result/ghost_else.c:27 + dropping duplicate def'n of func normal_if_ghost_else_intricated at tests/pretty_printing/ghost_else.i:25 in favor of that at tests/pretty_printing/result/ocode_ghost_else.c:27 [kernel] tests/pretty_printing/ghost_else.i:32: Warning: - dropping duplicate def'n of func ghost_else_plus_else_association at tests/pretty_printing/ghost_else.i:32 in favor of that at tests/pretty_printing/result/ghost_else.c:35 + dropping duplicate def'n of func ghost_else_plus_else_association at tests/pretty_printing/ghost_else.i:32 in favor of that at tests/pretty_printing/result/ocode_ghost_else.c:35 /* Generated by Frama-C */ void if_ghost_else_one_line(int x) /*@ ghost (int y) */ { diff --git a/tests/pretty_printing/oracle/ghost_parameters.res.oracle b/tests/pretty_printing/oracle/ghost_parameters.res.oracle index b59174093b427f5066ee7460d3eccb3583401913..a98cc2f56963e1b66093dabaed9becf4e460b1e5 100644 --- a/tests/pretty_printing/oracle/ghost_parameters.res.oracle +++ b/tests/pretty_printing/oracle/ghost_parameters.res.oracle @@ -77,22 +77,22 @@ int main(void) } -[kernel] Parsing tests/pretty_printing/result/ghost_parameters.c (with preprocessing) +[kernel] Parsing tests/pretty_printing/result/ocode_ghost_parameters.c (with preprocessing) [kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing) [kernel] tests/pretty_printing/ghost_parameters.c:7: Warning: - dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:7 in favor of that at tests/pretty_printing/result/ghost_parameters.c:4 + dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:7 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:4 [kernel] tests/pretty_printing/ghost_parameters.c:9: Warning: - dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:9 in favor of that at tests/pretty_printing/result/ghost_parameters.c:11 + dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:9 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:11 [kernel] tests/pretty_printing/ghost_parameters.c:11: Warning: - dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:11 in favor of that at tests/pretty_printing/result/ghost_parameters.c:18 + dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:11 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:18 [kernel] tests/pretty_printing/ghost_parameters.c:13: Warning: - dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:13 in favor of that at tests/pretty_printing/result/ghost_parameters.c:25 + dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:13 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:25 [kernel] tests/pretty_printing/ghost_parameters.c:15: Warning: - dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:15 in favor of that at tests/pretty_printing/result/ghost_parameters.c:32 + dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:15 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:32 [kernel] tests/pretty_printing/ghost_parameters.c:22: Warning: - dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:22 in favor of that at tests/pretty_printing/result/ghost_parameters.c:42 + dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:22 in favor of that at tests/pretty_printing/result/ocode_ghost_parameters.c:42 [kernel] tests/pretty_printing/ghost_parameters.c:24: Warning: - def'n of func main at tests/pretty_printing/ghost_parameters.c:24 (sum 21482) conflicts with the one at tests/pretty_printing/result/ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ghost_parameters.c:47. + def'n of func main at tests/pretty_printing/ghost_parameters.c:24 (sum 21482) conflicts with the one at tests/pretty_printing/result/ocode_ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ocode_ghost_parameters.c:47. /* Generated by Frama-C */ void decl_function_void_no_ghost(void); diff --git a/tests/pretty_printing/oracle/relations.res.oracle b/tests/pretty_printing/oracle/relations.res.oracle index 94bbc7e081951208d9f06c0696a1d8ac958295b7..1b97788b575d57ec592946b007b6a6d7535a2104 100644 --- a/tests/pretty_printing/oracle/relations.res.oracle +++ b/tests/pretty_printing/oracle/relations.res.oracle @@ -5,7 +5,7 @@ /*@ predicate rel2(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≡ z ∧ z ≥ t; */ -[kernel] Parsing tests/pretty_printing/result/relations.c (with preprocessing) +[kernel] Parsing tests/pretty_printing/result/ocode_relations.c (with preprocessing) [kernel] Parsing tests/pretty_printing/relations.c (with preprocessing) /* Generated by Frama-C */ /*@ predicate rel1(ℤ x, ℤ y, ℤ z, ℤ t) = x ≤ y ≤ z ∧ z ≥ t; diff --git a/tests/pretty_printing/test_config b/tests/pretty_printing/test_config index 3ef00bad562303349e568b77920e4499cd980972..ff6680cfb28502ee263c420ddbb028c47ffde076 100644 --- a/tests/pretty_printing/test_config +++ b/tests/pretty_printing/test_config @@ -3,4 +3,4 @@ COMMENT: the default option checks that pretty-printed code can be merged COMMENT: with the original one PLUGIN: CMD: FRAMAC_PLUGIN=tests/.empty @frama-c@ -OPT: @PTEST_FILE@ -print -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print +OPT: @PTEST_FILE@ -print -then -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@.c -print -then @PTEST_RESULT@/ocode_@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print diff --git a/tests/saveload/basic.i b/tests/saveload/basic.i index aa5e20c519e90c4b82ee0e9cd9a8040912b818aa..96e934171473758e5b70f373733d4c78325ab754 100644 --- a/tests/saveload/basic.i +++ b/tests/saveload/basic.i @@ -3,16 +3,16 @@ EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/basic.sav > @PTEST_RESULT@/basic_sav.res 2> @PTEST_RESULT@/basic_sav.err MODULE: EXECNOW: LOG basic_sav.1.res LOG basic_sav.1.err BIN basic.1.sav @frama-c@ -save @PTEST_RESULT@/basic.1.sav @PTEST_FILE@ -eva @EVA_OPTIONS@ -out -input -deps > @PTEST_RESULT@/basic_sav.1.res 2> @PTEST_RESULT@/basic_sav.1.err - STDOPT: +"-load @PTEST_RESULT@/basic.sav -eva @EVA_OPTIONS@ -out -input -deps" + STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.sav} -eva @EVA_OPTIONS@ -out -input -deps" MODULE: @PTEST_NAME@ - STDOPT: +"-load @PTEST_RESULT@/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -print" + STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.1}.sav -eva @EVA_OPTIONS@ -out -input -deps -print" MODULE: - STDOPT: +"-load @PTEST_RESULT@/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps" + STDOPT: +"-load %{dep:@PTEST_RESULT@/basic.1}.sav -eva @EVA_OPTIONS@ -out -input -deps" MODULE: status EXECNOW: LOG status_sav.res LOG status_sav.err BIN status.sav @frama-c@ -save @PTEST_RESULT@/status.sav @PTEST_FILE@ > @PTEST_RESULT@/status_sav.res 2> @PTEST_RESULT@/status_sav.err - STDOPT: +"-load @PTEST_RESULT@/status.sav" + STDOPT: +"-load %{dep:@PTEST_RESULT@/status.sav}" MODULE: - STDOPT: +"-load @PTEST_RESULT@/status.sav" + STDOPT: +"-load %{dep:@PTEST_RESULT@/status.sav}" */ int main() { int i,j; i=10; /*@ assert (i == 10); */ diff --git a/tests/saveload/bool.c b/tests/saveload/bool.c index 6101341838697f0bb957216bd1d532fa31e9fc68..ee02ead4e9d496c0b0df6b584b6454ca770acc57 100644 --- a/tests/saveload/bool.c +++ b/tests/saveload/bool.c @@ -1,7 +1,7 @@ /* 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 - STDOPT: +"-load @PTEST_RESULT@/bool.sav -out -input -deps" - STDOPT: +"-load @PTEST_RESULT@/bool.sav -eva @EVA_OPTIONS@" + 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 %{dep:@PTEST_RESULT@/bool.sav} -out -input -deps" + STDOPT: +"-load %{dep:@PTEST_RESULT@/bool.sav} -eva @EVA_OPTIONS@" */ #include "stdbool.h" diff --git a/tests/saveload/callbacks.i b/tests/saveload/callbacks.i index 31080cb964bc2de06d93c43bd6e278a695cd7666..5d0b112d238d1c3f9fb76ecef4492e95d051f47f 100644 --- a/tests/saveload/callbacks.i +++ b/tests/saveload/callbacks.i @@ -1,6 +1,6 @@ /* 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 - STDOPT: +"-load @PTEST_RESULT@/callbacks.sav -main main2 -then -main main3" + 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 %{dep:@PTEST_RESULT@/callbacks.sav} -main main2 -then -main main3" */ /* This tests whether the callbacks for callwise inout and from survive after diff --git a/tests/saveload/deps.i b/tests/saveload/deps.i index 02bc741da501590b68ba789eb1a39e2add5a19c5..633c19718ec97a731deb96a7354f64763379b5ba 100644 --- a/tests/saveload/deps.i +++ b/tests/saveload/deps.i @@ -1,15 +1,15 @@ /* run.config MODULE: deps_A EXECNOW: LOG deps_sav.res LOG deps_sav.err BIN deps.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/deps.sav > @PTEST_RESULT@/deps_sav.res 2> @PTEST_RESULT@/deps_sav.err - STDOPT: +"-load @PTEST_RESULT@/deps.sav -eva @EVA_OPTIONS@ -out -input -deps " + STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -eva @EVA_OPTIONS@ -out -input -deps " MODULE: deps_B - STDOPT: +"-load @PTEST_RESULT@/deps.sav -out -input -deps " + STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps " MODULE: deps_C - STDOPT: +"-load @PTEST_RESULT@/deps.sav -out -input -deps " + STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps " MODULE: deps_D - STDOPT: +"-load @PTEST_RESULT@/deps.sav -out -input -deps " + STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps " MODULE: deps_E - STDOPT: +"-load @PTEST_RESULT@/deps.sav -out -input -deps " + STDOPT: +"-load %{dep:@PTEST_RESULT@/deps.sav} -out -input -deps " */ int main() { diff --git a/tests/saveload/isset.c b/tests/saveload/isset.c index 26c3f18e1fc8a7c0627f9dcc29bfc678ddb0b2d4..ebbce985577b02a719fafbf360c4f5bb05a3ce7c 100644 --- a/tests/saveload/isset.c +++ b/tests/saveload/isset.c @@ -1,9 +1,9 @@ /* 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 - STDOPT: +"-quiet -load @PTEST_RESULT@/isset.sav" - STDOPT: +"-load @PTEST_RESULT@/isset.sav" - STDOPT: +"-eva @EVA_OPTIONS@ -load @PTEST_RESULT@/isset.sav" - STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load @PTEST_RESULT@/isset.sav" + 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 %{dep:@PTEST_RESULT@/isset.sav}" + STDOPT: +"-load %{dep:@PTEST_RESULT@/isset.sav}" + STDOPT: +"-eva @EVA_OPTIONS@ -load %{dep:@PTEST_RESULT@/isset.sav}" + STDOPT: +"-quiet -eva @EVA_OPTIONS@ -load %{dep:@PTEST_RESULT@/isset.sav}" */ int main() { diff --git a/tests/saveload/multi_project.i b/tests/saveload/multi_project.i index 7631ac9cf43acd82fd71b28101bf581c31ffdd67..ec08de1fdb456c2aa77a3902568c09ff6513a32e 100644 --- a/tests/saveload/multi_project.i +++ b/tests/saveload/multi_project.i @@ -1,7 +1,7 @@ /* run.config PLUGIN: @EVA_PLUGINS@ constant_propagation EXECNOW: BIN multi_project.sav LOG multi_project_sav.res LOG multi_project_sav.err @frama-c@ -save @PTEST_RESULT@/multi_project.sav @EVA_OPTIONS@ -semantic-const-folding @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_RESULT@/multi_project_sav.res 2> @PTEST_RESULT@/multi_project_sav.err - STDOPT: +"-load @PTEST_RESULT@/multi_project.sav" + STDOPT: +"-load %{dep:@PTEST_RESULT@/multi_project.sav}" MODULE: @PTEST_NAME@ OPT: -eva @EVA_OPTIONS@ */ diff --git a/tests/saveload/segfault_datatypes.i b/tests/saveload/segfault_datatypes.i index c9f3c903e9be03fb7df6ead50d84ace91cdea1bb..128453345c41c009c35b09b4ac912e801942a281 100644 --- a/tests/saveload/segfault_datatypes.i +++ b/tests/saveload/segfault_datatypes.i @@ -2,7 +2,7 @@ MODULE: segfault_datatypes_A EXECNOW: LOG segfault_datatypes_sav.res LOG segfault_datatypes_sav.err BIN segfault_datatypes.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save @PTEST_RESULT@/segfault_datatypes.sav > @PTEST_RESULT@/segfault_datatypes_sav.res 2> @PTEST_RESULT@/segfault_datatypes_sav.err MODULE: segfault_datatypes_B - STDOPT: +"-load @PTEST_RESULT@/segfault_datatypes.sav -eva -out -input -deps" + STDOPT: +"-load %{dep:@PTEST_RESULT@/segfault_datatypes.sav} -eva -out -input -deps" */ int main() { diff --git a/tests/saveload/sparecode.i b/tests/saveload/sparecode.i index 31038cd694580d3273716dcd1e44736f2970aa30..933cb8cb8de234563c6dea164eb9193a7df0ab87 100644 --- a/tests/saveload/sparecode.i +++ b/tests/saveload/sparecode.i @@ -1,7 +1,7 @@ /* 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 - STDOPT: +"-load @PTEST_RESULT@/sparecode.sav" + 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 %{dep:@PTEST_RESULT@/sparecode.sav}" */ int G; int f (int x, int y) { 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/label_decl.i b/tests/syntax/label_decl.i index c6a7fcb79492044085cf80ecbee80f69eacb2e63..2304ecf7522732f3208f6b4a901012412022b4b1 100644 --- a/tests/syntax/label_decl.i +++ b/tests/syntax/label_decl.i @@ -1,5 +1,5 @@ /* run.config -MACRO: TMP @PTEST_RESULT@/@PTEST_NAME@.i +MACRO: TMP @PTEST_RESULT@/ocode_@PTEST_NAME@.i OPT: -print -then -print -ocode @TMP@ -then @TMP@ -print -ocode="" */ struct s { int i; }; 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/oracle/label_decl.res.oracle b/tests/syntax/oracle/label_decl.res.oracle index 00c3bd3ef4dde9fec38209c01b097120091b110b..a89bc6ffece739b4ed56d206272bf00f2a2488f2 100644 --- a/tests/syntax/oracle/label_decl.res.oracle +++ b/tests/syntax/oracle/label_decl.res.oracle @@ -24,7 +24,7 @@ void main(void) } -[kernel] Parsing tests/syntax/result/label_decl.i (no preprocessing) +[kernel] Parsing tests/syntax/result/ocode_label_decl.i (no preprocessing) /* Generated by Frama-C */ struct s { int i ; 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"