From a0d20d3fff6ce68ef610db7207327ae4172d5975 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 Mar 2020 18:30:27 +0200
Subject: [PATCH] [kernel] fixed oracles wrt old wrong expr-to-term
Fixes incorrect internal casts in sub-terms representing integer C-arith.
---
tests/constant_propagation/oracle/enum.res.oracle | 4 ++--
tests/syntax/oracle/assembly_gmp.1.res.oracle | 6 +++---
tests/syntax/oracle/assembly_gmp.2.res.oracle | 6 +++---
.../oracle/undeclared_local_bts1113.res.oracle | 12 +++++++++---
tests/syntax/oracle/vla_strlen.res.oracle | 6 +++++-
tests/value/oracle/descending.res.oracle | 2 +-
tests/value/oracle/downcast.3.res.oracle | 2 +-
tests/value/oracle/incompatible_states.res.oracle | 6 ++++--
8 files changed, 28 insertions(+), 16 deletions(-)
diff --git a/tests/constant_propagation/oracle/enum.res.oracle b/tests/constant_propagation/oracle/enum.res.oracle
index cbd71cd5823..d7c4e9f6ea0 100644
--- a/tests/constant_propagation/oracle/enum.res.oracle
+++ b/tests/constant_propagation/oracle/enum.res.oracle
@@ -14,7 +14,7 @@
[eva] Recording results for f
[eva] Done for function f
[eva:alarm] tests/constant_propagation/enum.i:13: Warning:
- signed overflow. assert B + c ≤ 2147483647;
+ signed overflow. assert (int)B + c ≤ 2147483647;
[eva:alarm] tests/constant_propagation/enum.i:15: Warning:
signed overflow. assert (int)(y + z) + t ≤ 2147483647;
[eva:alarm] tests/constant_propagation/enum.i:15: Warning:
@@ -43,7 +43,7 @@ int main(int c, unsigned int u)
enum E x = A;
int y = f(0U);
int z = f(D);
- /*@ assert Eva: signed_overflow: B + c ≤ 2147483647; */
+ /*@ assert Eva: signed_overflow: (int)B + c ≤ 2147483647; */
int t = B + c;
int v = (int)(2U + u);
/*@ assert Eva: signed_overflow: (int)(y + z) + t ≤ 2147483647; */
diff --git a/tests/syntax/oracle/assembly_gmp.1.res.oracle b/tests/syntax/oracle/assembly_gmp.1.res.oracle
index 63a12b1b07b..70ffc4d780c 100644
--- a/tests/syntax/oracle/assembly_gmp.1.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.1.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
p0 = (long)(__m0 * __m1);
}
/*@ assigns r2, r1, r0;
- assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+ assigns r2 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+ assigns r1 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
+ assigns r0 \from r0, p1, *(ap + (unsigned long)(n - 3)), p0;
*/
__asm__ (
"add\t%6, %q2\n\t"
diff --git a/tests/syntax/oracle/assembly_gmp.2.res.oracle b/tests/syntax/oracle/assembly_gmp.2.res.oracle
index 2684a9a6655..d3e9aca3737 100644
--- a/tests/syntax/oracle/assembly_gmp.2.res.oracle
+++ b/tests/syntax/oracle/assembly_gmp.2.res.oracle
@@ -38,9 +38,9 @@ mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
p0 = (long)(__m0 * __m1);
}
/*@ assigns r2, r1, r0;
- assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
- assigns r0 \from r0, p1, *(ap + (n - 3)), p0;
+ assigns r2 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+ assigns r1 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
+ assigns r0 \from r0, p1, *(ap + (unsigned int)(n - 3)), p0;
*/
__asm__ (
"add%I6c\t%2, %5, %6\n\t"
diff --git a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
index 809576ab5a8..97b551d63eb 100644
--- a/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
+++ b/tests/syntax/oracle/undeclared_local_bts1113.res.oracle
@@ -16,19 +16,25 @@ void funk(int rounds)
int i;
unsigned int __lengthof_k_long_long_size;
int k_positive_size[4 - 2];
- /*@ assert alloca_bounds: 0 < sizeof(int) * (2 * rounds) ≤ 4294967295; */
+ /*@
+ assert alloca_bounds: 0 < sizeof(int) * (int)(2 * rounds) ≤ 4294967295;
+ */
;
__lengthof_k = (unsigned int)(2 * rounds);
int *k = __fc_vla_alloc(sizeof(int) * __lengthof_k);
/*@
assert
- alloca_bounds: 0 < sizeof(int) * (unsigned int)(2 * rounds) ≤ 4294967295;
+ alloca_bounds:
+ 0 < sizeof(int) * (unsigned int)((int)(2 * rounds)) ≤ 4294967295;
*/
;
__lengthof_kk = (unsigned int)(2 * rounds);
int *kk = __fc_vla_alloc(sizeof(int) * __lengthof_kk);
long long j = (long long)(rounds * rounds);
- /*@ assert alloca_bounds: 0 < sizeof(int) * (j * 2) ≤ 4294967295; */ ;
+ /*@
+ assert alloca_bounds: 0 < sizeof(int) * (long long)(j * 2) ≤ 4294967295;
+ */
+ ;
__lengthof_k_long_long_size = (unsigned int)(j * (long long)2);
int *k_long_long_size =
__fc_vla_alloc(sizeof(int) * __lengthof_k_long_long_size);
diff --git a/tests/syntax/oracle/vla_strlen.res.oracle b/tests/syntax/oracle/vla_strlen.res.oracle
index 49dc5fb0597..0fe38231c89 100644
--- a/tests/syntax/oracle/vla_strlen.res.oracle
+++ b/tests/syntax/oracle/vla_strlen.res.oracle
@@ -17,7 +17,11 @@ void f(char *s)
unsigned int __lengthof_t;
size_t tmp;
tmp = strlen((char const *)s);
- /*@ assert alloca_bounds: 0 < sizeof(char) * (tmp + 1) ≤ 4294967295; */ ;
+ /*@
+ assert
+ alloca_bounds: 0 < sizeof(char) * (unsigned int)(tmp + 1) ≤ 4294967295;
+ */
+ ;
__lengthof_t = tmp + (size_t)1;
char *t = __fc_vla_alloc(sizeof(char) * __lengthof_t);
char *p = t;
diff --git a/tests/value/oracle/descending.res.oracle b/tests/value/oracle/descending.res.oracle
index 3b11d3495c6..7e67df6441b 100644
--- a/tests/value/oracle/descending.res.oracle
+++ b/tests/value/oracle/descending.res.oracle
@@ -14,7 +14,7 @@
[eva:alarm] tests/value/descending.i:13: Warning:
accessing out of bounds index. assert (int)(i - 1) < 10;
[eva:alarm] tests/value/descending.i:13: Warning:
- accessing uninitialized left-value. assert \initialized(&A[i - 1]);
+ accessing uninitialized left-value. assert \initialized(&A[(int)(i - 1)]);
[eva] Recording results for test1
[eva] Done for function test1
[eva] computing for function test2 <- main.
diff --git a/tests/value/oracle/downcast.3.res.oracle b/tests/value/oracle/downcast.3.res.oracle
index 8f130d992c0..8d2a9ee99b2 100644
--- a/tests/value/oracle/downcast.3.res.oracle
+++ b/tests/value/oracle/downcast.3.res.oracle
@@ -61,7 +61,7 @@
[eva] computing for function main6_val_warn_converted_signed <- main.
Called from tests/value/downcast.i:161.
[eva:alarm] tests/value/downcast.i:75: Warning:
- signed downcast. assert (int)65300u ≤ 32767;
+ signed downcast. assert 65300u ≤ 32767;
[eva:alarm] tests/value/downcast.i:91: Warning:
signed downcast. assert -32768 ≤ (int)e_1;
[eva:alarm] tests/value/downcast.i:95: Warning:
diff --git a/tests/value/oracle/incompatible_states.res.oracle b/tests/value/oracle/incompatible_states.res.oracle
index 9cd3bb24391..d020cc43176 100644
--- a/tests/value/oracle/incompatible_states.res.oracle
+++ b/tests/value/oracle/incompatible_states.res.oracle
@@ -22,9 +22,11 @@
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva:alarm] tests/value/incompatible_states.c:38: Warning:
- accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+ accessing uninitialized left-value.
+ assert \initialized(&t[(int)((int)(2 * i) / 2)]);
[eva:alarm] tests/value/incompatible_states.c:41: Warning:
- accessing uninitialized left-value. assert \initialized(&t[(2 * i) / 2]);
+ accessing uninitialized left-value.
+ assert \initialized(&t[(int)((int)(2 * i) / 2)]);
[eva] Recording results for main2
[eva] Done for function main2
[eva] computing for function main3 <- main.
--
GitLab