gen_bts2191.c

/* Generated by Frama-C */
char *__gen_e_acsl_literal_string;
char *__gen_e_acsl_literal_string_2;
struct ST {
   char *str ;
   int num ;
};
struct ST _G[2] =
  {{.str = (char *)"Struct_G[0]", .num = 99},
   {.str = (char *)"Struct_G[1]", .num = 147}};
void __e_acsl_globals_init(void)
{
  __gen_e_acsl_literal_string = "Struct_G[1]";
  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
                       sizeof("Struct_G[1]"));
  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
  __gen_e_acsl_literal_string_2 = "Struct_G[0]";
  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
                       sizeof("Struct_G[0]"));
  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
  __e_acsl_store_block((void *)(_G),32UL);
  __e_acsl_full_init((void *)(& _G));
  return;
}

int main(int argc, char **argv)
{
  int __retres;
  __e_acsl_memory_init(& argc,& argv,8UL);
  __e_acsl_globals_init();
  /*@ assert \valid_read(_G[0].str); */
  {
    {
      int __gen_e_acsl_initialized;
      int __gen_e_acsl_and;
      __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0].str),
                                                      sizeof(char *));
      if (__gen_e_acsl_initialized) {
        int __gen_e_acsl_valid_read;
        __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
                                                      sizeof(char));
        __gen_e_acsl_and = __gen_e_acsl_valid_read;
      }
      else __gen_e_acsl_and = 0;
      __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
                      (char *)"\\valid_read(_G[0].str)",22);
    }
  }
  __retres = 0;
  __e_acsl_delete_block((void *)(_G));
  __e_acsl_memory_clean();
  return __retres;
}