[Ada] Remove special case for processing null range in GNATprove

Message ID 20200706113854.GA135430@adacore.com
State New
Headers show
Series
  • [Ada] Remove special case for processing null range in GNATprove
Related show

Commit Message

Pierre-Marie de Rodat July 6, 2020, 11:38 a.m.
Historically both low and high range bounds were resolved with the range
type, but we decided to resolve high bound with the range's base type.
This appears to be necessary for having proper range checks in GNATprove
mode, especially for null ranges, but it is no longer needed.

This patch reverts change in Resolve_Range that was made for GNATprove.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_res.adb (Resolve_Range): Resolve both low and high bounds
	with the range type.

Patch

diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -10257,13 +10257,8 @@  package body Sem_Res is
    begin
       Set_Etype (N, Typ);
 
-      --  The lower bound should be in Typ. The higher bound can be in Typ's
-      --  base type if the range is null. It may still be invalid if it is
-      --  higher than the lower bound. This is checked later in the context in
-      --  which the range appears.
-
       Resolve (L, Typ);
-      Resolve (H, Base_Type (Typ));
+      Resolve (H, Typ);
 
       --  Reanalyze the lower bound after both bounds have been analyzed, so
       --  that the range is known to be static or not by now. This may trigger