Skip to content
Snippets Groups Projects
Commit ffdb9d93 authored by David Bühler's avatar David Bühler Committed by Virgile Prevosto
Browse files

[Eva] Adds tests of pointer conversion, including to intptr_t and uintptr_t.

parent 8a852153
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 421 additions and 244 deletions
tests/value/downcast.i → tests/value/downcast.c
+ 35
− 9
View file @ ffdb9d93
......@@ -6,6 +6,9 @@
STDOPT: +"-lib-entry -no-warn-signed-downcast -no-warn-unsigned-downcast -no-warn-pointer-downcast"
*/
#include <__fc_builtin.h>
#include <stdint.h>
signed char sx,sy,sz;
unsigned char uc;
int x;
......@@ -45,22 +48,45 @@ void main3_reduction() {
unsigned char d = y;
}
/* The cvalue abstraction does not represent how an address is represented in a
C type. Thus alarms should always be emitted on a downcast of pointer values,
as we don't known if they fit in the destination type. */
/* Tests conversions of pointer values to various integer types. */
void main4_pointer() {
int x;
long long int p = (long long int)(&x);
p += 100;
unsigned int q = p;
signed int r = p;
int x, a[10];
int i = Frama_C_interval(0, 9);
int *p = &x;
if (v) p = &a[i];
if (v) p = 0;
int *q = p + i; // Invalid pointer.
/* On conversions below, no alarm should be emitted as all pointer values
fit in the destination type. */
long long int lli = (long long int)p;
lli = (long long int)q;
unsigned int ui = (unsigned int)p;
ui = (unsigned int)q;
/* On conversions below, downcast alarms must be emitted as all pointers do
not fit into the destination type. [q] and [p] cannot be reduced. */
signed int si = (signed int)p;
si = (signed int)q;
unsigned short us = (unsigned short)p;
us = (unsigned short)q;
char c = (char)p;
c = (char)q;
/* No alarm should be emitted as all pointer values fit in [uintptr_t]. */
uintptr_t uintptr = (uintptr_t)p;
uintptr = (uintptr_t)q;
/* No alarm should be emitted as valid pointers can always be converted to
"intptr_t", even if all pointer values do not fit in it.*/
intptr_t intptr = (intptr_t)p;
/* Alarm must be emitted as [q] may be an invalid pointer and all pointer
values do not fit in the "intptr_t" type. */
intptr = (intptr_t)q;
intptr = (intptr_t)q; // No alarm if [q] has been reduced at the line before.
}
// Perform a computation that overflows on signed integers without alarm. The assertions can be proven with enough slevel
void main5_wrap_signed() {
int x = v;
//@ assert ASSUME: x >= 100000;
//@ assert x > 0x7FFFFFFF-145 || x <= 0x7FFFFFFF-145;
//@ assert x > 0x7FFFFFFF-145 || x <= 0x7FFFFFFF-145;
unsigned int y = x;
y += 145;
int z = y;
......
tests/value/oracle/downcast.0.res.oracle
+ 65
− 33
View file @ ffdb9d93
[kernel] Parsing downcast.i (no preprocessing)
[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -14,66 +14,82 @@
s ∈ [--..--]
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from downcast.i:156.
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.i:157.
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.i:158.
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.i:159.
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert p + 100 ≤ 9223372036854775807;
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.i:160.
[eva:alarm] downcast.i:62: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.i:63: assertion got status valid.
[eva] downcast.i:67:
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:
[2147483503..2147483647],
[2147483648..2147483792],
[-2147483648..-2147483504]
[eva] downcast.i:67:
[eva] downcast.c:93:
Frama_C_show_each:
[100000..2147483502], [100145..2147483647], [100145..2147483647]
[eva] downcast.i:68: assertion got status valid.
[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.i:161.
[eva:alarm] downcast.i:95: Warning:
Called from downcast.c:187.
[eva:alarm] downcast.c:121: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] downcast.i:96: Warning:
[eva:alarm] downcast.c:122: Warning:
pointer downcast. assert (unsigned int)p ≤ 32767;
[eva:alarm] downcast.i:97: Warning:
[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.i:162.
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.i:163.
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.i:164.
[eva] downcast.i:138: assertion got status valid.
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.i:165.
[eva] downcast.i:149: starting to merge loop iterations
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
......@@ -102,9 +118,18 @@
y ∈ [--..--]
d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
p ∈ {{ &x_0 + {100} }}
q ∈ {{ &x_0 + {100} }}
r ∈ {{ &x_0 + {100} }}
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..2147483792]
......@@ -124,6 +149,7 @@
.[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 ∈ [--..--]
......@@ -138,6 +164,8 @@
[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
......@@ -153,6 +181,9 @@
[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
......@@ -166,7 +197,7 @@
[from] Function main3_reduction:
NO EFFECTS
[from] Function main4_pointer:
NO EFFECTS
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:
......@@ -178,6 +209,7 @@
[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
......@@ -201,9 +233,9 @@
[inout] Inputs for function main3_reduction:
v
[inout] Out (internal) for function main4_pointer:
p; q; r
Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
\nothing
Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
x_0; y; z
[inout] Inputs for function main5_wrap_signed:
......@@ -225,6 +257,6 @@
[inout] Inputs for function main9_bitfield:
v
[inout] Out (internal) for function main:
sz; uc; x; ux; s
Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
sx; sy; x; uy; uz; v
Frama_C_entropy_source; sx; sy; x; uy; uz; v
tests/value/oracle/downcast.1.res.oracle
+ 92
− 62
View file @ ffdb9d93
[kernel] Parsing downcast.i (no preprocessing)
[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -14,98 +14,112 @@
s ∈ [--..--]
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from downcast.i:156.
[eva:alarm] downcast.i:23: Warning:
Called from downcast.c:182.
[eva:alarm] downcast.c:26: Warning:
signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
[eva:alarm] downcast.i:23: Warning:
[eva:alarm] downcast.c:26: Warning:
signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
[eva:alarm] downcast.i:26: Warning:
[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.i:157.
[eva:alarm] downcast.i:36: Warning: signed downcast. assert i ≤ 15;
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.i:158.
[eva:alarm] downcast.i:42: Warning: signed downcast. assert -128 ≤ x_0;
[eva:alarm] downcast.i:42: Warning: signed downcast. assert x_0 ≤ 127;
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.i:159.
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] downcast.i:56: Warning: signed downcast. assert -2147483648 ≤ p;
[eva:alarm] downcast.i:56: Warning: signed downcast. assert p ≤ 2147483647;
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.i:160.
[eva:alarm] downcast.i:62: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.i:63: assertion got status valid.
[eva:alarm] downcast.i:66: Warning: signed downcast. assert y ≤ 2147483647;
[eva] downcast.i:67:
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.i:68: assertion got status valid.
[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.i:161.
[eva:alarm] downcast.i:75: Warning: signed downcast. assert 65300u ≤ 32767;
[eva:alarm] downcast.i:86: Warning: signed downcast. assert e_0 ≤ 32767;
[eva:alarm] downcast.i:91: Warning: signed downcast. assert e_1 ≤ 32767;
[eva:alarm] downcast.i:95: Warning:
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.i:96: Warning:
[eva:alarm] downcast.c:122: Warning:
pointer downcast. assert (unsigned int)p ≤ 32767;
[eva:alarm] downcast.i:97: Warning:
[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.i:162.
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.i:163.
[eva:alarm] downcast.i:118: Warning: signed downcast. assert S.i1 ≤ 31;
[eva:alarm] downcast.i:119: Warning: signed downcast. assert S.i1 ≤ 127;
[eva:alarm] downcast.i:123: Warning: signed downcast. assert S.i1 ≤ 31;
[eva:alarm] downcast.i:124: Warning: signed downcast. assert S.i1 ≤ 127;
[eva:alarm] downcast.i:128: Warning: signed downcast. assert S.i1 ≤ 31;
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.i:164.
[eva:alarm] downcast.i:137: Warning: signed downcast. assert bf.a ≤ 1023;
[eva:alarm] downcast.i:141: Warning: signed downcast. assert bf.a ≤ 127;
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.i:165.
[eva:alarm] downcast.i:151: Warning: signed downcast. assert bf.b ≤ 127;
[eva] downcast.i:149: starting to merge loop iterations
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.i:36: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:75: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:86: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:91: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:118: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:119: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:123: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:124: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:128: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:137: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:141: assertion 'Eva,signed_downcast' got final status invalid.
[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 ∈ [--..--]
......@@ -130,9 +144,18 @@
y ∈ [--..--]
d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
p ∈ {{ &x_0 + {100} }}
q ∈ {{ &x_0 + {100} }}
r ∈ {{ &x_0 + {100} }}
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]
......@@ -151,6 +174,7 @@
.[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]
......@@ -165,6 +189,8 @@
[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
......@@ -180,6 +206,9 @@
[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
......@@ -193,7 +222,7 @@
[from] Function main3_reduction:
NO EFFECTS
[from] Function main4_pointer:
NO EFFECTS
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:
......@@ -205,6 +234,7 @@
[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
......@@ -228,9 +258,9 @@
[inout] Inputs for function main3_reduction:
v
[inout] Out (internal) for function main4_pointer:
p; q; r
Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
\nothing
Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
x_0; y; z
[inout] Inputs for function main5_wrap_signed:
......@@ -252,6 +282,6 @@
[inout] Inputs for function main9_bitfield:
v
[inout] Out (internal) for function main:
sz; uc; x; ux; s
Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
sx; sy; x; uy; uz; v
Frama_C_entropy_source; sx; sy; x; uy; uz; v
tests/value/oracle/downcast.2.res.oracle
+ 80
− 48
View file @ ffdb9d93
[kernel] Parsing downcast.i (no preprocessing)
[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -14,84 +14,100 @@
s ∈ [--..--]
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from downcast.i:156.
[eva:alarm] downcast.i:24: Warning:
Called from downcast.c:182.
[eva:alarm] downcast.c:27: Warning:
unsigned downcast. assert 0 ≤ (int)((int)sx + (int)sy);
[eva:alarm] downcast.i:25: Warning: unsigned downcast. assert 0 ≤ x;
[eva:alarm] downcast.i:25: Warning: unsigned downcast. assert x ≤ 255;
[eva:alarm] downcast.i:28: Warning:
[eva:alarm] downcast.c:28: Warning: unsigned downcast. assert 0 ≤ x;
[eva:alarm] downcast.c:28: Warning: unsigned downcast. assert x ≤ 255;
[eva:alarm] downcast.c:31: Warning:
unsigned downcast. assert (unsigned int)(uy + uz) ≤ 65535;
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
Called from downcast.i:157.
[eva:alarm] downcast.i:37: Warning: unsigned downcast. assert j ≤ 31;
Called from downcast.c:183.
[eva:alarm] downcast.c:40: Warning: unsigned downcast. assert j ≤ 31;
[eva] Recording results for main2_bitfield
[eva] Done for function main2_bitfield
[eva] computing for function main3_reduction <- main.
Called from downcast.i:158.
[eva:alarm] downcast.i:44: Warning: unsigned downcast. assert 0 ≤ v;
[eva:alarm] downcast.i:45: Warning: unsigned downcast. assert y ≤ 255;
Called from downcast.c:184.
[eva:alarm] downcast.c:47: Warning: unsigned downcast. assert 0 ≤ v;
[eva:alarm] downcast.c:48: Warning: unsigned downcast. assert y ≤ 255;
[eva] Recording results for main3_reduction
[eva] Done for function main3_reduction
[eva] computing for function main4_pointer <- main.
Called from downcast.i:159.
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] downcast.i:55: Warning: unsigned downcast. assert 0 ≤ p;
[eva:alarm] downcast.i:55: Warning: unsigned downcast. assert p ≤ 4294967295;
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.i:160.
[eva:alarm] downcast.i:62: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.i:63: assertion got status valid.
[eva] downcast.i:67:
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.i:68: Warning: assertion got status unknown.
[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.i:161.
[eva:alarm] downcast.i:85: Warning: unsigned downcast. assert 0 ≤ (int)(-12);
[eva:alarm] downcast.i:90: Warning:
Called from downcast.c:187.
[eva:alarm] downcast.c:111: Warning: unsigned downcast. assert 0 ≤ (int)(-12);
[eva:alarm] downcast.c:116: Warning:
unsigned downcast. assert 0 ≤ (int)(-64000);
[eva:alarm] downcast.i:95: Warning:
[eva:alarm] downcast.c:121: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] downcast.i:96: Warning:
[eva:alarm] downcast.c:122: Warning:
pointer downcast. assert (unsigned int)p ≤ 32767;
[eva:alarm] downcast.i:97: Warning:
[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.i:162.
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.i:163.
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.i:164.
[eva] downcast.i:138: assertion got status valid.
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.i:165.
[eva:alarm] downcast.i:150: Warning: unsigned downcast. assert 0 ≤ v;
[eva:alarm] downcast.i:150: Warning: unsigned downcast. assert v ≤ 1023;
[eva] downcast.i:149: starting to merge loop iterations
Called from downcast.c:191.
[eva:alarm] downcast.c:176: Warning: unsigned downcast. assert 0 ≤ v;
[eva:alarm] downcast.c:176: Warning: unsigned downcast. assert v ≤ 1023;
[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.i:37: assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] downcast.i:85: assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] downcast.i:90: assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] downcast.c:40: assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] downcast.c:111:
assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] downcast.c:116:
assertion 'Eva,unsigned_downcast' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
sz ∈ [--..--]
......@@ -115,9 +131,18 @@
y ∈ [0..255]
d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
p ∈ {{ &x_0 + {100} }}
q ∈ {{ &x_0 + {100} }}
r ∈ {{ &x_0 + {100} }}
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..2147483792]
......@@ -137,6 +162,7 @@
.[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 ∈ [--..--]
......@@ -151,6 +177,8 @@
[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
......@@ -166,6 +194,9 @@
[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
......@@ -179,7 +210,7 @@
[from] Function main3_reduction:
NO EFFECTS
[from] Function main4_pointer:
NO EFFECTS
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:
......@@ -191,6 +222,7 @@
[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
......@@ -214,9 +246,9 @@
[inout] Inputs for function main3_reduction:
v
[inout] Out (internal) for function main4_pointer:
p; q; r
Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
\nothing
Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
x_0; y; z
[inout] Inputs for function main5_wrap_signed:
......@@ -238,6 +270,6 @@
[inout] Inputs for function main9_bitfield:
v
[inout] Out (internal) for function main:
sz; uc; x; ux; s
Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
sx; sy; x; uy; uz; v
Frama_C_entropy_source; sx; sy; x; uy; uz; v
tests/value/oracle/downcast.3.res.oracle
+ 85
− 54
View file @ ffdb9d93
[kernel] Parsing downcast.i (no preprocessing)
[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -14,89 +14,104 @@
s ∈ [--..--]
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from downcast.i:156.
[eva:alarm] downcast.i:23: Warning:
Called from downcast.c:182.
[eva:alarm] downcast.c:26: Warning:
signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
[eva:alarm] downcast.i:23: Warning:
[eva:alarm] downcast.c:26: Warning:
signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
[eva] Recording results for main1
[eva] Done for function main1
[eva] computing for function main2_bitfield <- main.
Called from downcast.i:157.
[eva:alarm] downcast.i:36: Warning: signed downcast. assert i ≤ 15;
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.i:158.
[eva:alarm] downcast.i:42: Warning: signed downcast. assert -128 ≤ x_0;
[eva:alarm] downcast.i:42: Warning: signed downcast. assert x_0 ≤ 127;
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.i:159.
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert p + 100 ≤ 9223372036854775807;
[eva:alarm] downcast.i:56: Warning: signed downcast. assert -2147483648 ≤ p;
[eva:alarm] downcast.i:56: Warning: signed downcast. assert p ≤ 2147483647;
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.i:160.
[eva:alarm] downcast.i:62: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.i:63: assertion got status valid.
[eva] downcast.i:67:
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.i:68: Warning: assertion got status unknown.
[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.i:161.
[eva:alarm] downcast.i:75: Warning: signed downcast. assert 65300u ≤ 32767;
[eva:alarm] downcast.i:91: Warning: signed downcast. assert -32768 ≤ (int)e_1;
[eva:alarm] downcast.i:95: Warning:
Called from downcast.c:187.
[eva:alarm] downcast.c:101: Warning: signed downcast. assert 65300u ≤ 32767;
[eva:alarm] downcast.c:117: Warning:
signed downcast. assert -32768 ≤ (int)e_1;
[eva:alarm] downcast.c:121: Warning:
pointer downcast. assert (unsigned int)p ≤ 2147483647;
[eva:alarm] downcast.i:96: Warning:
[eva:alarm] downcast.c:122: Warning:
pointer downcast. assert (unsigned int)p ≤ 32767;
[eva:alarm] downcast.i:97: Warning:
[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.i:162.
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.i:163.
[eva:alarm] downcast.i:123: Warning: signed downcast. assert (int)S.i1 ≤ 31;
[eva:alarm] downcast.i:124: Warning: signed downcast. assert (int)S.i1 ≤ 127;
[eva:alarm] downcast.i:128: Warning: signed downcast. assert (int)S.i1 ≤ 31;
Called from downcast.c:189.
[eva:alarm] downcast.c:149: Warning: signed downcast. assert (int)S.i1 ≤ 31;
[eva:alarm] downcast.c:150: Warning: signed downcast. assert (int)S.i1 ≤ 127;
[eva:alarm] downcast.c:154: Warning: signed downcast. assert (int)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.i:164.
[eva] downcast.i:138: assertion got status valid.
[eva:alarm] downcast.i:141: Warning: signed downcast. assert -128 ≤ (int)bf.a;
Called from downcast.c:190.
[eva] downcast.c:164: assertion got status valid.
[eva:alarm] downcast.c:167: Warning: signed downcast. assert -128 ≤ (int)bf.a;
[eva] Recording results for main9_bitfield
[eva] Done for function main9_bitfield
[eva] computing for function main10_loop <- main.
Called from downcast.i:165.
[eva:alarm] downcast.i:151: Warning: signed downcast. assert -128 ≤ (int)bf.b;
[eva:alarm] downcast.i:151: Warning: signed downcast. assert (int)bf.b ≤ 127;
[eva] downcast.i:149: starting to merge loop iterations
Called from downcast.c:191.
[eva:alarm] downcast.c:177: Warning: signed downcast. assert -128 ≤ (int)bf.b;
[eva:alarm] downcast.c:177: Warning: signed downcast. assert (int)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.i:36: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:75: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:91: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:123: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:124: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:128: assertion 'Eva,signed_downcast' got final status invalid.
[eva] downcast.i:141: assertion 'Eva,signed_downcast' got final status invalid.
[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:117: 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:167: assertion 'Eva,signed_downcast' got final status invalid.
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main1:
sz ∈ [--..--]
......@@ -121,9 +136,18 @@
y ∈ [--..--]
d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
p ∈ {{ &x_0 + {100} }}
q ∈ {{ &x_0 + {100} }}
r ∈ {{ &x_0 + {100} }}
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..2147483792]
......@@ -143,6 +167,7 @@
.[bits 11 to 31] ∈ UNINITIALIZED
c ∈ UNINITIALIZED
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
sz ∈ [--..--]
uc ∈ [--..--]
x ∈ [--..--]
......@@ -157,6 +182,8 @@
[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
......@@ -172,6 +199,9 @@
[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
......@@ -185,7 +215,7 @@
[from] Function main3_reduction:
NO EFFECTS
[from] Function main4_pointer:
NO EFFECTS
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:
......@@ -197,6 +227,7 @@
[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
......@@ -220,9 +251,9 @@
[inout] Inputs for function main3_reduction:
v
[inout] Out (internal) for function main4_pointer:
p; q; r
Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
\nothing
Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
x_0; y; z
[inout] Inputs for function main5_wrap_signed:
......@@ -244,6 +275,6 @@
[inout] Inputs for function main9_bitfield:
v
[inout] Out (internal) for function main:
sz; uc; x; ux; s
Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
sx; sy; x; uy; uz; v
Frama_C_entropy_source; sx; sy; x; uy; uz; v
tests/value/oracle/downcast.4.res.oracle
+ 57
− 31
View file @ ffdb9d93
[kernel] Parsing downcast.i (no preprocessing)
[kernel] Parsing downcast.c (with preprocessing)
[eva] Analyzing an incomplete application starting at main
[eva] Computing initial state
[eva] Initial state computed
......@@ -14,59 +14,69 @@
s ∈ [--..--]
v ∈ [--..--]
[eva] computing for function main1 <- main.
Called from downcast.i:156.
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.i:157.
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.i:158.
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.i:159.
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert -9223372036854775808 ≤ p + 100;
[eva:alarm] downcast.i:54: Warning:
signed overflow. assert p + 100 ≤ 9223372036854775807;
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.i:160.
[eva:alarm] downcast.i:62: Warning: assertion 'ASSUME' got status unknown.
[eva] downcast.i:63: assertion got status valid.
[eva] downcast.i:67:
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.i:68: Warning: assertion got status unknown.
[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.i:161.
[eva:garbled-mix:write] downcast.i:96:
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.i:97:
[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.i:162.
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.i:163.
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.i:164.
[eva] downcast.i:138: assertion got status valid.
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.i:165.
[eva] downcast.i:149: starting to merge loop iterations
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
......@@ -95,9 +105,18 @@
y ∈ [--..--]
d ∈ [--..--]
[eva:final-states] Values at end of function main4_pointer:
p ∈ {{ &x_0 + {100} }}
q ∈ {{ &x_0 + {100} }}
r ∈ {{ &x_0 + {100} }}
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]
......@@ -117,6 +136,7 @@
.[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 ∈ [--..--]
......@@ -131,6 +151,8 @@
[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
......@@ -146,6 +168,9 @@
[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
......@@ -159,7 +184,7 @@
[from] Function main3_reduction:
NO EFFECTS
[from] Function main4_pointer:
NO EFFECTS
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:
......@@ -171,6 +196,7 @@
[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
......@@ -194,9 +220,9 @@
[inout] Inputs for function main3_reduction:
v
[inout] Out (internal) for function main4_pointer:
p; q; r
Frama_C_entropy_source; i; p; q; lli; ui; si; us; c; uintptr; intptr
[inout] Inputs for function main4_pointer:
\nothing
Frama_C_entropy_source; v
[inout] Out (internal) for function main5_wrap_signed:
x_0; y; z
[inout] Inputs for function main5_wrap_signed:
......@@ -218,6 +244,6 @@
[inout] Inputs for function main9_bitfield:
v
[inout] Out (internal) for function main:
sz; uc; x; ux; s
Frama_C_entropy_source; sz; uc; x; ux; s
[inout] Inputs for function main:
sx; sy; x; uy; uz; v
Frama_C_entropy_source; sx; sy; x; uy; uz; v
tests/value/oracle_apron/downcast.1.res.oracle
+ 1
− 1
View file @ ffdb9d93
54c54
68c68
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
> [100000..2147483502], [100145..2147483647], [100145..2147483647]
tests/value/oracle_equality/downcast.2.res.oracle
+ 2
− 2
View file @ ffdb9d93
100c100
116c116
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
143c143
169c169
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
tests/value/oracle_octagon/downcast.1.res.oracle
+ 2
− 2
View file @ ffdb9d93
54c54
68c68
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
> [100000..2147483502], [100145..2147483647], [100145..2147483647]
137c137
160c160
< x_0 ∈ [100000..2147483647]
---
> x_0 ∈ [100000..2147483502]
tests/value/oracle_symblocs/downcast.1.res.oracle
+ 2
− 2
View file @ ffdb9d93
114c114
128c128
< ux ∈ [--..--]
---
> ux ∈ [0..2147483647]
157c157
181c181
< ux ∈ [--..--]
---
> ux ∈ [0..2147483647]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment