From 574b1690dac6ac03281477f835d649ca6183f2be Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@cea.fr>
Date: Tue, 5 Sep 2023 14:06:52 +0200
Subject: [PATCH] [kernel] Return typedef in priority
---
src/kernel_services/ast_queries/cil.ml | 7 ++++++-
tests/rte/oracle/addsub_typedef.res.oracle | 7 ++++---
2 files changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 425fd3c893e..f7aaf9c113d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -6541,7 +6541,12 @@ and mkCastTGen ?(check=true) ?context ?(fromsource=false) ?(force=false)
then
begin
Kernel.debug ~dkey "no cast to perform";
- (oldt, e)
+ let returned_type =
+ match newt with
+ | TNamed _ -> newt
+ | _ -> oldt
+ in
+ (returned_type, e)
end
else
let newt = if fromsource then newt else !typeForInsertedCast e oldt newt in
diff --git a/tests/rte/oracle/addsub_typedef.res.oracle b/tests/rte/oracle/addsub_typedef.res.oracle
index 3c40e7028eb..84af60c46ab 100644
--- a/tests/rte/oracle/addsub_typedef.res.oracle
+++ b/tests/rte/oracle/addsub_typedef.res.oracle
@@ -12,7 +12,7 @@
[rte] addsub_typedef.c:13: Warning:
guaranteed RTE:
assert
- signed_overflow: -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
+ signed_overflow: -2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1;
/* Generated by Frama-C */
typedef int tint;
int main(void)
@@ -30,7 +30,7 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1; */
/*@ assert
rte: signed_overflow:
- -2147483648 ≤ (int)(-((int)((int)(-0x7fffffff) - 1))) - 1;
+ -2147483648 ≤ (tint)(-((int)((int)(-0x7fffffff) - 1))) - 1;
*/
z = - (-0x7fffffff - 1) - 1;
z = 0x7fffffff + 0;
@@ -38,7 +38,8 @@ int main(void)
/*@ assert rte: signed_overflow: -2147483648 ≤ x + y; */
/*@ assert rte: signed_overflow: x + y ≤ 2147483647; */
z = x + y;
- /*@ assert rte: signed_overflow: -2147483648 ≤ (int)(-0x7ffffffc) - y; */
+ /*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-0x7ffffffc) - y;
+ */
z = -0x7ffffffc - y;
/*@ assert rte: signed_overflow: -2147483647 ≤ x; */
/*@ assert rte: signed_overflow: -2147483648 ≤ (tint)(-x) - 0x7ffffffc;
--
GitLab