Skip to content
Snippets Groups Projects
Commit 1640e5f0 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[tests] more use of @PTEST_RESULT@ and @PTEST_DIR@ in order to ease dune migration

parent b7723577
No related branches found
No related tags found
No related merge requests found
Showing
with 37 additions and 37 deletions
/* run.config
NOFRAMAC:
LIBS:
EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log.txt
EXECNOW: LOG @PTEST_NAME@.res.1.log.txt @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log.txt
EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} @PTEST_FILE@ -save @PTEST_RESULT@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@.res.0.log.txt
EXECNOW: LOG @PTEST_NAME@.res.1.log.txt @frama-c@ -load @PTEST_RESULT@/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_RESULT@/@PTEST_NAME@.res.1.log.txt
*/
/* run.config_prove
DONTRUN:
......
/* run.config
CMD: @frama-c@ -eva -eva-no-results -mdr-gen sarif -mdr-sarif-deterministic
LOG: with-libc.sarif
OPT: -mdr-out @PTEST_DIR@/result/with-libc.sarif
OPT: -mdr-out @PTEST_RESULT@/with-libc.sarif
LOG: without-libc.sarif
OPT: -mdr-no-print-libc -mdr-out @PTEST_DIR@/result/without-libc.sarif
OPT: -mdr-no-print-libc -mdr-out @PTEST_RESULT@/without-libc.sarif
*/
#include <string.h>
......
/* run.config*
LOG: @PTEST_NAME@.sarif
OPT: -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out @PTEST_DIR@/result/@PTEST_NAME@.sarif
OPT: -eva -then -mdr-sarif-deterministic -mdr-gen sarif -mdr-out @PTEST_RESULT@/@PTEST_NAME@.sarif
*/
#include "string.c"
......
/*run.config
OPT: -add-path tests/dynamic/file_path -add-path tests/dynamic/directory_path -add-path tests/dynamic/none
OPT: -add-path @PTEST_DIR@/file_path -add-path @PTEST_DIR@/directory_path -add-path @PTEST_DIR@/none
MODULE: empty abstract abstract2
OPT:
*/
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
EXECNOW: LOG build-callgraph.res LOG build-callgraph.err bin/frama-c-script heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_DIR@/result/build-callgraph.res 2> @PTEST_DIR@/result/build-callgraph.err
EXECNOW: LOG build-callgraph.res LOG build-callgraph.err bin/frama-c-script heuristic-print-callgraph @PTEST_DIR@/@PTEST_NAME@.i > @PTEST_RESULT@/build-callgraph.res 2> @PTEST_RESULT@/build-callgraph.err
*/
#include <stdio.h>
......
/* run.config
NOFRAMAC: testing frama-c-script, not frama-c itself
EXECNOW: LOG recursions.res LOG recursions.err bin/frama-c-script heuristic-detect-recursion @PTEST_FILE@ > @PTEST_DIR@/result/recursions.res 2> @PTEST_DIR@/result/recursions.err
EXECNOW: LOG recursions.res LOG recursions.err bin/frama-c-script heuristic-detect-recursion @PTEST_FILE@ > @PTEST_RESULT@/recursions.res 2> @PTEST_RESULT@/recursions.err
*/
volatile int v;
......
......@@ -7,7 +7,7 @@
MODULE: @PTEST_NAME@
OPT: -json-compilation-database %{dep:@PTEST_DIR@/with_arguments.json}
MODULE:
EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/compile_commands_working.json} > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
EXECNOW: LOG list_files.res LOG list_files.err %{bin:frama-c-script} list-files %{dep:@PTEST_DIR@/compile_commands_working.json} > @PTEST_RESULT@/list_files.res 2> @PTEST_RESULT@/list_files.err
*/
#include <stdio.h>
......
......@@ -43,6 +43,6 @@ int main(int argc, char **argv)
/*
Local Variables:
compile-command: "cd ../.. && ptests.byte -show -config gcc tests/libc/time.c"
compile-command: "cd ../.. && ptests.byte -show -config gcc @PTEST_DIR@/time.c"
End:
*/
......@@ -2,7 +2,7 @@
STDOPT: #"-metrics-no-libc -metrics-eva-cover"
STDOPT: #"-metrics-libc -metrics-eva-cover"
LOG: libc.json
STDOPT: #"-metrics-libc -metrics-output @PTEST_DIR@/result/libc.json"
STDOPT: #"-metrics-libc -metrics-output @PTEST_RESULT@/libc.json"
*/
#include <ctype.h>
#include <stdio.h> // defines external variables
......
/* run.config
OPT: -typecheck tests/misc/bts0525.i
OPT: -typecheck @PTEST_DIR@/bts0525.i
*/
typedef enum {E1=2, E2} T_EN1 ;
......
/* run.config
OPT: tests/misc/bts0525-2.i
OPT: @PTEST_DIR@/bts0525-2.i
*/
typedef enum {E3=2, E4} T_EN2 ;
typedef enum {E1=2, E2} T_EN1 ;
......
......@@ -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
// tests/misc/bts0990_link_1.i
// @PTEST_DIR@/bts0990_link_1.i
char *s;
......
/* run.config
OPT: -print tests/misc/mergestruct1.i tests/misc/mergestruct2.i
OPT: -print tests/misc/mergestruct2.i tests/misc/mergestruct1.i
OPT: -print @PTEST_DIR@/mergestruct1.i @PTEST_DIR@/mergestruct2.i
OPT: -print @PTEST_DIR@/mergestruct2.i @PTEST_DIR@/mergestruct1.i
*/
struct s { float a; } s2;
......
/* run.config
PLUGIN:
MODULE: @PTEST_NAME@
EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@_sav.res 2> @PTEST_DIR@/result/@PTEST_NAME@_sav.err
EXECNOW: LOG my_visitor_sav.res LOG my_visitor_sav.err BIN my_visitor.sav @frama-c@ @PTEST_FILE@ -main f -save @PTEST_DIR@/@PTEST_NAME@.sav > @PTEST_RESULT@/@PTEST_NAME@_sav.res 2> @PTEST_RESULT@/@PTEST_NAME@_sav.err
OPT: -load %{dep:@PTEST_DIR@/@PTEST_NAME@.sav} -no-my-visitor -print
MODULE:
OPT: -load %{dep:@PTEST_DIR@/@PTEST_NAME@.sav} -print
......
/* run.config
STDOPT: +"-lib-entry -main g -pdg -pdg-dot tests/pdg/result/call "
STDOPT: +"-lib-entry -main g -pdg -pdg-dot @PTEST_RESULT@/call "
*/
/* Ne pas modifier : exemple utilisé dans le rapport. */
......
/* run.config
STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot tests/pdg/result/doc"
STDOPT: +"-lib-entry -main g -fct-pdg g -pdg-dot @PTEST_RESULT@/doc"
*/
/* To build the svg file:
* dot -Tsvg tests/pdg/result/doc.g.dot > tests/pdg/result/doc.g.svg
* dot -Tsvg @PTEST_RESULT@/doc.g.dot > @PTEST_RESULT@/doc.g.svg
*/
int G1, G2, T[10];
......
......@@ -20,15 +20,15 @@ F=maybe_infinite
Pour voir le CFG :
bin/toplevel.opt -lib-entry -main $F -deps -verbose tests/pdg/loops.c
bin/toplevel.opt -lib-entry -main $F -deps -verbose @PTEST_DIR@/loops.c
zgrviewer ./$F_cfg.dot
Pour voir les postdominateurs :
bin/toplevel.opt -lib-entry -main $F -fct-pdg $F -dot-postdom p tests/pdg/loops.c ;
bin/toplevel.opt -lib-entry -main $F -fct-pdg $F -dot-postdom p @PTEST_DIR@/loops.c ;
zgrviewer ./p.$F.dot
Pour voir le PDG :
bin/toplevel.opt -lib-entry -main $F -fct-pdg $F -pdg-dot pdg tests/pdg/loops.c ;
bin/toplevel.opt -lib-entry -main $F -fct-pdg $F -pdg-dot pdg @PTEST_DIR@/loops.c ;
zgrviewer ./pdg.$F.dot
*/
......@@ -123,7 +123,7 @@ L : n--;
return n;
}
/* this function is similar to [test_ctrl_dpd_multiple] in
* [tests/pdg/dpds_intra.c] but the value analysis converges,
* [@PTEST_DIR@/dpds_intra.c] but the value analysis converges,
* so we can see that [x=x+2;] has a control dependency on both [n<0] and [x<n].
*/
int non_natural_loop (int n) {
......
/* run.config
MODULE: @PTEST_NAME@
EXECNOW: LOG basic_sav.res LOG basic_sav.err BIN basic.sav @frama-c@ -eva @EVA_OPTIONS@ -out -input -deps @PTEST_FILE@ -save ./tests/saveload/result/basic.sav > ./tests/saveload/result/basic_sav.res 2> ./tests/saveload/result/basic_sav.err
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 ./tests/saveload/result/basic.1.sav @PTEST_FILE@ -eva @EVA_OPTIONS@ -out -input -deps > ./tests/saveload/result/basic_sav.1.res 2> ./tests/saveload/result/basic_sav.1.err
STDOPT: +"-load ./tests/saveload/result/basic.sav -eva @EVA_OPTIONS@ -out -input -deps"
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"
MODULE: @PTEST_NAME@
STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -print"
STDOPT: +"-load @PTEST_RESULT@/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps -print"
MODULE:
STDOPT: +"-load ./tests/saveload/result/basic.1.sav -eva @EVA_OPTIONS@ -out -input -deps"
STDOPT: +"-load @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 ./tests/saveload/result/status.sav @PTEST_FILE@ > ./tests/saveload/result/status_sav.res 2> ./tests/saveload/result/status_sav.err
STDOPT: +"-load ./tests/saveload/result/status.sav"
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"
MODULE:
STDOPT: +"-load ./tests/saveload/result/status.sav"
STDOPT: +"-load @PTEST_RESULT@/status.sav"
*/
int main() {
int i,j; i=10; /*@ assert (i == 10); */
......
/* run.config
EXECNOW: BIN bool.sav LOG bool_sav.res LOG bool_sav.err @frama-c@ -save ./tests/saveload/result/bool.sav -machdep x86_32 -eva @EVA_OPTIONS@ ./tests/saveload/bool.c > tests/saveload/result/bool_sav.res 2> tests/saveload/result/bool_sav.err
STDOPT: +"-load ./tests/saveload/result/bool.sav -out -input -deps"
STDOPT: +"-load ./tests/saveload/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@ @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@"
*/
#include "stdbool.h"
......
/* run.config
EXECNOW: LOG callbacks_initial.res LOG callbacks_initial.err BIN callbacks.sav @frama-c@ tests/saveload/callbacks.i -out -calldeps -eva-show-progress -main main1 -save ./tests/saveload/result/callbacks.sav > ./tests/saveload/result/callbacks_initial.res 2> ./tests/saveload/result/callbacks_initial.err
STDOPT: +"-load ./tests/saveload/result/callbacks.sav -main main2 -then -main main3"
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"
*/
/* This tests whether the callbacks for callwise inout and from survive after
......
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