Skip to content
Snippets Groups Projects
Commit 0b0cceb6 authored by Andre Maroneze's avatar Andre Maroneze Committed by Patrick Baudin
Browse files

[tests] dune: fix test directory 'syntax'

parent dd481d05
No related branches found
No related tags found
No related merge requests found
/* run.config /* run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
MODULE: @PTEST_NAME@ MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@ OPT: @EVA_OPTIONS@
*/ */
......
/* run.config /* 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) { static inline void f(void) {
return; return;
......
/* run.config /* run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
STDOPT: +"-copy" +"-eva" STDOPT: +"-copy" +"-eva"
*/ */
/*@ predicate p(int x); */ /*@ predicate p(int x); */
......
/* run.config /* run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
STDOPT: +"-copy -eva @EVA_CONFIG@" STDOPT: +"-copy -eva @EVA_CONFIG@"
*/ */
struct S { struct S {
......
/* run.config* /* 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 [\$(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 "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\")\"" OPT: -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
......
/* run.config /* 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@_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@ OPT: %{dep:@PTEST_DIR@/@PTEST_NAME@_2.i} %{dep:@PTEST_DIR@/@PTEST_NAME@_1.i} -eva @EVA_CONFIG@
*/ */
......
/* run.config /* run.config
MODULE: @PTEST_NAME@ 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); void f(int x);
......
/*run.config /*run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
OPT: -eva -eva-verbose 0 OPT: -eva -eva-verbose 0
*/ */
......
/* run.config /* run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
STDOPT: +"-eva-slevel 100 -eva" STDOPT: +"-eva-slevel 100 -eva"
STDOPT: +"-ulevel 1 -eva-slevel 100 -eva" STDOPT: +"-ulevel 1 -eva-slevel 100 -eva"
STDOPT: +"-ulevel 2 -eva-slevel 100 -eva" STDOPT: +"-ulevel 2 -eva-slevel 100 -eva"
......
/* run.config /* run.config
OPT: @PTEST_SHARE_DIR@/libc/string.h @PTEST_FILE@ @PTEST_FILE@ -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@ @PTEST_SHARE_DIR@/libc/string.h @PTEST_FILE@ -cpp-extra-args="-I@PTEST_SHARE_DIR@/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@ @PTEST_SHARE_DIR@/libc/string.h -cpp-extra-args="-I@PTEST_SHARE_DIR@/libc" -print OPT: @PTEST_FILE@ @PTEST_FILE@ @FRAMAC_SHARE@/libc/string.h -cpp-extra-args="-I@FRAMAC_SHARE@/libc" -print
*/ */
#include "string.h" #include "string.h"
......
/* run.config* /* run.config*
PLUGIN: eva,scope variadic PLUGIN: eva,inout,scope,variadic
TIMEOUT: 600 TIMEOUT: 600
OPT: -eva OPT: -eva
*/ */
......
/* run.config /* run.config
PLUGIN: eva,scope PLUGIN: eva,inout,scope
STDOPT: +"-eva @EVA_CONFIG@" STDOPT: +"-eva @EVA_CONFIG@"
STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3" STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/ */
......
/* run.config* /* run.config*
PLUGIN: eva,scope,variadic PLUGIN: eva,inout,scope,variadic
TIMEOUT: 600 TIMEOUT: 600
OPT: -eva OPT: -eva
*/ */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment