void main(void)
{
	//@ loop assigns i;
	for (int i=0; i<10; ++i)
		;
}

/* 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;
}