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 --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 3a0f86fc7f2cea6354c6e5eaaf011a7dc2fdc4c5..8e6fba46b82eae141154c48c78241cdc85db4aa0 100644 (file)
--- 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 0ccd32f13896cf49578ab41f46f840e5ed43d572..ffbb444cfe1f53b9b7e12debd5b3e97ee1e5d31a 100644 (file)
--- 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.