[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/value/volatile2.i (no preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value:initial-state] Values of globals at initialization
  t[0..9] ∈ [--..--]
  u ∈ [--..--]
  pu ∈ {{ &u }}
  s ∈ {0}
  ps ∈ {{ &s }}
  v ∈ [--..--]
  BITF ∈ [--..--]
[value] computing for function main1 <- main.
        Called from tests/value/volatile2.i:123.
tests/value/volatile2.i:23:[value] warning: signed overflow. assert (int)c << 8 ≤ 32767;
tests/value/volatile2.i:24:[value] warning: signed overflow. assert (int)*p << 8 ≤ 32767;
tests/value/volatile2.i:25:[value] warning: signed overflow. assert (int)t[1] << 8 ≤ 32767;
tests/value/volatile2.i:26:[value] warning: signed overflow. assert (int)u.f1 << 8 ≤ 32767;
[value] Recording results for main1
[value] Done for function main1
[value] computing for function main2 <- main.
        Called from tests/value/volatile2.i:124.
[value] Recording results for main2
[value] Done for function main2
[value] computing for function main3 <- main.
        Called from tests/value/volatile2.i:125.
tests/value/volatile2.i:47:[value] warning: assertion got status invalid (stopping propagation).
tests/value/volatile2.i:52:[value] assertion got status valid.
tests/value/volatile2.i:55:[value] warning: assertion got status unknown.
tests/value/volatile2.i:56:[value] warning: assertion got status unknown.
tests/value/volatile2.i:59:[value] assertion got status valid.
[value] Recording results for main3
[value] Done for function main3
[value] computing for function main4 <- main.
        Called from tests/value/volatile2.i:126.
[value] Recording results for main4
[value] Done for function main4
[value] computing for function main5 <- main.
        Called from tests/value/volatile2.i:127.
tests/value/volatile2.i:76:[value] warning: signed overflow. assert i + 1 ≤ 32767;
tests/value/volatile2.i:76:[value] warning: signed overflow. assert j + 1 ≤ 32767;
tests/value/volatile2.i:76:[value] warning: signed overflow.
                 assert -32768 ≤ tmp + tmp_0;
                 (tmp from i++, tmp_0 from j++)
tests/value/volatile2.i:76:[value] warning: signed overflow. assert tmp + tmp_0 ≤ 32767;
                                  (tmp from i++, tmp_0 from j++)
tests/value/volatile2.i:78:[value] warning: signed overflow. assert i + 1 ≤ 32767;
tests/value/volatile2.i:78:[value] warning: signed overflow. assert j + 1 ≤ 32767;
tests/value/volatile2.i:78:[value] warning: signed overflow. assert -32768 ≤ i + j;
tests/value/volatile2.i:78:[value] warning: signed overflow. assert i + j ≤ 32767;
[value] DUMPING STATE of file tests/value/volatile2.i line 80
        t[0..9] ∈ [--..--]
        u ∈ [--..--]
        pu ∈ {{ &u }}
        s ∈ {0}
        ps ∈ {{ &s }}
        v ∈ [--..--]
        i ∈ [--..--]
        j ∈ [--..--]
        k ∈ [--..--]
        tmp ∈ [--..--]
        tmp_0 ∈ [--..--]
        l ∈ [--..--]
        BITF ∈ [--..--]
        =END OF DUMP==
[value] Recording results for main5
[value] Done for function main5
[value] computing for function main6 <- main.
        Called from tests/value/volatile2.i:128.
[value] Recording results for main6
[value] Done for function main6
[value] computing for function main7 <- main.
        Called from tests/value/volatile2.i:129.
[value] Recording results for main7
[value] Done for function main7
[value] computing for function main8 <- main.
        Called from tests/value/volatile2.i:130.
[value] Called Frama_C_show_each([--..--], [--..--], [--..--], [--..--], [--..--])
[value] Recording results for main8
[value] Done for function main8
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value:final-states] Values at end of function main1:
  c ∈ [--..--]
  x ∈ {1}
  p ∈ {{ (unsigned char volatile *)&x }}
  i ∈ [0..32767]
  j ∈ [0..32767]
  k ∈ [0..32767]
  l ∈ [0..32767]
[value:final-states] Values at end of function main2:
  i ∈ [-128..127]
  j ∈ [0..255]
  k ∈ [0..255]
[value:final-states] Values at end of function main3:
  
[value:final-states] Values at end of function main4:
  p1 ∈ {{ &i }}
  p2 ∈ {{ &i + [--..--] }}
[value:final-states] Values at end of function main5:
  i ∈ [--..--]
  j ∈ [--..--]
  k ∈ [--..--]
  l ∈ [--..--]
[value:final-states] Values at end of function main6:
  i ∈ {1}
  j ∈ {1}
