https://gcc.gnu.org/g:b0483f45604396756a0131f724ed4464d45c68dd
commit r17-938-gb0483f45604396756a0131f724ed4464d45c68dd Author: Javier Miranda <[email protected]> Date: Fri Mar 13 19:48:26 2026 +0000 ada: Missing overflow check on Integer_128 under GNATProve mode Under GNATProve mode the frontend does not generate overflow checks on type conversions of Universal Integer numbers to 128-bit integer type numbers. gcc/ada/ChangeLog: * checks.adb (Apply_Scalar_Range_Check): When the type of the expression is Universal Integer we cannot statically determine if the expression is in the range of the target type. * sem_eval.adb (In_Subrange_Of): Do not consider T2 in the range of Universal Integer (since theoretically they are not). (Test_In_Range): Do not consider Universal type expressions in range of subtype Typ. Diff: --- gcc/ada/checks.adb | 8 ++++++++ gcc/ada/sem_eval.adb | 17 +++++++++++++++++ 2 files changed, 25 insertions(+) diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index 3a0f86fc7f2c..8e6fba46b82e 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -3367,6 +3367,12 @@ package body Checks is -- for floating-point types. But the additional less precise tests below -- catch these cases. + -- Under GNATProve mode, when the type of the expression is Universal + -- Integer we cannot determine if the expression is in the range of the + -- target type. Required because, Universal_Integer is implemented as a + -- 128-bit type but, in theory, its values may be out of range for + -- 128-bit target types. + -- Note: skip this if we are given a source_typ, since the point of -- supplying a Source_Typ is to stop us looking at the expression. -- We could sharpen this test to be out parameters only ??? @@ -3374,6 +3380,8 @@ package body Checks is if Is_Discrete_Type (Target_Typ) and then not Is_Unconstrained_Subscr_Ref and then No (Source_Typ) + and then not (Etype (Expr) = Universal_Integer + and then GNATprove_Mode) then declare Thi : constant Node_Id := Type_High_Bound (Target_Typ); diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index 0ccd32f13896..ffbb444cfe1f 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -5351,6 +5351,15 @@ package body Sem_Eval is then return False; + -- Under GNATprove mode, do not consider T2 in the range of Universal + -- Integer (since theoretically they are not); required because + -- Universal_Integer is implemented as a 128-bits type. + + elsif GNATprove_Mode + and then T1 = Universal_Integer + then + return False; + else L1 := Type_Low_Bound (T1); H1 := Type_High_Bound (T1); @@ -7388,6 +7397,14 @@ package body Sem_Eval is elsif Is_Universal_Numeric_Type (Typ) then return In_Range; + -- Under GNATprove mode, Universal type expressions are not in range + -- of subtype Typ. + + elsif GNATprove_Mode + and then Is_Universal_Numeric_Type (Etype (N)) + then + return Unknown; + -- Never known if not scalar type. Don't know if this can actually -- happen, but our spec allows it, so we must check.
