From db081543c00cbe36eaee4a420e6ecade237d58b2 Mon Sep 17 00:00:00 2001
From: Pierre Nigron <pierre.nigron@cea.fr>
Date: Thu, 31 Aug 2023 09:20:42 +0200
Subject: [PATCH] [kernel] Plus Integer Promotion
---
src/kernel_internals/typing/cabs2cil.ml | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 09a1cb3bbc0..17f391e2704 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -6067,7 +6067,17 @@ and doExp local_env
else
abort_context "Unary ~ on a non-integral type"
- | Cabs.UNARY(Cabs.PLUS, e) -> doExp (no_paren_local_env local_env) asconst e what
+ | Cabs.UNARY(Cabs.PLUS, e) ->
+ let (r, se, e, t as v) = doExp (no_paren_local_env local_env) asconst e what in
+ if isIntegralType t then
+ let newt = integralPromotion t in
+ let e' = makeCastT ~e ~oldt:t ~newt in
+ finishExp r se e' newt
+ else
+ if isArithmeticType t then
+ v
+ else
+ abort_context "Unary + on a non-arithmetic type"
| Cabs.UNARY(Cabs.ADDROF, e) ->
(* some normalization is needed here to remove potential COMMA, QUESTION
--
GitLab