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

[aorai tests] adds DEPS directive and %{dep:file}

parent 4e1af746
No related branches found
No related tags found
No related merge requests found
Showing
with 23 additions and 24 deletions
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct S { int x; };
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/assigns_det.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
MODULE: name_projects
LIBS:
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -then -print
*/
int X;
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@-2.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void a(void) {}
......@@ -11,4 +11,3 @@ void main(void)
for (int i=0; i<10; ++i)
a();
}
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int X;
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) { return x; }
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void)
{
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) { }
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(){};
......
/* run.config*
EXIT: 1
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void) {}
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
......
/* run.config*
EXIT: 1
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
void g(void) {}
......
/* run.config
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) {}
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) {
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int x=0;
......
/* run.config
NOFRAMAC:
LIBS:
EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @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.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
*/
/* run.config_prove
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() { }
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() {}
......
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