@@ -142,6 +142,16 @@ package body Sem_Eval is
-- Local Subprograms --
-----------------------
+ procedure Check_Non_Static_Context_For_Overflow
+ (N : Node_Id;
+ Stat : Boolean;
+ Result : Uint);
+ -- For a signed integer type, check non-static overflow in Result when
+ -- Stat is False. This applies also inside inlined code, where the static
+ -- property may be an effect of the inlining, which should not be allowed
+ -- to remove run-time checks (whether during compilation, or even more
+ -- crucially in the special inlining-for-proof in GNATprove mode).
+
function Choice_Matches
(Expr : Node_Id;
Choice : Node_Id) return Match_Result;
@@ -649,6 +659,34 @@ package body Sem_Eval is
end if;
end Check_Non_Static_Context;
+ -------------------------------------------
+ -- Check_Non_Static_Context_For_Overflow --
+ -------------------------------------------
+
+ procedure Check_Non_Static_Context_For_Overflow
+ (N : Node_Id;
+ Stat : Boolean;
+ Result : Uint)
+ is
+ begin
+ if (not Stat or else In_Inlined_Body)
+ and then Is_Signed_Integer_Type (Etype (N))
+ then
+ declare
+ BT : constant Entity_Id := Base_Type (Etype (N));
+ Lo : constant Uint := Expr_Value (Type_Low_Bound (BT));
+ Hi : constant Uint := Expr_Value (Type_High_Bound (BT));
+ begin
+ if Result < Lo or else Result > Hi then
+ Apply_Compile_Time_Constraint_Error
+ (N, "value not in range of }??",
+ CE_Overflow_Check_Failed,
+ Ent => BT);
+ end if;
+ end;
+ end if;
+ end Check_Non_Static_Context_For_Overflow;
+
---------------------------------
-- Check_String_Literal_Length --
---------------------------------
@@ -2143,25 +2181,10 @@ package body Sem_Eval is
if Is_Modular_Integer_Type (Ltype) then
Result := Result mod Modulus (Ltype);
-
- -- For a signed integer type, check non-static overflow
-
- elsif (not Stat) and then Is_Signed_Integer_Type (Ltype) then
- declare
- BT : constant Entity_Id := Base_Type (Ltype);
- Lo : constant Uint := Expr_Value (Type_Low_Bound (BT));
- Hi : constant Uint := Expr_Value (Type_High_Bound (BT));
- begin
- if Result < Lo or else Result > Hi then
- Apply_Compile_Time_Constraint_Error
- (N, "value not in range of }??",
- CE_Overflow_Check_Failed,
- Ent => BT);
- return;
- end if;
- end;
end if;
+ Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
-- If we get here we can fold the result
Fold_Uint (N, Result, Stat);
@@ -3202,6 +3225,8 @@ package body Sem_Eval is
Result := Result mod Modulus (Etype (N));
end if;
+ Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
Fold_Uint (N, Result, Stat);
end if;
end;
@@ -4375,6 +4400,8 @@ package body Sem_Eval is
Result := abs Rint;
end if;
+ Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
Fold_Uint (N, Result, Stat);
end;