bts-1787.1.res.oracle

[kernel] Parsing bts-1787.i (no preprocessing)
[scf] beginning constant propagation
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  G1 ∈ {0}
  a ∈ {0}
  b ∈ {0}
  G2{.p1; .p2} ∈ {{ (? *)&G1 }}
    .p3 ∈ {{ &G1.c3 }}
[eva] computing for function g <- main.
  Called from bts-1787.i:39.
[eva] Recording results for g
[eva] Done for function g
[eva] Recording results for main
[eva] done for function main
/* Generated by Frama-C */
struct __anonstruct_S1_t_1 {
   int s ;
};
typedef struct __anonstruct_S1_t_1 S1_t;
struct __anonstruct_S2_t_2 {
   S1_t const *p1 ;
   S1_t *p2 ;
   S1_t *p3 ;
};
typedef struct __anonstruct_S2_t_2 S2_t;
struct __anonstruct_G1_3 {
   S1_t c12 ;
   S1_t c3 ;
};
struct __anonstruct_G1_3 G1;
static S2_t const G2 =
  {.p1 = (S1_t const *)(& G1.c12), .p2 = & G1.c12, .p3 = & G1.c3};
void g(S2_t const *q)
{
  S1_t *s1 = & G1.c12;
  G1.c3.s = G1.c12.s + G1.c12.s;
  G1.c12.s = 3;
  return;
}

int main(int c)
{
  int __retres;
  int tmp;
  if (c) tmp = 1; else tmp = 2;
  int s = tmp;
  G1.c12.s = s;
  g(& G2);
  __retres = G1.c3.s;
  return __retres;
}

int const a = 0;
int b = a;

[scf] constant propagation done