bts1553_2.res.oracle

[kernel] Parsing bts1553_2.i (no preprocessing)
[kernel:file:print-one] 
  result of parsing bts1553_2.i:
  /* Generated by Frama-C */
  struct a {
     int b ;
  };
  /* compiler builtin: 
     __builtin_va_list __builtin_next_arg(void);   */
  /* compiler builtin: 
     unsigned int __builtin_offsetof(unsigned int);   */
  /* compiler builtin: 
     void __builtin_stdarg_start(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_arg(__builtin_va_list, unsigned int, void *);   */
  /* compiler builtin: 
     void __builtin_va_copy(__builtin_va_list, __builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_end(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_start(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_varargs_start(__builtin_va_list);   */
  static struct a __constr_expr_0 = {.b = 1};
  struct a *d[1] = {& __constr_expr_0};
  static struct a __constr_expr_1 = {.b = 2};
  struct a *e[1] = {& __constr_expr_1};
  void foo(int c)
  {
    struct a **tmp;
    
    if (c) tmp = d; else tmp = e;
    struct a **p = tmp;
    return;
  }
[kernel] Parsing bts1553.i (no preprocessing)
[kernel:file:print-one] 
  result of parsing bts1553.i:
  /* Generated by Frama-C */
  struct a {
     int b ;
  };
  /* compiler builtin: 
     __builtin_va_list __builtin_next_arg(void);   */
  /* compiler builtin: 
     unsigned int __builtin_offsetof(unsigned int);   */
  /* compiler builtin: 
     void __builtin_stdarg_start(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_arg(__builtin_va_list, unsigned int, void *);   */
  /* compiler builtin: 
     void __builtin_va_copy(__builtin_va_list, __builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_end(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_va_start(__builtin_va_list);   */
  /* compiler builtin: 
     void __builtin_varargs_start(__builtin_va_list);   */
  static struct a __constr_expr_0 = {.b = 1};
  struct a *d[1] = {& __constr_expr_0};
  static struct a __constr_expr_1 = {.b = 5};
  struct a *tmp[1] = {& __constr_expr_1};
  int wibble(void)
  {
    return 1;
  }
  
  static struct a __constr_expr_2 = {.b = 2};
  struct a *e[1] = {& __constr_expr_2};
[kernel:file:annotation] Marking properties
/* Generated by Frama-C */
struct a {
   int b ;
};
static struct a __constr_expr_0 = {.b = 1};
struct a *d[1] = {& __constr_expr_0};
static struct a __constr_expr_1 = {.b = 2};
struct a *e[1] = {& __constr_expr_1};
void foo(int c)
{
  struct a **tmp_0;
  if (c) tmp_0 = d; else tmp_0 = e;
  struct a **p = tmp_0;
  return;
}

static struct a __constr_expr_3 = {.b = 5};
struct a *tmp[1] = {& __constr_expr_3};
int wibble(void)
{
  int __retres;
  __retres = 1;
  return __retres;
}