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;
 


Reply via email to