diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 09a1cb3bbc09371d93d886c8002f26dcb6e367ca..17f391e2704081adc407c00bf89c2bfd4ac3437e 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