gen_bts1307.c

/* Generated by Frama-C */
#include "stdlib.h"
/*@ requires \valid(Mtmax_in);
    requires \valid(Mwmax);
    requires \valid(Mtmax_out);
    
    behavior OverEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmax_out) ≡
        *\old(Mtmax_in) + (5 - ((5 / 80) * *\old(Mwmax)) * 0.4);
 */
void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out);

/*@ requires \valid(Mtmax_in);
    requires \valid(Mwmax);
    requires \valid(Mtmax_out);
    
    behavior OverEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmax_out) ≡
        *\old(Mtmax_in) + (5 - ((5 / 80) * *\old(Mwmax)) * 0.4);
 */
void foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
  __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
  __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
  __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
  __e_acsl_initialize((void *)Mtmax_out,sizeof(float));
  *Mtmax_out = (float)((double)*Mtmax_in + ((double)5 - (double)((float)(
                                                                 5 / 80) * *Mwmax) * 0.4));
  __e_acsl_delete_block((void *)(& Mtmax_in));
  __e_acsl_delete_block((void *)(& Mwmax));
  __e_acsl_delete_block((void *)(& Mtmax_out));
  return;
}

/*@ requires \valid(Mtmin_in);
    requires \valid(Mwmin);
    requires \valid(Mtmin_out);
    
    behavior UnderEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85 * *\old(Mwmin)?
          *\old(Mtmin_in) ≢ 0.:
          0.85 * *\old(Mwmin) ≢ 0.;
 */
void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out);

/*@ requires \valid(Mtmin_in);
    requires \valid(Mwmin);
    requires \valid(Mtmin_out);
    
    behavior UnderEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85 * *\old(Mwmin)?
          *\old(Mtmin_in) ≢ 0.:
          0.85 * *\old(Mwmin) ≢ 0.;
 */
void bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
  __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
  __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
  __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
  __e_acsl_initialize((void *)Mtmin_out,sizeof(float));
  *Mtmin_out = (float)(0.85 * (double)*Mwmin);
  __e_acsl_delete_block((void *)(& Mtmin_in));
  __e_acsl_delete_block((void *)(& Mwmin));
  __e_acsl_delete_block((void *)(& Mtmin_out));
  return;
}

int main(void)
{
  int __retres;
  float f;
  float g;
  float h;
  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
  __e_acsl_store_block((void *)(& h),(size_t)4);
  __e_acsl_store_block((void *)(& g),(size_t)4);
  __e_acsl_store_block((void *)(& f),(size_t)4);
  __e_acsl_full_init((void *)(& f));
  f = (float)1.0;
  __e_acsl_full_init((void *)(& g));
  g = (float)1.0;
  __gen_e_acsl_foo(& f,& g,& h);
  __gen_e_acsl_bar(& f,& g,& h);
  __retres = 0;
  __e_acsl_delete_block((void *)(& h));
  __e_acsl_delete_block((void *)(& g));
  __e_acsl_delete_block((void *)(& f));
  __e_acsl_memory_clean();
  return __retres;
}

/*@ requires \valid(Mtmin_in);
    requires \valid(Mwmin);
    requires \valid(Mtmin_out);
    
    behavior UnderEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmin_out) ≡ *\old(Mtmin_in) < 0.85 * *\old(Mwmin)?
          *\old(Mtmin_in) ≢ 0.:
          0.85 * *\old(Mwmin) ≢ 0.;
 */
