[kernel] Parsing tests/rte/bool.i (no preprocessing)
[rte] annotating function g
[rte] annotating function ko1
[rte] annotating function ko2
/* Generated by Frama-C */
struct s_bool {
   char c ;
   _Bool b ;
};
struct s_bool sb;
_Bool ko1(void)
{
  _Bool __retres;
  char *p = & sb.c;
  /*@ assert rte: mem_access: \valid(p + 1); */
  *(p + 1) = (char)17;
  /*@ assert rte: bool_value: sb.b ≡ 0 ∨ sb.b ≡ 1; */
  __retres = sb.b;
  /*@ assert rte: bool_value: __retres ≡ 0 ∨ __retres ≡ 1; */
  return __retres;
}

_Bool ko2(void)
{
  _Bool b;
  char *p = (char *)(& b);
  /*@ assert rte: mem_access: \valid(p); */
  *p = (char)17;
  /*@ assert rte: bool_value: b ≡ 0 ∨ b ≡ 1; */
  return b;
}

extern _Bool f(void);

_Bool g(void)
{
  _Bool __retres;
  _Bool x = f();
  _Bool y = ko2();
  /*@ assert rte: bool_value: x ≡ 0 ∨ x ≡ 1; */
  if (x) {
    /*@ assert rte: bool_value: y ≡ 0 ∨ y ≡ 1; */
    __retres = y;
    goto return_label;
  }
  /*@ assert rte: bool_value: x ≡ 0 ∨ x ≡ 1; */
  __retres = x;
  return_label:
  /*@ assert rte: bool_value: __retres ≡ 0 ∨ __retres ≡ 1; */
  return __retres;
}