From ffdb9d93580fa5e97dab69dfb0c4308b332108dc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 5 Sep 2024 13:28:20 +0200
Subject: [PATCH] [Eva] Adds tests of pointer conversion, including to intptr_t
and uintptr_t.
---
tests/value/{downcast.i => downcast.c} | 44 ++++-
tests/value/oracle/downcast.0.res.oracle | 98 +++++++----
tests/value/oracle/downcast.1.res.oracle | 154 +++++++++++-------
tests/value/oracle/downcast.2.res.oracle | 128 +++++++++------
tests/value/oracle/downcast.3.res.oracle | 139 ++++++++++------
tests/value/oracle/downcast.4.res.oracle | 88 ++++++----
.../value/oracle_apron/downcast.1.res.oracle | 2 +-
.../oracle_equality/downcast.2.res.oracle | 4 +-
.../oracle_octagon/downcast.1.res.oracle | 4 +-
.../oracle_symblocs/downcast.1.res.oracle | 4 +-
10 files changed, 421 insertions(+), 244 deletions(-)
rename tests/value/{downcast.i => downcast.c} (72%)
diff --git a/tests/value/downcast.i b/tests/value/downcast.c
similarity index 72%
rename from tests/value/downcast.i
rename to tests/value/downcast.c
index 70d4eae7bdb..44d35b84d99 100644
--- a/tests/value/downcast.i
+++ b/tests/value/downcast.c
@@ -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;
diff --git a/tests/value/oracle/downcast.0.res.oracle b/tests/value/oracle/downcast.0.res.oracle
index b7889d7ae46..1da4f878b8d 100644
--- a/tests/value/oracle/downcast.0.res.oracle
+++ b/tests/value/oracle/downcast.0.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/tests/value/oracle/downcast.1.res.oracle b/tests/value/oracle/downcast.1.res.oracle
index 30618f94ce0..af221b0a197 100644
--- a/tests/value/oracle/downcast.1.res.oracle
+++ b/tests/value/oracle/downcast.1.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/tests/value/oracle/downcast.2.res.oracle b/tests/value/oracle/downcast.2.res.oracle
index 16a83990300..be309c6dd7a 100644
--- a/tests/value/oracle/downcast.2.res.oracle
+++ b/tests/value/oracle/downcast.2.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/tests/value/oracle/downcast.3.res.oracle b/tests/value/oracle/downcast.3.res.oracle
index 994ce5ae4fc..604f3921585 100644
--- a/tests/value/oracle/downcast.3.res.oracle
+++ b/tests/value/oracle/downcast.3.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/tests/value/oracle/downcast.4.res.oracle b/tests/value/oracle/downcast.4.res.oracle
index 5417bdf0ee0..191580ecf3b 100644
--- a/tests/value/oracle/downcast.4.res.oracle
+++ b/tests/value/oracle/downcast.4.res.oracle
@@ -1,4 +1,4 @@
-[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
diff --git a/tests/value/oracle_apron/downcast.1.res.oracle b/tests/value/oracle_apron/downcast.1.res.oracle
index cd4295f4700..78178cea2d3 100644
--- a/tests/value/oracle_apron/downcast.1.res.oracle
+++ b/tests/value/oracle_apron/downcast.1.res.oracle
@@ -1,4 +1,4 @@
-54c54
+68c68
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
> [100000..2147483502], [100145..2147483647], [100145..2147483647]
diff --git a/tests/value/oracle_equality/downcast.2.res.oracle b/tests/value/oracle_equality/downcast.2.res.oracle
index 947c8b0bd67..73a343e692b 100644
--- a/tests/value/oracle_equality/downcast.2.res.oracle
+++ b/tests/value/oracle_equality/downcast.2.res.oracle
@@ -1,8 +1,8 @@
-100c100
+116c116
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
-143c143
+169c169
< ux ∈ [--..--]
---
> ux ∈ [0..65535]
diff --git a/tests/value/oracle_octagon/downcast.1.res.oracle b/tests/value/oracle_octagon/downcast.1.res.oracle
index dc085cd080c..36631e7f5aa 100644
--- a/tests/value/oracle_octagon/downcast.1.res.oracle
+++ b/tests/value/oracle_octagon/downcast.1.res.oracle
@@ -1,8 +1,8 @@
-54c54
+68c68
< [100000..2147483647], [100145..2147483647], [100145..2147483647]
---
> [100000..2147483502], [100145..2147483647], [100145..2147483647]
-137c137
+160c160
< x_0 ∈ [100000..2147483647]
---
> x_0 ∈ [100000..2147483502]
diff --git a/tests/value/oracle_symblocs/downcast.1.res.oracle b/tests/value/oracle_symblocs/downcast.1.res.oracle
index 9285a0bd422..58791e9f168 100644
--- a/tests/value/oracle_symblocs/downcast.1.res.oracle
+++ b/tests/value/oracle_symblocs/downcast.1.res.oracle
@@ -1,8 +1,8 @@
-114c114
+128c128
< ux ∈ [--..--]
---
> ux ∈ [0..2147483647]
-157c157
+181c181
< ux ∈ [--..--]
---
> ux ∈ [0..2147483647]
--
GitLab