void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
{
  float *__gen_e_acsl_at_6;
  float *__gen_e_acsl_at_5;
  float *__gen_e_acsl_at_4;
  float *__gen_e_acsl_at_3;
  float *__gen_e_acsl_at_2;
  float *__gen_e_acsl_at;
  {
    int __gen_e_acsl_valid;
    int __gen_e_acsl_valid_2;
    int __gen_e_acsl_valid_3;
    __e_acsl_store_block((void *)(& Mtmin_in),(size_t)8);
    __e_acsl_store_block((void *)(& Mwmin),(size_t)8);
    __e_acsl_store_block((void *)(& Mtmin_out),(size_t)8);
    __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmin_in,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"bar",
                    (char *)"\\valid(Mtmin_in)",17);
    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmin,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
                    (char *)"bar",(char *)"\\valid(Mwmin)",18);
    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmin_out,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
                    (char *)"bar",(char *)"\\valid(Mtmin_out)",19);
    __gen_e_acsl_at_6 = Mwmin;
    __gen_e_acsl_at_5 = Mtmin_in;
    __gen_e_acsl_at_4 = Mwmin;
    __gen_e_acsl_at_3 = Mtmin_in;
    __gen_e_acsl_at_2 = Mtmin_in;
    __gen_e_acsl_at = Mtmin_out;
    bar(Mtmin_in,Mwmin,Mtmin_out);
  }
  {
    int __gen_e_acsl_valid_read;
    int __gen_e_acsl_valid_read_2;
    int __gen_e_acsl_and;
    int __gen_e_acsl_if;
    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
                                                  sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"bar",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",23);
    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
                                                    sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"bar",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",23);
    if (*__gen_e_acsl_at == *__gen_e_acsl_at_2) {
      int __gen_e_acsl_valid_read_3;
      int __gen_e_acsl_valid_read_4;
      __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at_4,
                                                      sizeof(float));
      __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"bar",
                      (char *)"mem_access: \\valid_read(__gen_e_acsl_at_4)",
                      23);
      __gen_e_acsl_valid_read_4 = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
                                                      sizeof(float));
      __e_acsl_assert(__gen_e_acsl_valid_read_4,(char *)"RTE",(char *)"bar",
                      (char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",
                      23);
      __gen_e_acsl_and = *__gen_e_acsl_at_3 < 0.85 * *__gen_e_acsl_at_4;
    }
    else __gen_e_acsl_and = 0;
    if (__gen_e_acsl_and) {
      int __gen_e_acsl_valid_read_5;
      __gen_e_acsl_valid_read_5 = __e_acsl_valid_read((void *)__gen_e_acsl_at_5,
                                                      sizeof(float));
      __e_acsl_assert(__gen_e_acsl_valid_read_5,(char *)"RTE",(char *)"bar",
                      (char *)"mem_access: \\valid_read(__gen_e_acsl_at_5)",
                      23);
      __gen_e_acsl_if = *__gen_e_acsl_at_5 != 0.;
    }
    else {
      int __gen_e_acsl_valid_read_6;
      __gen_e_acsl_valid_read_6 = __e_acsl_valid_read((void *)__gen_e_acsl_at_6,
                                                      sizeof(float));
      __e_acsl_assert(__gen_e_acsl_valid_read_6,(char *)"RTE",(char *)"bar",
                      (char *)"mem_access: \\valid_read(__gen_e_acsl_at_6)",
                      23);
      __gen_e_acsl_if = 0.85 * *__gen_e_acsl_at_6 != 0.;
    }
    __e_acsl_assert(__gen_e_acsl_if,(char *)"Postcondition",(char *)"bar",
                    (char *)"*\\old(Mtmin_out) == *\\old(Mtmin_in) < 0.85 * *\\old(Mwmin)?\n  *\\old(Mtmin_in) != 0.:\n  0.85 * *\\old(Mwmin) != 0.",
                    23);
    __e_acsl_delete_block((void *)(& Mtmin_in));
    __e_acsl_delete_block((void *)(& Mwmin));
    __e_acsl_delete_block((void *)(& Mtmin_out));
    return;
  }
}

/*@ requires \valid(Mtmax_in);
    requires \valid(Mwmax);
    requires \valid(Mtmax_out);
    
    behavior OverEstimate_Motoring:
      assumes \true;
      ensures
        *\old(Mtmax_out) ≡
        *\old(Mtmax_in) + (5 - ((5 / 80) * *\old(Mwmax)) * 0.4);
 */
void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
{
  float *__gen_e_acsl_at_3;
  float *__gen_e_acsl_at_2;
  float *__gen_e_acsl_at;
  {
    int __gen_e_acsl_valid;
    int __gen_e_acsl_valid_2;
    int __gen_e_acsl_valid_3;
    __e_acsl_store_block((void *)(& Mtmax_in),(size_t)8);
    __e_acsl_store_block((void *)(& Mwmax),(size_t)8);
    __e_acsl_store_block((void *)(& Mtmax_out),(size_t)8);
    __gen_e_acsl_valid = __e_acsl_valid((void *)Mtmax_in,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"foo",
                    (char *)"\\valid(Mtmax_in)",5);
    __gen_e_acsl_valid_2 = __e_acsl_valid((void *)Mwmax,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Precondition",
                    (char *)"foo",(char *)"\\valid(Mwmax)",6);
    __gen_e_acsl_valid_3 = __e_acsl_valid((void *)Mtmax_out,sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_3,(char *)"Precondition",
                    (char *)"foo",(char *)"\\valid(Mtmax_out)",7);
    __gen_e_acsl_at_3 = Mwmax;
    __gen_e_acsl_at_2 = Mtmax_in;
    __gen_e_acsl_at = Mtmax_out;
    foo(Mtmax_in,Mwmax,Mtmax_out);
  }
  {
    int __gen_e_acsl_valid_read;
    int __gen_e_acsl_valid_read_2;
    int __gen_e_acsl_valid_read_3;
    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)__gen_e_acsl_at_3,
                                                  sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"foo",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_3)",11);
    __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)__gen_e_acsl_at_2,
                                                    sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",(char *)"foo",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at_2)",11);
    __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)__gen_e_acsl_at,
                                                    sizeof(float));
    __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"foo",
                    (char *)"mem_access: \\valid_read(__gen_e_acsl_at)",11);
    __e_acsl_assert(*__gen_e_acsl_at == *__gen_e_acsl_at_2 + ((long double)5 - 
                                                              ((long double)(
                                                               5 / 80) * *__gen_e_acsl_at_3) * 0.4),
                    (char *)"Postcondition",(char *)"foo",
                    (char *)"*\\old(Mtmax_out) == *\\old(Mtmax_in) + (5 - ((5 / 80) * *\\old(Mwmax)) * 0.4)",
                    11);
    __e_acsl_delete_block((void *)(& Mtmax_in));
    __e_acsl_delete_block((void *)(& Mwmax));
    __e_acsl_delete_block((void *)(& Mtmax_out));
    return;
  }
}