[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
  sx ∈ [--..--]
  sy ∈ [--..--]
  sz ∈ [--..--]
  uc ∈ [--..--]
  x ∈ [--..--]
  ux ∈ [--..--]
  uy ∈ [--..--]
  uz ∈ [--..--]
  s ∈ [--..--]
  v ∈ [--..--]
[eva] computing for function main1 <- main.
  Called from downcast.c:182.
[eva:alarm] downcast.c:26: Warning: 
  signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
[eva:alarm] downcast.c:26: Warning: 
  signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
[eva:alarm] downcast.c:29: Warning: 
  signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
  Called from downcast.c:183.
[eva:alarm] downcast.c:39: Warning: signed downcast. assert i ≤ 15;
[eva] Recording results for main2_bitfield
[eva] Done for function main2_bitfield
[eva] computing for function main3_reduction <- main.
  Called from downcast.c:184.
[eva:alarm] downcast.c:45: Warning: signed downcast. assert -128 ≤ x_0;
[eva:alarm] downcast.c:45: Warning: signed downcast. assert x_0 ≤ 127;
[eva] Recording results for main3_reduction
[eva] Done for function main3_reduction
[eva] computing for function main4_pointer <- main.
  Called from downcast.c:185.
[eva] computing for function Frama_C_interval <- main4_pointer <- main.
  Called from downcast.c:54.
[eva] using specification for function Frama_C_interval
[eva] downcast.c:54: 
  function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] downcast.c:67: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] downcast.c:68: Warning: 
  pointer downcast. assert (unsigned int)q ≤ 2147483647;
[eva:alarm] downcast.c:69: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 65535;
[eva:alarm] downcast.c:70: Warning: 
  pointer downcast. assert (unsigned int)q ≤ 65535;
[eva:alarm] downcast.c:71: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 127;
[eva:alarm] downcast.c:72: Warning: 
  pointer downcast. assert (unsigned int)q ≤ 127;
[eva:alarm] downcast.c:81: Warning: 
  invalid pointer creation. assert \object_pointer(q);
[eva] Recording results for main4_pointer
[eva] Done for function main4_pointer
[eva] computing for function main5_wrap_signed <- main.
  Called from downcast.c:186.
[eva:alarm] downcast.c:88: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.c:89: assertion got status valid.
[eva:alarm] downcast.c:92: Warning: signed downcast. assert y ≤ 2147483647;
[eva] downcast.c:93: 
  Frama_C_show_each:
  [100000..2147483647], [100145..2147483647], [100145..2147483647]
[eva] downcast.c:94: assertion got status valid.
[eva] Recording results for main5_wrap_signed
[eva] Done for function main5_wrap_signed
[eva] computing for function main6_val_warn_converted_signed <- main.
  Called from downcast.c:187.
[eva:alarm] downcast.c:101: Warning: signed downcast. assert 65300u ≤ 32767;
[eva:alarm] downcast.c:112: Warning: signed downcast. assert e_0 ≤ 32767;
[eva:alarm] downcast.c:117: Warning: signed downcast. assert e_1 ≤ 32767;
[eva:alarm] downcast.c:121: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] downcast.c:122: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 32767;
[eva:alarm] downcast.c:123: Warning: 
  pointer downcast. assert (unsigned int)p ≤ 65535;
[eva] Recording results for main6_val_warn_converted_signed
[eva] Done for function main6_val_warn_converted_signed
[eva] computing for function main7_signed_upcast <- main.
  Called from downcast.c:188.
[eva] Recording results for main7_signed_upcast
[eva] Done for function main7_signed_upcast
[eva] computing for function main8_bitfields <- main.
  Called from downcast.c:189.
[eva:alarm] downcast.c:144: Warning: signed downcast. assert S.i1 ≤ 31;
[eva:alarm] downcast.c:145: Warning: signed downcast. assert S.i1 ≤ 127;
[eva:alarm] downcast.c:149: Warning: signed downcast. assert S.i1 ≤ 31;
[eva:alarm] downcast.c:150: Warning: signed downcast. assert S.i1 ≤ 127;
[eva:alarm] downcast.c:154: Warning: signed downcast. assert S.i1 ≤ 31;
[eva] Recording results for main8_bitfields
[eva] Done for function main8_bitfields
[eva] computing for function main9_bitfield <- main.
  Called from downcast.c:190.
[eva:alarm] downcast.c:163: Warning: signed downcast. assert bf.a ≤ 1023;
[eva:alarm] downcast.c:167: Warning: signed downcast. assert bf.a ≤ 127;
[eva] Recording results for main9_bitfield
[eva] Done for function main9_bitfield
[eva] computing for function main10_loop <- main.
  Called from downcast.c:191.
[eva:alarm] downcast.c:177: Warning: signed downcast. assert bf.b ≤ 127;
[eva] downcast.c:175: starting to merge loop iterations
[eva] Recording results for main10_loop
[eva] Done for function main10_loop
[eva] Recording results for main
[eva] Done for function main
[eva] downcast.c:39: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:101: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:112: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:117: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:144: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:145: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:149: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:150: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:154: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:163: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.c:167: assertion 'Eva,signed_downcast' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
  sz ∈ [--..--]
  uc ∈ [--..--]
  x ∈ [0..2147483647]
  ux ∈ [--..--]
  s ∈ [--..--]