[value:final-states] Values at end of function main7:
  i ∈ {-3; -2; -1; 0; 1; 2; 3; 4}
  k ∈ [1..16]
[value:final-states] Values at end of function main8:
  a ∈ [--..--]
  b ∈ [--..--]
  c ∈ [--..--]
  d ∈ [--..--]
  e ∈ [--..--]
[value:final-states] Values at end of function main:
  
/* Generated by Frama-C */
struct u {
   unsigned char f1 ;
   unsigned char f2 ;
};
struct s {
   char i1 ;
   char i2 ;
};
struct bitf {
   int i : 3 ;
   unsigned int j : 4 ;
};
struct __anonstruct_S_1 {
   int field ;
};
typedef struct __anonstruct_S_1 S;
typedef S volatile vS;
struct __anonstruct_vS2_2 {
   int field ;
};
typedef struct __anonstruct_vS2_2 volatile vS2;
union __anonunion_U_3 {
   int field ;
};
typedef union __anonunion_U_3 U;
typedef U volatile vU;
unsigned char volatile t[10];
struct u volatile u;
struct u *pu = (struct u *)(& u);
void main1(void)
{
  unsigned char volatile c;
  int x;
  unsigned char volatile *p;
  unsigned int i;
  unsigned int j;
  unsigned int k;
  unsigned int l;
  c = (unsigned char)1;
  x = 1;
  p = (unsigned char volatile *)(& x);
  /*@ assert Value: signed_overflow: (int)c << 8 ≤ 32767; */
  i = (unsigned int)(((int)c << 8) + (int)c);
  /*@ assert Value: signed_overflow: (int)*p << 8 ≤ 32767; */
  j = (unsigned int)(((int)*p << 8) + (int)*p);
  /*@ assert Value: signed_overflow: (int)t[1] << 8 ≤ 32767; */
  k = (unsigned int)(((int)t[1] << 8) + (int)t[2]);
  /*@ assert Value: signed_overflow: (int)u.f1 << 8 ≤ 32767; */
  l = (unsigned int)(((int)u.f1 << 8) + (int)u.f2);
  return;
}

struct s s;
struct s volatile *ps = (struct s volatile *)(& s);
void main2(void)
{
  int i;
  int j;
  int k;
  i = (int)ps->i1;
  j = (int)u.f1;
  k = (int)t[1];
  return;
}

int volatile v;
void main3(void)
{
  if (v) 
    /*@ assert \false; */ ;
  if (v) 
    /*@ assert \true; */ ;
  /*@ assert v ≡ 0; */ ;
  /*@ assert v ≡ 0; */ ;
  if (v) 
    /*@ assert \true; */ ;
  return;
}

void main4(void)
{
  int volatile i;
  int volatile *p1;
  int volatile * volatile p2;
  p1 = & i;
  p2 = & i;
  return;
}

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int ( /* missing proto */ Frama_C_dump_each)();

void main5(void)
{
  int volatile i;
  int volatile j;
  int k;
  int tmp;
  int tmp_0;
  int l;
  i = 0;
  j = 0;
  { /* sequence */
    tmp = i;
    /*@ assert Value: signed_overflow: i + 1 ≤ 32767; */
    i ++;
    tmp_0 = j;
    /*@ assert Value: signed_overflow: j + 1 ≤ 32767; */
    j ++;
    ;
  }
  /*@ assert Value: signed_overflow: -32768 ≤ tmp + tmp_0; */
  /*@ assert Value: signed_overflow: tmp + tmp_0 ≤ 32767; */
  k = tmp + tmp_0;
  { /* sequence */
    /*@ assert Value: signed_overflow: i + 1 ≤ 32767; */
    i ++;
    /*@ assert Value: signed_overflow: j + 1 ≤ 32767; */
    j ++;
  }
  /*@ assert Value: signed_overflow: -32768 ≤ i + j; */
  /*@ assert Value: signed_overflow: i + j ≤ 32767; */
  l = i + j;
  Frama_C_dump_each();
  return;
}

void main6(void)
{
  int i;
  int j;
  i = 1;
  j = i;
  return;
}

struct bitf volatile BITF;
void main7(void)
{
  int i;
  int k;
  i = (int)BITF.i + 1;
  k = (int)BITF.j + 1;
  return;
}

/*@ assigns \result;
    assigns \result \from \nothing; */
extern int ( /* missing proto */ Frama_C_show_each)();

void main8(void)
{
  S volatile a;
  vS b;
  vS2 c;
  U volatile d;
  vU e;
  a.field = 0;
  b.field = 0;
  c.field = 0;
  d.field = 0;
  e.field = 0;
  Frama_C_show_each(a,b,c,d,e);
  return;
}

void main(void)
{
  main1();
  main2();
  main3();
  main4();
  main5();
  main6();
  main7();
  main8();
  return;
}