Commit 44b4c498 authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Virgile Prevosto
Browse files

[Aorai] update test oracles

parent b902e2f3
......@@ -25,24 +25,24 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
/*@ lemma i_0_deterministic_trans{L}: \true;
/*@ check lemma i_0_deterministic_trans{L}: \true;
*/
/*@ lemma h_0_deterministic_trans{L}: \true;
/*@ check lemma h_0_deterministic_trans{L}: \true;
*/
/*@ lemma g_0_deterministic_trans{L}: \true;
/*@ check lemma g_0_deterministic_trans{L}: \true;
*/
/*@ lemma f_0_deterministic_trans{L}: \true;
/*@ check lemma f_0_deterministic_trans{L}: \true;
*/
/*@ lemma d_deterministic_trans{L}: \true;
/*@ check lemma d_deterministic_trans{L}: \true;
*/
/*@ lemma c_deterministic_trans{L}: \true;
/*@ check lemma c_deterministic_trans{L}: \true;
*/
/*@ lemma a_deterministic_trans{L}: \true;
/*@ check lemma a_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
lemma b_deterministic_trans{L}:
check lemma b_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
\at(aorai_CurOperation,L) ≡ op_f ∧
......@@ -51,7 +51,7 @@ lemma b_deterministic_trans{L}:
/*@ ghost int aorai_CurStates = a; */
/*@ ghost int aorai_x = 0; */
/*@
lemma e_deterministic_trans{L}:
check lemma e_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
\at(aorai_CurOperation,L) ≡ op_h ∧
......
......@@ -20,17 +20,17 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
/*@ lemma init_deterministic_trans{L}: \true;
/*@ check lemma init_deterministic_trans{L}: \true;
*/
/*@ lemma filling_stack_deterministic_trans{L}: \true;
/*@ check lemma filling_stack_deterministic_trans{L}: \true;
*/
/*@ lemma accept_deterministic_trans{L}: \true;
/*@ check lemma accept_deterministic_trans{L}: \true;
*/
int g = 0;
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
lemma empty_stack_deterministic_trans{L}:
check lemma empty_stack_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_push ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
\at(aorai_CurOperation,L) ≡ op_main ∧
......@@ -39,14 +39,14 @@ lemma empty_stack_deterministic_trans{L}:
/*@ ghost int aorai_CurStates = init; */
/*@ ghost int aorai_n = 0; */
/*@
lemma filled_stack_deterministic_trans{L}:
check lemma filled_stack_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_pop ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ \at(aorai_n,L) > 0 ∧
\at(aorai_CurOperation,L) ≡ op_push ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called);
*/
/*@
lemma emptying_stack_deterministic_trans{L}:
check lemma emptying_stack_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_pop ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
\at(aorai_n,L) ≡ 1 ∧ \at(aorai_CurOperation,L) ≡ op_pop ∧
......
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