From a7375cf0314cfac8ae64c9ee2335c6edb99fe4e2 Mon Sep 17 00:00:00 2001 From: Andre Maroneze <andre.maroneze@cea.fr> Date: Wed, 16 Feb 2022 18:07:27 +0100 Subject: [PATCH] [tests] dune: fix test directory 'syntax' --- tests/syntax/Refresh_visitor.i | 2 +- tests/syntax/aggressive_merging_1.i | 2 +- tests/syntax/copy_logic.i | 2 +- tests/syntax/copy_visitor.i | 2 +- tests/syntax/cpp-command.c | 2 +- tests/syntax/extern_init.i | 2 +- tests/syntax/formals_decl_leak.i | 2 +- tests/syntax/local-init-const.i | 2 +- tests/syntax/loop-case-switch-for-unroll.c | 2 +- tests/syntax/multiple_decls_contracts.c | 6 +++--- tests/syntax/string_concat.c | 2 +- tests/syntax/unroll_labels.i | 2 +- tests/syntax/wstring_concat.c | 2 +- 13 files changed, 15 insertions(+), 15 deletions(-) diff --git a/tests/syntax/Refresh_visitor.i b/tests/syntax/Refresh_visitor.i index c1d19f0a1d6..8e90e305d54 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 78f7123911b..1ff332eec4e 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 fee16b61204..c9c68d8a493 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 d2d4bdb124e..d0c307b2068 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 3103293805e..2510c0664e1 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 2a7d0516f9b..1e63bc6a5cd 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 0b767a13285..75df98918e1 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 09793138d46..aeb29c151f7 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 3052cb9f552..89f55e84166 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 f79505c2b03..ed1bb4e8816 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 b78a7d85590..880298a40b7 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 4fcef3f5d46..7747244a7ae 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 9bd6571dd63..c0d264e6f1e 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 */ -- GitLab