[kernel] Parsing cert_exp46.i (no preprocessing)
[kernel:CERT:EXP:46] cert_exp46.i:5: Warning: 
  operand of bitwise operator is a logical relation
[kernel:CERT:EXP:46] cert_exp46.i:11: Warning: 
  operand of bitwise operator is a logical relation
[kernel:CERT:EXP:46] cert_exp46.i:11: Warning: 
  operand of bitwise operator is a logical relation
[kernel:CERT:EXP:46] cert_exp46.i:17: Warning: 
  operand of bitwise operator has boolean type
[kernel:CERT:EXP:46] cert_exp46.i:17: Warning: 
  operand of bitwise operator has boolean type
/* Generated by Frama-C */
extern int f(void);

extern int g(void);

int non_compliant_1(void)
{
  int __retres;
  int tmp_0;
  int tmp;
  int tmp_1;
  tmp = f();
  if (tmp) tmp_0 = 0; else tmp_0 = 1;
  tmp_1 = g();
  if (tmp_0 & (tmp_1 == 0)) {
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

int non_compliant_2(void)
{
  int __retres;
  int tmp_1;
  int tmp_2;
  int x = f();
  int y = g();
  tmp_1 = x;
  x ++;
  tmp_2 = y;
  y --;
  ;
  if ((tmp_1 == 0) | (tmp_2 == 0)) {
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

int non_compliant_3(void)
{
  int __retres;
  int tmp;
  int tmp_0;
  tmp = f();
  _Bool b = (_Bool)(tmp != 0);
  tmp_0 = g();
  _Bool c = (_Bool)(tmp_0 != 0);
  if ((int)b ^ (int)c) {
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}

int compliant_1(void)
{
  int __retres;
  int tmp;
  tmp = f();
  if (tmp) {
    __retres = 0;
    goto return_label;
  }
  else {
    int tmp_0;
    tmp_0 = g();
    if (tmp_0 == 0) {
      __retres = 1;
      goto return_label;
    }
    else {
      __retres = 0;
      goto return_label;
    }
  }
  return_label: return __retres;
}

int compliant_2(void)
{
  int __retres;
  int tmp_1;
  int x = f();
  int y = g();
  tmp_1 = x;
  x ++;
  ;
  if (tmp_1 == 0) {
    __retres = 1;
    goto return_label;
  }
  else {
    int tmp_2;
    tmp_2 = y;
    y --;
    ;
    if (tmp_2 == 0) {
      __retres = 1;
      goto return_label;
    }
    else {
      __retres = 0;
      goto return_label;
    }
  }
  return_label: return __retres;
}

int compliant_3(void)
{
  int __retres;
  int tmp;
  int tmp_0;
  tmp = f();
  _Bool b = (_Bool)(tmp != 0);
  tmp_0 = g();
  _Bool c = (_Bool)(tmp_0 != 0);
  if (b) goto _LOR;
  else 
    if (c) {
      _LOR: ;
      if (b) 
        if (c) {
          __retres = 0;
          goto return_label;
        }
        else {
          __retres = 1;
          goto return_label;
        }
      else {
        __retres = 1;
        goto return_label;
      }
    }
    else {
      __retres = 0;
      goto return_label;
    }
  return_label: return __retres;
}

int compliant_4(void)
{
  int __retres;
  int tmp;
  int tmp_0;
  tmp = f();
  _Bool b = (_Bool)(tmp != 0);
  tmp_0 = g();
  _Bool c = (_Bool)(tmp_0 != 0);
  if ((int)b ^ (int)c) {
    __retres = 1;
    goto return_label;
  }
  else {
    __retres = 0;
    goto return_label;
  }
  return_label: return __retres;
}