Skip to content
Snippets Groups Projects
Commit a7375cf0 authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[tests] dune: fix test directory 'syntax'

parent 79e79600
No related branches found
No related tags found
No related merge requests found
/* run.config
PLUGIN: eva,scope
PLUGIN: eva,inout,scope
MODULE: @PTEST_NAME@
OPT: @EVA_OPTIONS@
*/
......
/* 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;
......
/* run.config
PLUGIN: eva,scope
PLUGIN: eva,inout,scope
STDOPT: +"-copy" +"-eva"
*/
/*@ predicate p(int x); */
......
/* run.config
PLUGIN: eva,scope
PLUGIN: eva,inout,scope
STDOPT: +"-copy -eva @EVA_CONFIG@"
*/
struct S {
......
/* 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\")\""
......
/* 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@
*/
......
/* 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);
......
/*run.config
PLUGIN: eva,scope
PLUGIN: eva,inout,scope
OPT: -eva -eva-verbose 0
*/
......
/* 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"
......
/* 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"
......
/* run.config*
PLUGIN: eva,scope variadic
PLUGIN: eva,inout,scope,variadic
TIMEOUT: 600
OPT: -eva
*/
......
/* run.config
PLUGIN: eva,scope
PLUGIN: eva,inout,scope
STDOPT: +"-eva @EVA_CONFIG@"
STDOPT: +"-eva @EVA_CONFIG@ -main main2 -eva-slevel 3"
*/
......
/* run.config*
PLUGIN: eva,scope,variadic
PLUGIN: eva,inout,scope,variadic
TIMEOUT: 600
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