gen_bts2192.c

/* Generated by Frama-C */
int a;
char *n = (char *)"134";
int main(int argc, char **argv)
{
  int __retres;
  { /* sequence */
    argc = __gen_e_acsl_atoi((char const *)n);
    a = argc;
  }
  __retres = 0;
  return __retres;
}