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

[tests] update oracles

parent ff09c192
......@@ -52,91 +52,97 @@ lemma emptying_stack_deterministic_trans{L}:
\at(aorai_n,L) ≡ 1 ∧ \at(aorai_CurOperation,L) ≡ op_pop ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ \at(aorai_n,L) > 1);
*/
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_in:
assumes
aorai_CurStates ≡ filled_stack ∨ aorai_CurStates ≡ empty_stack;
ensures aorai_CurStates ≡ filling_stack;
behavior buch_state_filling_stack_out:
assumes
aorai_CurStates ≢ filled_stack ∧ aorai_CurStates ≢ empty_stack;
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void push_pre_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
else
if (1 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_in:
assumes
aorai_CurStates ≡ filled_stack ∨ aorai_CurStates ≡ empty_stack;
ensures aorai_CurStates ≡ filling_stack;
behavior buch_state_filling_stack_out:
assumes
aorai_CurStates ≢ filled_stack ∧ aorai_CurStates ≢ empty_stack;
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void push_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_push;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
else
if (1 == aorai_CurStates) aorai_CurStates_tmp = filling_stack;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
/*@ requires aorai_CurStates ≡ filling_stack;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_in_0:
assumes aorai_CurStates ≡ filling_stack;
ensures aorai_CurStates ≡ filled_stack;
ensures aorai_n ≡ \old(aorai_n + 1);
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ filling_stack;
ensures aorai_CurStates ≢ filled_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void push_post_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) {
aorai_CurStates_tmp = filled_stack;
aorai_n ++;
*/
/*@ ghost
/@ requires aorai_CurStates ≡ filling_stack;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_push;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_in_0:
assumes aorai_CurStates ≡ filling_stack;
ensures aorai_CurStates ≡ filled_stack;
ensures aorai_n ≡ \old(aorai_n + 1);
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ filling_stack;
ensures aorai_CurStates ≢ filled_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void push_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_push;
aorai_CurStates_tmp = aorai_CurStates;
if (4 == aorai_CurStates) {
aorai_CurStates_tmp = filled_stack;
aorai_n ++;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
*/
/*@ requires
aorai_CurStates ≡ empty_stack ∨ aorai_CurStates ≡ filled_stack;
......@@ -158,109 +164,115 @@ void push_post_func(void)
*/
void push(void)
{
push_pre_func();
/*@ ghost push_pre_func(); */
g ++;
push_post_func();
/*@ ghost push_post_func(); */
return;
}
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_in:
assumes aorai_CurStates ≡ filled_stack ∧ aorai_n > 0;
ensures aorai_CurStates ≡ emptying_stack;
behavior buch_state_emptying_stack_out:
assumes aorai_CurStates ≢ filled_stack ∨ ¬(aorai_n > 0);
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void pop_pre_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates)
if (aorai_n > 0) aorai_CurStates_tmp = emptying_stack;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_in:
assumes aorai_CurStates ≡ filled_stack ∧ aorai_n > 0;
ensures aorai_CurStates ≡ emptying_stack;
behavior buch_state_emptying_stack_out:
assumes aorai_CurStates ≢ filled_stack ∨ ¬(aorai_n > 0);
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void pop_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
aorai_CurStates_tmp = aorai_CurStates;
if (3 == aorai_CurStates)
if (aorai_n > 0) aorai_CurStates_tmp = emptying_stack;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
/*@ requires aorai_CurStates ≡ emptying_stack;
requires
aorai_CurStates ≡ emptying_stack ⇒ aorai_n > 1 ∨ aorai_n ≡ 1;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n ≡ 1;
ensures aorai_CurStates ≡ empty_stack;
ensures aorai_n ≡ \old(aorai_n - 1);
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1);
ensures aorai_CurStates ≢ empty_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_in_0:
assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n > 1;
ensures aorai_CurStates ≡ filled_stack;
ensures aorai_n ≡ \old(aorai_n - 1);
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1);
ensures aorai_CurStates ≢ filled_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void pop_post_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
aorai_CurStates_tmp = aorai_CurStates;
if (2 == aorai_CurStates)
if (aorai_n > 1) {
aorai_CurStates_tmp = filled_stack;
aorai_n --;
}
if (2 == aorai_CurStates)
if (aorai_n == 1) {
aorai_CurStates_tmp = empty_stack;
aorai_n --;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
*/
/*@ ghost
/@ requires aorai_CurStates ≡ emptying_stack;
requires
aorai_CurStates ≡ emptying_stack ⇒ aorai_n > 1 ∨ aorai_n ≡ 1;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_pop;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n ≡ 1;
ensures aorai_CurStates ≡ empty_stack;
ensures aorai_n ≡ \old(aorai_n - 1);
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n ≡ 1);
ensures aorai_CurStates ≢ empty_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_in_0:
assumes aorai_CurStates ≡ emptying_stack ∧ aorai_n > 1;
ensures aorai_CurStates ≡ filled_stack;
ensures aorai_n ≡ \old(aorai_n - 1);
behavior buch_state_filled_stack_out:
assumes aorai_CurStates ≢ emptying_stack ∨ ¬(aorai_n > 1);
ensures aorai_CurStates ≢ filled_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void pop_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
aorai_CurStates_tmp = aorai_CurStates;
if (2 == aorai_CurStates)
if (aorai_n > 1) {
aorai_CurStates_tmp = filled_stack;
aorai_n --;
}
if (2 == aorai_CurStates)
if (aorai_n == 1) {
aorai_CurStates_tmp = empty_stack;
aorai_n --;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
*/
/*@ requires aorai_CurStates ≡ filled_stack;
requires aorai_CurStates ≡ filled_stack ⇒ aorai_n > 0;
......@@ -282,94 +294,100 @@ void pop_post_func(void)
*/
void pop(void)
{
pop_pre_func();
/*@ ghost pop_pre_func(); */
/*@ assert g > 0; */ ;
g --;
pop_post_func();
/*@ ghost pop_post_func(); */
return;
}
/*@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ init;
ensures aorai_CurStates ≡ empty_stack;
ensures aorai_n ≡ \old(0);
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ init;
ensures aorai_CurStates ≢ empty_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void main_pre_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (5 == aorai_CurStates) {
aorai_CurStates_tmp = empty_stack;
aorai_n = 0;
/*@ ghost
/@ ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_n, aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_out:
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_in_0:
assumes aorai_CurStates ≡ init;
ensures aorai_CurStates ≡ empty_stack;
ensures aorai_n ≡ \old(0);
behavior buch_state_empty_stack_out:
assumes aorai_CurStates ≢ init;
ensures aorai_CurStates ≢ empty_stack;
ensures aorai_n ≡ \old(aorai_n);
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void main_pre_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (5 == aorai_CurStates) {
aorai_CurStates_tmp = empty_stack;
aorai_n = 0;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
aorai_CurStates = aorai_CurStates_tmp;
return;
}
/*@ requires aorai_CurStates ≡ empty_stack;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_in:
assumes aorai_CurStates ≡ empty_stack;
ensures aorai_CurStates ≡ accept;
behavior buch_state_accept_out:
assumes aorai_CurStates ≢ empty_stack;
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
*/
void main_post_func(void)
{
/*@ ghost int aorai_CurStates_tmp; */
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates) aorai_CurStates_tmp = accept;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
*/
/*@ ghost
/@ requires aorai_CurStates ≡ empty_stack;
ensures aorai_CurOpStatus ≡ aorai_Terminated;
ensures aorai_CurOperation ≡ op_main;
assigns aorai_CurOpStatus, aorai_CurOperation, aorai_CurStates;
behavior buch_state_accept_in:
assumes aorai_CurStates ≡ empty_stack;
ensures aorai_CurStates ≡ accept;
behavior buch_state_accept_out:
assumes aorai_CurStates ≢ empty_stack;
ensures aorai_CurStates ≢ accept;
behavior buch_state_empty_stack_out:
ensures aorai_CurStates ≢ empty_stack;
behavior buch_state_emptying_stack_out:
ensures aorai_CurStates ≢ emptying_stack;
behavior buch_state_filled_stack_out:
ensures aorai_CurStates ≢ filled_stack;
behavior buch_state_filling_stack_out:
ensures aorai_CurStates ≢ filling_stack;
behavior buch_state_init_out:
ensures aorai_CurStates ≢ init;
@/
void main_post_func(void)
{
int aorai_CurStates_tmp;
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_main;
aorai_CurStates_tmp = aorai_CurStates;
if (1 == aorai_CurStates) aorai_CurStates_tmp = accept;
aorai_CurStates = aorai_CurStates_tmp;
return;
}
*/
/*@ requires aorai_CurStates ≡ init;
......@@ -381,7 +399,7 @@ void main_post_func(void)
*/
void main(void)
{
main_pre_func();
/*@ ghost main_pre_func(); */
push();
pop();
push();
......@@ -392,7 +410,7 @@ void main(void)
pop();
pop();
pop();
main_post_func();
/*@ ghost main_post_func(); */
return;
}
......
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