diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i index c1d19f0a1d62fa1dd8b3d2f9befaaf2872fd4b25..8e90e305d54670a110f619787381ac9e1100d754 100644 --- a/tests/syntax/Refresh_visitor.i +++ b/tests/syntax/Refresh_visitor.i @@ -1,5 +1,5 @@ /* run.config - PLUGIN: eva,scope + PLUGIN: eva,inout,scope MODULE: @PTEST_NAME@ OPT: @EVA_OPTIONS@ */ diff --git a/tests/syntax/aggressive_merging_1.i b/tests/syntax/aggressive_merging_1.i index 78f7123911b96029ba8f65fb1f55b78808c3cf65..1ff332eec4e9331acd9f2b91b82e9dce907fe024 100644 --- a/tests/syntax/aggressive_merging_1.i +++ b/tests/syntax/aggressive_merging_1.i @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"@PTEST_DIR@/aggressive_merging_2.i -aggressive-merging" + STDOPT: +"%{dep:@PTEST_DIR@/aggressive_merging_2.i} -aggressive-merging" */ static inline void f(void) { return; diff --git a/tests/syntax/copy_logic.i b/tests/syntax/copy_logic.i index fee16b6120468fa4170798dc4290114348c9ee3d..c9c68d8a493f321d323ef1382a82dc84d98eff25 100644 --- a/tests/syntax/copy_logic.i +++ b/tests/syntax/copy_logic.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope STDOPT: +"-copy" +"-eva" */ /*@ predicate p(int x); */ diff --git a/tests/syntax/copy_visitor.i b/tests/syntax/copy_visitor.i index d2d4bdb124e786dd2ee04327d9803b86b6c3dbe7..d0c307b2068b9db0356af413dfe3c78b7c8045a0 100644 --- a/tests/syntax/copy_visitor.i +++ b/tests/syntax/copy_visitor.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope STDOPT: +"-copy -eva @EVA_CONFIG@" */ struct S { diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c index 3103293805e66116dcc164d40fb9b10e3333df4d..2510c0664e13ed50791184392085a1abf20a793e 100644 --- a/tests/syntax/cpp-command.c +++ b/tests/syntax/cpp-command.c @@ -1,5 +1,5 @@ /* run.config* - FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::g; s:$(realpath @PTEST_SHARE_DIR@)/:FRAMAC_SHARE/:g; s:@PTEST_MAKE_DIR@/result@PTEST_CONFIG@/::g; s: -m32::" + FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::g; s:$(realpath @FRAMAC_SHARE@)/:FRAMAC_SHARE/:g; s:@PTEST_MAKE_DIR@/result@PTEST_CONFIG@/::g; s: -m32::" OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']" OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'" OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\"" diff --git a/tests/syntax/extern_init.i b/tests/syntax/extern_init.i index 2a7d0516f9bc639eb3797d330672997f25b28c9a..1e63bc6a5cd0edcd038a9d842debb5ac53e5ec80 100644 --- a/tests/syntax/extern_init.i +++ b/tests/syntax/extern_init.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope OPT: %{dep:@PTEST_DIR@/@PTEST_NAME@_1.i} %{dep:@PTEST_DIR@/@PTEST_NAME@_2.i} -eva @EVA_CONFIG@ OPT: %{dep:@PTEST_DIR@/@PTEST_NAME@_2.i} %{dep:@PTEST_DIR@/@PTEST_NAME@_1.i} -eva @EVA_CONFIG@ */ diff --git a/tests/syntax/formals_decl_leak.i b/tests/syntax/formals_decl_leak.i index 0b767a1328585f2b970022d3318315d8d381ec7d..75df98918e1701ee9d233ba79608fccadaee7da2 100644 --- a/tests/syntax/formals_decl_leak.i +++ b/tests/syntax/formals_decl_leak.i @@ -1,6 +1,6 @@ /* run.config MODULE: @PTEST_NAME@ - OPT: -print -no-autoload-plugins @PTEST_DIR@/@PTEST_NAME@_1.i + OPT: -print -no-autoload-plugins %{dep:@PTEST_DIR@/@PTEST_NAME@_1.i} */ void f(int x); diff --git a/tests/syntax/local-init-const.i b/tests/syntax/local-init-const.i index 09793138d4693239a17072a39327874320e9e4ff..aeb29c151f7af352361381c4ba9611dcfedbdf91 100644 --- a/tests/syntax/local-init-const.i +++ b/tests/syntax/local-init-const.i @@ -1,5 +1,5 @@ /*run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope OPT: -eva -eva-verbose 0 */ diff --git a/tests/syntax/loop-case-switch-for-unroll.c b/tests/syntax/loop-case-switch-for-unroll.c index 3052cb9f5529fa6a77d6763f81aaee4673598cbd..89f55e84166e4ac47316c2293ba53e2a861a4730 100644 --- a/tests/syntax/loop-case-switch-for-unroll.c +++ b/tests/syntax/loop-case-switch-for-unroll.c @@ -1,5 +1,5 @@ /* run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope STDOPT: +"-eva-slevel 100 -eva" STDOPT: +"-ulevel 1 -eva-slevel 100 -eva" STDOPT: +"-ulevel 2 -eva-slevel 100 -eva" diff --git a/tests/syntax/multiple_decls_contracts.c b/tests/syntax/multiple_decls_contracts.c index f79505c2b03a7798b228f71157c1b53022a7d54f..ed1bb4e881630b31d8ff7f4ff1a072f1a06a51ce 100644 --- a/tests/syntax/multiple_decls_contracts.c +++ b/tests/syntax/multiple_decls_contracts.c @@ -1,7 +1,7 @@ /* run.config -OPT: @PTEST_SHARE_DIR@/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-I@PTEST_SHARE_DIR@/libc" -print -OPT: @PTEST_FILE@ @PTEST_SHARE_DIR@/libc/string.h @PTEST_FILE@ -cpp-extra-args="-I@PTEST_SHARE_DIR@/libc" -print -OPT: @PTEST_FILE@ @PTEST_FILE@ @PTEST_SHARE_DIR@/libc/string.h -cpp-extra-args="-I@PTEST_SHARE_DIR@/libc" -print +OPT: @FRAMAC_SHARE@/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print +OPT: @PTEST_FILE@ @FRAMAC_SHARE@/libc/string.h @PTEST_FILE@ -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print +OPT: @PTEST_FILE@ @PTEST_FILE@ @FRAMAC_SHARE@/libc/string.h -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print */ #include "string.h" diff --git a/tests/syntax/string_concat.c b/tests/syntax/string_concat.c index b78a7d85590f3c5981b36737e9d20ec207dc0aad..880298a40b739d8cb8462d02229ffea2e46db699 100644 --- a/tests/syntax/string_concat.c +++ b/tests/syntax/string_concat.c @@ -1,5 +1,5 @@ /* run.config* -PLUGIN: eva,scope variadic +PLUGIN: eva,inout,scope,variadic TIMEOUT: 600 OPT: -eva */ diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i index 4fcef3f5d46dfd9784cf49c16fa8fbe38b7c99f4..7747244a7ae8b6e13488bb985d673736de6a9c04 100644 --- a/tests/syntax/unroll_labels.i +++ b/tests/syntax/unroll_labels.i @@ -1,5 +1,5 @@ /* run.config -PLUGIN: eva,scope +PLUGIN: eva,inout,scope STDOPT: +"-eva @EVA_CONFIG@" STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3" */ diff --git a/tests/syntax/wstring_concat.c b/tests/syntax/wstring_concat.c index 9bd6571dd63b901380598f6dc29c9b769f8f6f24..c0d264e6f1e5d8ba48a4d280f4f95fb8c7db88b8 100644 --- a/tests/syntax/wstring_concat.c +++ b/tests/syntax/wstring_concat.c @@ -1,5 +1,5 @@ /* run.config* -PLUGIN: eva,scope,variadic +PLUGIN: eva,inout,scope,variadic TIMEOUT: 600 OPT: -eva */