ftest_annot.c (1,773 bytes)
2012-10-25 19:01
/* Generated by Frama-C */
//****************
//* BEGIN Primitives generated for LTL verification
//*
//*
//* Some constants
enum aorai_ListOper {
op_main = 0
};
enum aorai_ListOper aorai_CurOperation = op_main;
enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called;
//*
//* States and Trans Variables
int S = 1;
//*
//* Loops management
int aorai_Loop_Init_11 = 0;
//*
//******************
//* Auxiliary variables used in transition conditions
//*
//*
//* END Primitives generated for LTL verification
//****************
/*@ ensures aorai_CurOpStatus == aorai_Called;
ensures aorai_CurOperation == op_main;
assigns aorai_CurOpStatus, aorai_CurOperation,
S;
behavior buch_state_S_in:
assumes 1 == S;
ensures 1 == S;
behavior buch_state_S_out:
assumes 0 == S;
ensures 0 == S;
*/
void main_pre_func(void);
/*@ requires 1 == S;
ensures aorai_CurOpStatus == aorai_Terminated;
ensures aorai_CurOperation == op_main;
assigns aorai_CurOpStatus, aorai_CurOperation,
S;
behavior buch_state_S_in:
assumes 1 == S;
ensures 1 == S;
behavior buch_state_S_out:
assumes 0 == S;
ensures 0 == S;
*/
void main_post_func(void);
/*@ requires 1 == S;
behavior Buchi_property_behavior:
ensures \true;
ensures 1 == S;
*/
void main(void)
{
int i;
main_pre_func();
i = 0;
/*@ ghost aorai_Loop_Init_11 = 1; */
/*@ loop assigns i;
loop invariant 1 == S; */
while (1) {
if (! (i < 10)) { goto while_0_break; }
/*@ ghost aorai_Loop_Init_11 = 0; */
i ++;
}
while_0_break: /* internal */ ;
main_post_func();
return;
}