downcast.4.res.oracle 9.26 KiB
[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] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
Called from downcast.c:183.
[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] 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:garbled-mix:write] downcast.c:69:
Assigning imprecise value to us because of arithmetic operation on addresses.
[eva:garbled-mix:write] downcast.c:70:
Assigning imprecise value to us because of arithmetic operation on addresses.
[eva:garbled-mix:write] downcast.c:71:
Assigning imprecise value to c because of arithmetic operation on addresses.
[eva:garbled-mix:write] downcast.c:72:
Assigning imprecise value to c because of arithmetic operation on addresses.
[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] downcast.c:93:
Frama_C_show_each:
[100000..2147483647], [100145..2147483792], [-2147483648..2147483647]
[eva:alarm] downcast.c:94: Warning: assertion got status unknown.
[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:garbled-mix:write] downcast.c:122:
Assigning imprecise value to y because of arithmetic operation on addresses.
[eva:garbled-mix:write] downcast.c:123:
Assigning imprecise value to z because of arithmetic operation on addresses.
[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] Recording results for main8_bitfields[eva] Done for function main8_bitfields
[eva] computing for function main9_bitfield <- main.
Called from downcast.c:190.
[eva] downcast.c:164: assertion got status valid.
[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] 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] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
sz ∈ [--..--]
uc ∈ [--..--]
x ∈ [--..--]
ux ∈ [--..--]
s ∈ [--..--]
[eva:final-states] Values at end of function main10_loop:
c ∈ [--..--] 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 ∈ {-11} or UNINITIALIZED
.j ∈ {30} or UNINITIALIZED
.[bits 10 to 31] ∈ UNINITIALIZED
[eva:final-states] Values at end of function main3_reduction:
x_0 ∈ [--..--]
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 + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],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 ∈ {{ garbled mix of &{x_0; a} (origin: Arithmetic {downcast.c:70}) }}
c ∈ {{ garbled mix of &{x_0; a} (origin: Arithmetic {downcast.c:72}) }}
uintptr ∈
{{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
intptr ∈ {{ NULL + [0..36],0%4 ; &x_0 + [0..36],0%4 ; &a + [0..72],0%4 }}
[eva:final-states] Values at end of function main5_wrap_signed:
x_0 ∈ [100000..2147483647]
y ∈ [100145..2147483792]
z ∈ [--..--]
[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 ∈ {-1; 1} or UNINITIALIZED
.[bits 24 to 31] ∈ UNINITIALIZED
c ∈ {-1; 1; 65} or UNINITIALIZED
[eva:final-states] Values at end of function main9_bitfield:
bf.a ∈ {1648}
.[bits 11 to 31] ∈ UNINITIALIZED
c ∈ {112} or UNINITIALIZED
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
sz ∈ [--..--] uc ∈ [--..--]
x ∈ [--..--]
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