[eva:final-states] Values at end of function main10_loop:
  c ∈ [0..127] or UNINITIALIZED
  bf.b ∈ [--..--] or UNINITIALIZED
    .[bits 10 to 31] ∈ UNINITIALIZED
  k ∈ {10}
[eva:final-states] Values at end of function main2_bitfield:
  i ∈ {117}
  j ∈ {254}
  ss.i ∈ UNINITIALIZED
    .j ∈ {30} or UNINITIALIZED
    .[bits 10 to 31] ∈ UNINITIALIZED
[eva:final-states] Values at end of function main3_reduction:
  x_0 ∈ [-128..127]
  c ∈ [--..--]
  y ∈ [--..--]
  d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
  Frama_C_entropy_source ∈ [--..--]
  i ∈ [0..9]
  p ∈ {{ NULL ; &x_0 ; &a + [0..36],0%4 }}
  q ∈ {{ NULL ; &x_0 + {0; 4} ; &a + [0..40],0%4 }}
  lli ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  ui ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  si ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  us ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  c ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  uintptr ∈
         {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
  intptr ∈ {{ NULL ; &x_0 + {0; 4} ; &a + [0..40],0%4 }}
[eva:final-states] Values at end of function main5_wrap_signed:
  x_0 ∈ [100000..2147483647]
  y ∈ [100145..2147483647]
  z ∈ [100145..2147483647]
[eva:final-states] Values at end of function main6_val_warn_converted_signed:
  
[eva:final-states] Values at end of function main7_signed_upcast:
  c ∈ {240}
  i ∈ {240}
[eva:final-states] Values at end of function main8_bitfields:
  S.i1 ∈ {65}
   {.i2; .[bits 24 to 31]} ∈ UNINITIALIZED
  c ∈ {65} or UNINITIALIZED
[eva:final-states] Values at end of function main9_bitfield:
  bf.a ∈ {1648}
    .[bits 11 to 31] ∈ UNINITIALIZED
  c ∈ UNINITIALIZED
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  sz ∈ [--..--]
  uc ∈ [--..--]
  x ∈ [0..2147483647]
  ux ∈ [--..--]
  s ∈ [--..--]
[from] Computing for function main1
[from] Done for function main1
[from] Computing for function main10_loop
[from] Done for function main10_loop
[from] Computing for function main2_bitfield
[from] Done for function main2_bitfield
[from] Computing for function main3_reduction
[from] Done for function main3_reduction
[from] Computing for function main4_pointer
[from] Computing for function Frama_C_interval <-main4_pointer
[from] Done for function Frama_C_interval
[from] Done for function main4_pointer
[from] Computing for function main5_wrap_signed
[from] Done for function main5_wrap_signed
[from] Computing for function main6_val_warn_converted_signed
[from] Done for function main6_val_warn_converted_signed
[from] Computing for function main7_signed_upcast
[from] Done for function main7_signed_upcast
[from] Computing for function main8_bitfields
[from] Done for function main8_bitfields
[from] Computing for function main9_bitfield
[from] Done for function main9_bitfield
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
  These dependencies hold at termination for the executions that terminate:
[from] Function Frama_C_interval:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
  \result FROM Frama_C_entropy_source; min; max
[from] Function main1:
  sz FROM sx; sy
  uc FROM x
  x FROM uy; uz
  ux FROM uy; uz
  s FROM uy; uz
[from] Function main10_loop:
  NO EFFECTS
[from] Function main2_bitfield:
  NO EFFECTS
[from] Function main3_reduction:
  NO EFFECTS
[from] Function main4_pointer:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function main5_wrap_signed:
  NO EFFECTS
[from] Function main6_val_warn_converted_signed:
  NO EFFECTS
[from] Function main7_signed_upcast:
  NO EFFECTS
[from] Function main8_bitfields:
  NO EFFECTS
[from] Function main9_bitfield:
  NO EFFECTS
[from] Function main:
  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
  sz FROM sx; sy
  uc FROM x
  x FROM uy; uz
  ux FROM uy; uz
  s FROM uy; uz
[from] ====== END OF DEPENDENCIES ======
[inout] Out (internal) for function main1:
    sz; uc; x; ux; s
[inout] Inputs for function main1:
    sx; sy; x; uy; uz
[inout] Out (internal) for function main10_loop:
    c; bf.b; k
[inout] Inputs for function main10_loop:
    v
[inout] Out (internal) for function main2_bitfield:
    i; j; ss{.i; .j}
[inout] Inputs for function main2_bitfield:
    v
[inout] Out (internal) for function main3_reduction:
    x_0; c; y; d
[inout] Inputs for function main3_reduction:
    v
[inout] Out (internal) for function main4_pointer:
    Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
    Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
    x_0; y; z
[inout] Inputs for function main5_wrap_signed:
    v
[inout] Out (internal) for function main6_val_warn_converted_signed:
    s_0; u; e; b; e_0; b_0; e_1; b_1; p; x_0; y; z
[inout] Inputs for function main6_val_warn_converted_signed:
    v
[inout] Out (internal) for function main7_signed_upcast:
    c; i
[inout] Inputs for function main7_signed_upcast:
    \nothing
[inout] Out (internal) for function main8_bitfields:
    S{.i1; .i2}; c
[inout] Inputs for function main8_bitfields:
    v
[inout] Out (internal) for function main9_bitfield:
    bf.a; signed_a; c
[inout] Inputs for function main9_bitfield:
    v
[inout] Out (internal) for function main:
    Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
    Frama_C_entropy_source; sx; sy; x; uy; uz; v