gen_bts1326.c

/* Generated by Frama-C */
typedef int ArrayInt[5];
/*@ ensures
      *\old(AverageAccel) ≡
      (((((*\old(Accel))[4] + (*\old(Accel))[3]) + (*\old(Accel))[2]) +
        (*\old(Accel))[1])
       + (*\old(Accel))[0])
      / 5;
 */
void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
                                                 int *AverageAccel);

/*@ ensures
      *\old(AverageAccel) ≡
      (((((*\old(Accel))[4] + (*\old(Accel))[3]) + (*\old(Accel))[2]) +
        (*\old(Accel))[1])
       + (*\old(Accel))[0])
      / 5;
 */
void atp_NORMAL_computeAverageAccel(ArrayInt *Accel, int *AverageAccel)
{
  __e_acsl_store_block((void *)(& Accel),8UL);
  __e_acsl_store_block((void *)(& AverageAccel),8UL);
  __e_acsl_initialize((void *)AverageAccel,sizeof(int));
  *AverageAccel = (((((*Accel)[4] + (*Accel)[3]) + (*Accel)[2]) + (*Accel)[1]) + (*Accel)[0]) / 5;
  __e_acsl_delete_block((void *)(& Accel));
  __e_acsl_delete_block((void *)(& AverageAccel));
  return;
}

int main(void)
{
  int __retres;
  ArrayInt Accel;
  int av;
  __e_acsl_memory_init((int *)0,(char ***)0,8UL);
  __e_acsl_store_block((void *)(& av),4UL);
  __e_acsl_store_block((void *)(Accel),20UL);
  __e_acsl_initialize((void *)(Accel),sizeof(int));
  Accel[0] = 1;
  __e_acsl_initialize((void *)(& Accel[1]),sizeof(int));
  Accel[1] = 2;
  __e_acsl_initialize((void *)(& Accel[2]),sizeof(int));
  Accel[2] = 3;
  __e_acsl_initialize((void *)(& Accel[3]),sizeof(int));
  Accel[3] = 4;
  __e_acsl_initialize((void *)(& Accel[4]),sizeof(int));
  Accel[4] = 5;
  __gen_e_acsl_atp_NORMAL_computeAverageAccel(& Accel,& av);
  __retres = 0;
  __e_acsl_delete_block((void *)(& av));
  __e_acsl_delete_block((void *)(Accel));
  __e_acsl_memory_clean();
  return __retres;
}

/*@ ensures
      *\old(AverageAccel) ≡
      (((((*\old(Accel))[4] + (*\old(Accel))[3]) + (*\old(Accel))[2]) +
        (*\old(Accel))[1])
       + (*\old(Accel))[0])
      / 5;
 */
void __gen_e_acsl_atp_NORMAL_computeAverageAccel(ArrayInt *Accel,
                                                 int *AverageAccel)
{
  ArrayInt *__gen_e_acsl_at_6;
  ArrayInt *__gen_e_acsl_at_5;
  ArrayInt *__gen_e_acsl_at_4;
  ArrayInt *__gen_e_acsl_at_3;
  ArrayInt *__gen_e_acsl_at_2;
  int *__gen_e_acsl_at;
  __e_acsl_store_block((void *)(& Accel),8UL);
  __e_acsl_store_block((void *)(& AverageAccel),8UL);
  __gen_e_acsl_at_6 = Accel;
  __gen_e_acsl_at_5 = Accel;
  __gen_e_acsl_at_4 = Accel;
  __gen_e_acsl_at_3 = Accel;
  __gen_e_acsl_at_2 = Accel;
  __gen_e_acsl_at = AverageAccel;
  atp_NORMAL_computeAverageAccel(Accel,AverageAccel);
  {
    int __gen_e_acsl_valid_read;
    int __gen_e_acsl_valid_read_2;
    int __gen_e_acsl_valid_read_3;
    int __gen_e_acsl_valid_read_4;
    int __gen_e_acsl_valid_read_5;
    int __gen_e_acsl_valid_read_6;
    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(*__gen_e_acsl_at_6),
                                                  sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read((int *)*__gen_e_acsl_at_6)",
                    8);
    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_5)[1]),
                                                    sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_5)[1])",
                    8);
    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_4)[2]),
                                                    sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_4)[2])",
                    8);
    __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_3)[3]),
                                                    sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_3)[3])",
                    8);
    __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)(& (*__gen_e_acsl_at_2)[4]),
                                                    sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read(&(*__gen_e_acsl_at_2)[4])",
                    8);
    __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
                                                    sizeof(int));
    __e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",8);
    __e_acsl_assert(*__gen_e_acsl_at == (int)((((((*__gen_e_acsl_at_2)[4] + (long)(*__gen_e_acsl_at_3)[3]) + (*__gen_e_acsl_at_4)[2]) + (*__gen_e_acsl_at_5)[1]) + (*__gen_e_acsl_at_6)[0]) / 5L),
                    (char *)"Postcondition",
                    (char *)"atp_NORMAL_computeAverageAccel",
                    (char *)"*\\old(AverageAccel) ==\n(((((*\\old(Accel))[4] + (*\\old(Accel))[3]) + (*\\old(Accel))[2]) +\n  (*\\old(Accel))[1])\n + (*\\old(Accel))[0])\n/ 5",
                    8);
    __e_acsl_delete_block((void *)(& Accel));
    __e_acsl_delete_block((void *)(& AverageAccel));
    return;
  }
}