[kernel] Parsing inline_calls.i (no preprocessing)
[kernel:CERT:MSC:37] inline_calls.i:40: Warning: 
  Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
{
  int __retres;
  __retres = 2;
  return __retres;
}

__inline static int in_f__fc_inline(void)
{
  int __retres;
  __retres = 3;
  return __retres;
}

int volatile v;
int g(void)
{
  int __retres;
  if (v) {
    int tmp;
    {
       /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
      __retres_5 = 2;
      tmp = __retres_5;
    }
    __retres = tmp;
    goto return_label;
  }
  else {
    int tmp_0;
    {
       /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */int __retres_6;
      __retres_6 = 3;
      tmp_0 = __retres_6;
    }
    __retres = tmp_0;
    goto return_label;
  }
  return_label: return __retres;
}

int h(void)
{
  int tmp;
  {
     /* __blockattribute__(____fc_inlined__("g")) */int __retres;
    if (v) {
      int tmp_3;
      {
         /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
        __retres_5 = 2;
        tmp_3 = __retres_5;
      }
      __retres = tmp_3;
      goto return_label;
    }
    else {
      int tmp_0;
      {
         /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
        int __retres_6;
        __retres_6 = 3;
        tmp_0 = __retres_6;
      }
      __retres = tmp_0;
      goto return_label;
    }
    return_label: tmp = __retres;
  }
  return tmp;
}

int i(void)
{
  int __retres;
  /*@ assert i: \true; */ ;
  __retres = 0;
  return __retres;
}

int rec(int x_0)
{
  int __retres;
  int tmp;
  if (x_0 < 0) {
    __retres = x_0;
    goto return_label;
  }
  {
     /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
                                                      int tmp_6;
    int x_0_5 = x_0 - 1;
    if (x_0_5 < 0) {
      __retres_7 = x_0_5;
      goto return_label_0;
    }
    tmp_6 = rec(x_0_5 - 1);
    __retres_7 = tmp_6;
    return_label_0: tmp = __retres_7;
  }
  __retres = tmp;
  return_label: return __retres;
}

int f1(int a);

int g1(int a);

int volatile nondet;
int f1(int a)
{
  int __retres;
  if (nondet) {
    int __inline_tmp;
    {
       /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
      if (nondet) g1(4);
      __inline_tmp = a_5;
    }
  }
  else 
    if (nondet) {
      int __inline_tmp_6;
      {
         /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
        int a_8 = 2;
        if (nondet) {
          int __inline_tmp_10;
          {
             /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 = 1;
            if (nondet) g1(4);
            __inline_tmp_10 = a_5_11;
          }
        }
        else 
          if (nondet) {
            int __inline_tmp_6_12;
            f1(2);
          }
        /*@ assert missing_return: \false; */ ;
        __retres_9 = 0;
        __inline_tmp_6 = __retres_9;
      }
    }
  /*@ assert missing_return: \false; */ ;
  __retres = 0;
  return __retres;
}

int g1(int a)
{
  if (nondet) {
    int __inline_tmp;
    {
       /* __blockattribute__(____fc_inlined__("g1")) */int a_4 = 4;
      if (nondet) {
        int __inline_tmp_5;
        g1(4);
      }
      __inline_tmp = a_4;
    }
  }
  return a;
}

