Commit f8f4b28e authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] post-rebase update of tests introduced in the metavariable branch

parent 44b4c498
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void) {}
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
......
/* run.config*
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
......
[kernel] Parsing tests/aorai/metavariables-incompatible.i (no preprocessing)
[kernel] Parsing tests/ya/metavariables-incompatible.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The use of metavariables is incompatible with non-deterministic automata, such as automa using extended transitions.
[kernel] Plug-in aorai aborted: invalid user input.
[kernel] Parsing tests/aorai/metavariables-right.i (no preprocessing)
[kernel] Parsing tests/ya/metavariables-right.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_metavariables-right_0.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
......@@ -59,7 +59,8 @@ check lemma e_deterministic_trans{L}:
*/
/*@ ghost int aorai_y = 0; */
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ b;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_f;
assigns aorai_y, aorai_x, aorai_CurOpStatus, aorai_CurOperation,
aorai_CurStates;
......@@ -187,7 +188,8 @@ void f(int x)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ b;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_g;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......@@ -300,7 +302,9 @@ void g(void)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ e;
requires aorai_CurStates ≡ e ⇒ aorai_x > 0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_h;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......@@ -415,7 +419,8 @@ void h(int x)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ g_0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_i;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......@@ -543,7 +548,8 @@ void i(void)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ a;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......
[kernel] Parsing tests/aorai/metavariables-wrong.i (no preprocessing)
[kernel] Parsing tests/ya/metavariables-wrong.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] User Error: The metavariables aorai_x may not be initialized before the transition from e to f_0:
(Call(h))
......
[kernel] Parsing tests/aorai/stack.i (no preprocessing)
[kernel] Parsing tests/ya/stack.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_stack_0.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
......@@ -53,7 +53,9 @@ check lemma emptying_stack_deterministic_trans{L}:
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_n,L) > 1);
*/
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires
aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≡ filled_stack;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......@@ -171,7 +173,9 @@ void push(void)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ filled_stack;
requires aorai_CurStates ≡ filled_stack ⇒ aorai_n > 0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......@@ -302,7 +306,8 @@ void pop(void)
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
/@ requires aorai_CurStates ≡ init;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
......
/* run.config*
OPT: -aorai-automata tests/aorai/stack.ya -aorai-test 1 -load-module tests/aorai/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment