Similar to what is done for compilation, range checks should not be
applied inside generics during GNATprove analysis. This fixes an
assertion failure in GNATprove.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* checks.adb (Selected_Range_Checks): Adapt the condition for
applying range checks so that it is not done inside generics.
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -10585,10 +10585,10 @@ package body Checks is
begin
-- Checks will be applied only when generating code. In GNATprove mode,
-- we do not apply the checks, but we still call Selected_Range_Checks
- -- to possibly issue errors on SPARK code when a run-time error can be
- -- detected at compile time.
+ -- outside of generics to possibly issue errors on SPARK code when a
+ -- run-time error can be detected at compile time.
- if not Expander_Active and not GNATprove_Mode then
+ if Inside_A_Generic or (not GNATprove_Mode and not Expander_Active) then
return Ret_Result;
end if;