From 2b91fda9e122ff35baffa332229c0408caed991f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 12 Mar 2020 11:39:11 +0100
Subject: [PATCH] [kernel] Do not restrict cast to unsigned expressions for
downcasts
---
src/kernel_services/ast_data/alarms.ml | 3 +-
tests/rte/oracle/bts2314.res.oracle | 4 +--
tests/rte/oracle/divmod.res.oracle | 6 ++--
tests/rte/oracle/divmod_typedef.res.oracle | 6 ++--
tests/rte/oracle/downcast.0.res.oracle | 4 +--
tests/rte/oracle/downcast.2.res.oracle | 8 +++---
tests/rte/oracle/minus.0.res.oracle | 4 +--
tests/rte/oracle/minus.1.res.oracle | 4 +--
.../oracle/signed_downcast.1.res.oracle | 4 +--
.../oracle/unsigned_downcast.res.oracle | 4 +--
tests/value/oracle/downcast.res.oracle | 28 +++++++++----------
11 files changed, 39 insertions(+), 36 deletions(-)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index 261c438947f..4bf060e886e 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -550,8 +550,7 @@ let create_predicate ?(loc=Location.unknown) alarm =
let loc = best_loc ~loc e.eloc in
let exp_type = Cil.typeOf e in
let t = match kind with
- | Signed_downcast | Unsigned_downcast
- when Cil.isUnsignedInteger exp_type ->
+ | Signed_downcast | Unsigned_downcast ->
let t = overflowed_expr_to_term ~loc e in
(* Without this cast, the alarm is:
- Signed_downcast: unsound ->
diff --git a/tests/rte/oracle/bts2314.res.oracle b/tests/rte/oracle/bts2314.res.oracle
index 7f03e2a4217..6ac02f4397c 100644
--- a/tests/rte/oracle/bts2314.res.oracle
+++ b/tests/rte/oracle/bts2314.res.oracle
@@ -12,8 +12,8 @@ void foo(int a, long b)
s.num = (int)b;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)s.num + a; */
/*@ assert rte: signed_overflow: (int)s.num + a ≤ 2147483647; */
- /*@ assert rte: signed_downcast: (int)s.num + a ≤ 63; */
- /*@ assert rte: signed_downcast: -64 ≤ (int)s.num + a; */
+ /*@ assert rte: signed_downcast: (int)((int)s.num + a) ≤ 63; */
+ /*@ assert rte: signed_downcast: -64 ≤ (int)((int)s.num + a); */
s.num = (int)((int)s.num + a);
return;
}
diff --git a/tests/rte/oracle/divmod.res.oracle b/tests/rte/oracle/divmod.res.oracle
index 19f1dcc24f0..01fa69c0ee7 100644
--- a/tests/rte/oracle/divmod.res.oracle
+++ b/tests/rte/oracle/divmod.res.oracle
@@ -20,7 +20,8 @@
guaranteed RTE:
assert
signed_downcast:
- (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
/* Generated by Frama-C */
int main(void)
{
@@ -70,7 +71,8 @@ int main(void)
z = (-0x7ffffff - 1) / y;
/*@ assert
rte: signed_downcast:
- (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
*/
z = (int)(-2147483648L / (long long)(-1L));
z = (int)(0x80000000 / (unsigned int)(-1));
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 17b553cb32d..51b06e5796e 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -20,7 +20,8 @@
guaranteed RTE:
assert
signed_downcast:
- (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
/* Generated by Frama-C */
typedef int tint;
typedef unsigned int tuint;
@@ -72,7 +73,8 @@ int main(void)
z = (-0x7ffffff - 1) / y;
/*@ assert
rte: signed_downcast:
- (long long)(-2147483648L) / (long long)((long)(-1L)) ≤ 2147483647;
+ (long long)((long long)(-2147483648L) / (long long)((long)(-1L))) ≤
+ 2147483647;
*/
z = (int)(-2147483648L / (long long)(-1L));
z = (int)(0x80000000 / (unsigned int)(-1));
diff --git a/tests/rte/oracle/downcast.0.res.oracle b/tests/rte/oracle/downcast.0.res.oracle
index 5963c8e9adf..3097cab2fa8 100644
--- a/tests/rte/oracle/downcast.0.res.oracle
+++ b/tests/rte/oracle/downcast.0.res.oracle
@@ -15,8 +15,8 @@ int main(void)
unsigned short s;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
/*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
- /*@ assert rte: signed_downcast: (int)sx + (int)sy ≤ 127; */
- /*@ assert rte: signed_downcast: -128 ≤ (int)sx + (int)sy; */
+ /*@ assert rte: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
+ /*@ assert rte: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
sz = (signed char)((int)sx + (int)sy);
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
/*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
diff --git a/tests/rte/oracle/downcast.2.res.oracle b/tests/rte/oracle/downcast.2.res.oracle
index dd0102f2be0..8413d87dbce 100644
--- a/tests/rte/oracle/downcast.2.res.oracle
+++ b/tests/rte/oracle/downcast.2.res.oracle
@@ -15,13 +15,13 @@ int main(void)
unsigned short s;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
/*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
- /*@ assert rte: signed_downcast: (int)sx + (int)sy ≤ 127; */
- /*@ assert rte: signed_downcast: -128 ≤ (int)sx + (int)sy; */
+ /*@ assert rte: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
+ /*@ assert rte: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
sz = (signed char)((int)sx + (int)sy);
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)sx + (int)sy; */
/*@ assert rte: signed_overflow: (int)sx + (int)sy ≤ 2147483647; */
- /*@ assert rte: unsigned_downcast: (int)sx + (int)sy ≤ 255; */
- /*@ assert rte: unsigned_downcast: 0 ≤ (int)sx + (int)sy; */
+ /*@ assert rte: unsigned_downcast: (int)((int)sx + (int)sy) ≤ 255; */
+ /*@ assert rte: unsigned_downcast: 0 ≤ (int)((int)sx + (int)sy); */
uc = (unsigned char)((int)sx + (int)sy);
/*@ assert rte: unsigned_downcast: x ≤ 255; */
/*@ assert rte: unsigned_downcast: 0 ≤ x; */
diff --git a/tests/rte/oracle/minus.0.res.oracle b/tests/rte/oracle/minus.0.res.oracle
index ea9f8124d52..19845be6ff9 100644
--- a/tests/rte/oracle/minus.0.res.oracle
+++ b/tests/rte/oracle/minus.0.res.oracle
@@ -36,11 +36,11 @@ int main(void)
*/
/*@ assert
rte: signed_downcast:
- (int)((unsigned short)((int)(65535 + 3))) + x ≤ 32767;
+ (int)((int)((unsigned short)((int)(65535 + 3))) + x) ≤ 32767;
*/
/*@ assert
rte: signed_downcast:
- -32768 ≤ (int)((unsigned short)((int)(65535 + 3))) + x;
+ -32768 ≤ (int)((int)((unsigned short)((int)(65535 + 3))) + x);
*/
sz = (short)((int)((unsigned short)(65535 + 3)) + x);
z = (int)(-0x80000000 - (unsigned int)1);
diff --git a/tests/rte/oracle/minus.1.res.oracle b/tests/rte/oracle/minus.1.res.oracle
index 8e295b1e3cf..9b6eb5d89be 100644
--- a/tests/rte/oracle/minus.1.res.oracle
+++ b/tests/rte/oracle/minus.1.res.oracle
@@ -34,11 +34,11 @@ int main(void)
*/
/*@ assert
rte: signed_downcast:
- (int)((unsigned short)((int)(65535 + 3))) + x ≤ 32767;
+ (int)((int)((unsigned short)((int)(65535 + 3))) + x) ≤ 32767;
*/
/*@ assert
rte: signed_downcast:
- -32768 ≤ (int)((unsigned short)((int)(65535 + 3))) + x;
+ -32768 ≤ (int)((int)((unsigned short)((int)(65535 + 3))) + x);
*/
sz = (short)((int)((unsigned short)(65535 + 3)) + x);
/*@ assert
diff --git a/tests/rte_manual/oracle/signed_downcast.1.res.oracle b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
index b53eac56ff9..508313da76c 100644
--- a/tests/rte_manual/oracle/signed_downcast.1.res.oracle
+++ b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
@@ -9,8 +9,8 @@ int main(void)
signed char cz;
/*@ assert rte: signed_overflow: -2147483648 ≤ (int)cx + (int)cy; */
/*@ assert rte: signed_overflow: (int)cx + (int)cy ≤ 2147483647; */
- /*@ assert rte: signed_downcast: (int)cx + (int)cy ≤ 127; */
- /*@ assert rte: signed_downcast: -128 ≤ (int)cx + (int)cy; */
+ /*@ assert rte: signed_downcast: (int)((int)cx + (int)cy) ≤ 127; */
+ /*@ assert rte: signed_downcast: -128 ≤ (int)((int)cx + (int)cy); */
cz = (signed char)((int)cx + (int)cy);
__retres = 0;
return __retres;
diff --git a/tests/rte_manual/oracle/unsigned_downcast.res.oracle b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
index 01400f1cd74..30bacde2ada 100644
--- a/tests/rte_manual/oracle/unsigned_downcast.res.oracle
+++ b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
@@ -6,8 +6,8 @@ unsigned char f(int a, int b)
unsigned char __retres;
/*@ assert rte: signed_overflow: -2147483648 ≤ a + b; */
/*@ assert rte: signed_overflow: a + b ≤ 2147483647; */
- /*@ assert rte: unsigned_downcast: a + b ≤ 255; */
- /*@ assert rte: unsigned_downcast: 0 ≤ a + b; */
+ /*@ assert rte: unsigned_downcast: (int)(a + b) ≤ 255; */
+ /*@ assert rte: unsigned_downcast: 0 ≤ (int)(a + b); */
__retres = (unsigned char)(a + b);
return __retres;
}
diff --git a/tests/value/oracle/downcast.res.oracle b/tests/value/oracle/downcast.res.oracle
index 7df2a56ff7b..18b563a5f18 100644
--- a/tests/value/oracle/downcast.res.oracle
+++ b/tests/value/oracle/downcast.res.oracle
@@ -16,9 +16,9 @@
[eva] computing for function main1 <- main.
Called from tests/value/downcast.i:152.
[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert -128 ≤ (int)sx + (int)sy;
+ signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert (int)sx + (int)sy ≤ 127;
+ signed downcast. assert (int)((int)sx + (int)sy) ≤ 127;
[eva:alarm] tests/value/downcast.i:22: Warning:
signed downcast. assert (unsigned int)(uy + uz) ≤ 2147483647;
[eva] Recording results for main1
@@ -440,8 +440,8 @@ unsigned short s;
int volatile v;
void main1(void)
{
- /*@ assert Eva: signed_downcast: -128 ≤ (int)sx + (int)sy; */
- /*@ assert Eva: signed_downcast: (int)sx + (int)sy ≤ 127; */
+ /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
+ /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
sz = (signed char)((int)sx + (int)sy);
uc = (unsigned char)((int)sx + (int)sy);
uc = (unsigned char)x;
@@ -642,7 +642,7 @@ void main(void)
[eva] computing for function main1 <- main.
Called from tests/value/downcast.i:152.
[eva:alarm] tests/value/downcast.i:20: Warning:
- unsigned downcast. assert 0 ≤ (int)sx + (int)sy;
+ unsigned downcast. assert 0 ≤ (int)((int)sx + (int)sy);
[eva:alarm] tests/value/downcast.i:21: Warning:
unsigned downcast. assert 0 ≤ x;
[eva:alarm] tests/value/downcast.i:21: Warning:
@@ -688,9 +688,9 @@ void main(void)
[eva] computing for function main6_val_warn_converted_signed <- main.
Called from tests/value/downcast.i:157.
[eva:alarm] tests/value/downcast.i:81: Warning:
- unsigned downcast. assert 0 ≤ -12;
+ unsigned downcast. assert 0 ≤ (int)(-12);
[eva:alarm] tests/value/downcast.i:86: Warning:
- unsigned downcast. assert 0 ≤ -64000;
+ unsigned downcast. assert 0 ≤ (int)(-64000);
[eva] tests/value/downcast.i:92:
Assigning imprecise value to y.
The imprecision originates from Arithmetic {tests/value/downcast.i:92}
@@ -997,7 +997,7 @@ int volatile v;
void main1(void)
{
sz = (signed char)((int)sx + (int)sy);
- /*@ assert Eva: unsigned_downcast: 0 ≤ (int)sx + (int)sy; */
+ /*@ assert Eva: unsigned_downcast: 0 ≤ (int)((int)sx + (int)sy); */
uc = (unsigned char)((int)sx + (int)sy);
/*@ assert Eva: unsigned_downcast: 0 ≤ x; */
/*@ assert Eva: unsigned_downcast: x ≤ 255; */
@@ -1081,12 +1081,12 @@ void main6_val_warn_converted_signed(void)
short b = (short)e;
}
if (v) {
- /*@ assert Eva: unsigned_downcast: 0 ≤ -12; */
+ /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-12); */
unsigned long e_0 = (unsigned long)(-12);
short b_0 = (short)e_0;
}
if (v) {
- /*@ assert Eva: unsigned_downcast: 0 ≤ -64000; */
+ /*@ assert Eva: unsigned_downcast: 0 ≤ (int)(-64000); */
unsigned int e_1 = (unsigned int)(-64000);
short b_1 = (short)e_1;
}
@@ -1191,9 +1191,9 @@ void main(void)
[eva] computing for function main1 <- main.
Called from tests/value/downcast.i:152.
[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert -128 ≤ (int)sx + (int)sy;
+ signed downcast. assert -128 ≤ (int)((int)sx + (int)sy);
[eva:alarm] tests/value/downcast.i:19: Warning:
- signed downcast. assert (int)sx + (int)sy ≤ 127;
+ 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.
@@ -1556,8 +1556,8 @@ unsigned short s;
int volatile v;
void main1(void)
{
- /*@ assert Eva: signed_downcast: -128 ≤ (int)sx + (int)sy; */
- /*@ assert Eva: signed_downcast: (int)sx + (int)sy ≤ 127; */
+ /*@ assert Eva: signed_downcast: -128 ≤ (int)((int)sx + (int)sy); */
+ /*@ assert Eva: signed_downcast: (int)((int)sx + (int)sy) ≤ 127; */
sz = (signed char)((int)sx + (int)sy);
uc = (unsigned char)((int)sx + (int)sy);
uc = (unsigned char)x;
--
GitLab