int main(void)
{
  int __inline_tmp_11;
  int __inline_tmp_8;
  int __inline_tmp;
  int tmp_1;
  {
     /* __blockattribute__(____fc_inlined__("i")) */int __retres;
    /*@ assert i: \true; */ ;
    __retres = 0;
    __inline_tmp = __retres;
  }
  int local_init = __inline_tmp;
  {
     /* __blockattribute__(____fc_inlined__("rec")) */int __retres_10;
                                                      int tmp;
    int x_0 = local_init;
    if (x_0 < 0) {
      __retres_10 = x_0;
      goto return_label;
    }
    {
       /* __blockattribute__(____fc_inlined__("rec")) */int __retres_7;
                                                        int tmp_6;
      int x_0_5 = x_0 - 1;
      if (x_0_5 < 0) {
        __retres_7 = x_0_5;
        goto return_label_0;
      }
      tmp_6 = rec(x_0_5 - 1);
      __retres_7 = tmp_6;
      return_label_0: tmp = __retres_7;
    }
    __retres_10 = tmp;
    return_label: __inline_tmp_8 = __retres_10;
  }
  int t = __inline_tmp_8;
  {
     /* __blockattribute__(____fc_inlined__("f1")) */int __retres_13;
    int a = 2;
    if (nondet) {
      int __inline_tmp_14;
      {
         /* __blockattribute__(____fc_inlined__("g1")) */int a_5 = 1;
        if (nondet) g1(4);
        __inline_tmp_14 = a_5;
      }
    }
    else 
      if (nondet) {
        int __inline_tmp_6;
        {
           /* __blockattribute__(____fc_inlined__("f1")) */int __retres_9;
          int a_8 = 2;
          if (nondet) {
            int __inline_tmp_10;
            {
               /* __blockattribute__(____fc_inlined__("g1")) */int a_5_11 =
                                                                 1;
              if (nondet) g1(4);
              __inline_tmp_10 = a_5_11;
            }
          }
          else 
            if (nondet) {
              int __inline_tmp_6_12;
              f1(2);
            }
          /*@ assert missing_return: \false; */ ;
          __retres_9 = 0;
          __inline_tmp_6 = __retres_9;
        }
      }
    /*@ assert missing_return: \false; */ ;
    __retres_13 = 0;
    __inline_tmp_11 = __retres_13;
  }
  {
     /* __blockattribute__(____fc_inlined__("h")) */int tmp_15;
    {
       /* __blockattribute__(____fc_inlined__("g")) */int __retres_16;
      if (v) {
        int tmp_3;
        {
           /* __blockattribute__(____fc_inlined__("f")) */int __retres_5;
          __retres_5 = 2;
          tmp_3 = __retres_5;
        }
        __retres_16 = tmp_3;
        goto return_label_1;
      }
      else {
        int tmp_0;
        {
           /* __blockattribute__(____fc_inlined__("in_f__fc_inline")) */
          int __retres_6;
          __retres_6 = 3;
          tmp_0 = __retres_6;
        }
        __retres_16 = tmp_0;
        goto return_label_1;
      }
      return_label_1: tmp_15 = __retres_16;
    }
    tmp_1 = tmp_15;
  }
  return tmp_1;
}

int with_static(void);

static int with_static_count = 0;
int with_static(void)
{
  with_static_count ++;
  return with_static_count;
}

int call_with_static(void)
{
  int tmp;
  {
     /* __blockattribute__(____fc_inlined__("with_static")) */with_static_count ++;
    tmp = with_static_count;
  }
  return tmp;
}

void builtin_acsl(void)
{
  float g_0 = 0.f;
  /*@ assert ¬\is_NaN(g_0); */ ;
  return;
}

void call_builtin_acsl(void)
{
  {
     /* __blockattribute__(____fc_inlined__("builtin_acsl")) */float g_0 =
                                                                 0.f;
    /*@ assert ¬\is_NaN(g_0); */ ;
    ;
  }
  return;
}

void f_slevel(void)
{
  /*@ slevel 0; */ ;
  return;
}

void call_f_slevel(void)
{
  {
     /* __blockattribute__(____fc_inlined__("f_slevel")) *//*@ slevel 0; */ ;
    ;
  }
  return;
}

void pre_decl(void);

extern int x;

int y;

void post_decl(void);

void middle_decl(void)
{
  {
     /* __blockattribute__(____fc_inlined__("pre_decl")) */x ++;
    y ++;
    post_decl();
    ;
  }
  return;
}

void post_decl(void);

int y = 23;
void pre_decl(void)
{
  x ++;
  y ++;
  post_decl();
  return;
}