inline_calls.0.res.oracle

[kernel] Parsing tests/syntax/inline_calls.i (no preprocessing)
[kernel] tests/syntax/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;
    {
      int __retres_5;
      __retres_5 = 2;
      tmp = __retres_5;
    }
    __retres = tmp;
    goto return_label;
  }
  else {
    int tmp_0;
    {
      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;
  {
    int __retres;
    if (v) {
      int tmp_3;
      {
        int __retres_5;
        __retres_5 = 2;
        tmp_3 = __retres_5;
      }
      __retres = tmp_3;
      goto return_label;
    }
    else {
      int tmp_0;
      {
        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;
  }
  {
    int __retres_6;
    int tmp_5;
    int x_0_7 = x_0 - 1;
    if (x_0_7 < 0) {
      __retres_6 = x_0_7;
      goto return_label_0;
    }
    tmp_5 = rec(x_0_7 - 1);
    __retres_6 = tmp_5;
    return_label_0: tmp = __retres_6;
  }
  __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;
    {
      int a_5 = 1;
      if (nondet) g1(4);
      __inline_tmp = a_5;
    }
  }
  else 
    if (nondet) {
      int __inline_tmp_6;
      {
        int __retres_8;
        int a_12 = 2;
        if (nondet) {
          int __inline_tmp_9;
          {
            int a_5_10 = 1;
            if (nondet) g1(4);
            __inline_tmp_9 = a_5_10;
          }
        }
        else 
          if (nondet) {
            int __inline_tmp_6_11;
            f1(2);
          }
        /*@ assert missing_return: \false; */ ;
        __retres_8 = 0;
        __inline_tmp_6 = __retres_8;
      }
    }
  /*@ assert missing_return: \false; */ ;
  __retres = 0;
  return __retres;
}

int g1(int a)
{
  if (nondet) {
    int __inline_tmp;
    {
      int a_5 = 4;
      if (nondet) {
        int __inline_tmp_4;
        g1(4);
      }
      __inline_tmp = a_5;
    }
  }
  return a;
}

int main(void)
{
  int __inline_tmp_11;
  int __inline_tmp_8;
  int __inline_tmp;
  int tmp_1;
  {
    int __retres;
    /*@ assert i: \true; */ ;
    __retres = 0;
    __inline_tmp = __retres;
  }
  int local_init = __inline_tmp;
  {
    int __retres_10;
    int tmp;
    int x_0 = local_init;
    if (x_0 < 0) {
      __retres_10 = x_0;
      goto return_label;
    }
    {
      int __retres_6;
      int tmp_5;
      int x_0_7 = x_0 - 1;
      if (x_0_7 < 0) {
        __retres_6 = x_0_7;
        goto return_label_0;
      }
      tmp_5 = rec(x_0_7 - 1);
      __retres_6 = tmp_5;
      return_label_0: tmp = __retres_6;
    }
    __retres_10 = tmp;
    return_label: __inline_tmp_8 = __retres_10;
  }
  int t = __inline_tmp_8;
  {
    int __retres_13;
    int a = 2;
    if (nondet) {
      int __inline_tmp_14;
      {
        int a_5 = 1;
        if (nondet) g1(4);
        __inline_tmp_14 = a_5;
      }
    }
    else 
      if (nondet) {
        int __inline_tmp_6;
        {
          int __retres_8;
          int a_12 = 2;
          if (nondet) {
            int __inline_tmp_9;
            {
              int a_5_10 = 1;
              if (nondet) g1(4);
              __inline_tmp_9 = a_5_10;
            }
          }
          else 
            if (nondet) {
              int __inline_tmp_6_11;
              f1(2);
            }
          /*@ assert missing_return: \false; */ ;
          __retres_8 = 0;
          __inline_tmp_6 = __retres_8;
        }
      }
    /*@ assert missing_return: \false; */ ;
    __retres_13 = 0;
    __inline_tmp_11 = __retres_13;
  }
  {
    int tmp_15;
    {
      int __retres_16;
      if (v) {
        int tmp_3;
        {
          int __retres_5;
          __retres_5 = 2;
          tmp_3 = __retres_5;
        }
        __retres_16 = tmp_3;
        goto return_label_1;
      }
      else {
        int tmp_0;
        {
          int __retres_6_17;
          __retres_6_17 = 3;
          tmp_0 = __retres_6_17;
        }
        __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;
  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)
{
  {
    float g_0 = 0.f;
    /*@ assert ¬\is_NaN(g_0); */ ;
    ;
  }
  return;
}

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

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

void pre_decl(void);

extern int x;

int y;

void post_decl(void);

void middle_decl(void)
{
  x ++;
  y ++;
  post_decl();
  ;
  return;
}

void post_decl(void);

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