exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of Expand_N_In...

2016-06-22  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of
	Expand_N_In: within an expanded range check that might raise
	Constraint_Error do not generate a predicate check as well. It
	is redundant because the context will add an explicit predicate
	check, and it will raise the wrong exception if it fails.
	* lib-xref-spark_specific.adb (Add_SPARK_File): Remove useless checks
	since dependency units always have an associated compilation unit.

From-SVN: r237683

gcc/ada/ChangeLog

+2016-06-22  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of
+	Expand_N_In: within an expanded range check that might raise
+	Constraint_Error do not generate a predicate check as well. It
+	is redundant because the context will add an explicit predicate
+	check, and it will raise the wrong exception if it fails.
+	* lib-xref-spark_specific.adb (Add_SPARK_File): Remove useless checks
+	since dependency units always have an associated compilation unit.
+
 2016-06-22  Arnaud Charlet  <charlet@adacore.com>
 
 	* lib.ads: Code cleanup.

gcc/ada/exp_ch4.adb

@@ -6107,18 +6107,60 @@ package body Exp_Ch4 is
       --  (the check is only done when the right operand is a subtype; see
       --  RM12-4.5.2 (28.1/3-30/3)).
 
-      declare
+      Predicate_Check : declare
+         function In_Range_Check return Boolean;
+         --  Within an expanded range check that may raise Constraint_Error do
+         --  not generate a predicate check as well. It is redundant because
+         --  the context will add an explicit predicate check, and it will
+         --  raise the wrong exception if it fails.
+
+         --------------------
+         -- In_Range_Check --
+         --------------------
+
+         function In_Range_Check return Boolean is
+            P : Node_Id;
+         begin
+            P := Parent (N);
+            while Present (P) loop
+               if Nkind (P) = N_Raise_Constraint_Error then
+                  return True;
+
+               elsif Nkind (P) in N_Statement_Other_Than_Procedure_Call
+                 or else Nkind (P) = N_Procedure_Call_Statement
+                 or else Nkind (P) in N_Declaration
+               then
+                  return False;
+               end if;
+
+               P := Parent (P);
+            end loop;
+
+            return False;
+         end In_Range_Check;
+
+         --  Local variables
+
          PFunc : constant Entity_Id := Predicate_Function (Rtyp);
+         R_Op  : Node_Id;
+
+      --  Start of processing for Predicate_Check
 
       begin
          if Present (PFunc)
            and then Current_Scope /= PFunc
            and then Nkind (Rop) /= N_Range
          then
+            if not In_Range_Check then
+               R_Op := Make_Predicate_Call (Rtyp, Lop, Mem => True);
+            else
+               R_Op := New_Occurrence_Of (Standard_True, Loc);
+            end if;
+
             Rewrite (N,
               Make_And_Then (Loc,
                 Left_Opnd  => Relocate_Node (N),
-                Right_Opnd => Make_Predicate_Call (Rtyp, Lop, Mem => True)));
+                Right_Opnd => R_Op));
 
             --  Analyze new expression, mark left operand as analyzed to
             --  avoid infinite recursion adding predicate calls. Similarly,
@@ -6131,7 +6173,7 @@ package body Exp_Ch4 is
 
             return;
          end if;
-      end;
+      end Predicate_Check;
    end Expand_N_In;
 
    --------------------------------

gcc/ada/lib-xref-spark_specific.adb

@@ -153,36 +153,27 @@ package body SPARK_Specific is
       --  Subunits are traversed as part of the top-level unit to which they
       --  belong.
 
-      if Present (Cunit (Ubody))
-        and then Nkind (Unit (Cunit (Ubody))) = N_Subunit
-      then
+      if Nkind (Unit (Cunit (Ubody))) = N_Subunit then
          return;
       end if;
 
       From := SPARK_Scope_Table.Last + 1;
 
-      --  Unit might not have an associated compilation unit, as seen in code
-      --  filling Sdep_Table in Write_ALI.
-
-      if Present (Cunit (Ubody)) then
       Traverse_Compilation_Unit
         (CU           => Cunit (Ubody),
          Process      => Detect_And_Add_SPARK_Scope'Access,
          Inside_Stubs => True);
-      end if;
 
       --  When two units are present for the same compilation unit, as it
       --  happens for library-level instantiations of generics, then add all
       --  scopes to the same SPARK file.
 
       if Ubody /= Uspec then
-         if Present (Cunit (Uspec)) then
          Traverse_Compilation_Unit
            (CU           => Cunit (Uspec),
             Process      => Detect_And_Add_SPARK_Scope'Access,
             Inside_Stubs => True);
       end if;
-      end if;
 
       --  Update scope numbers
 
@@ -209,8 +200,7 @@ package body SPARK_Specific is
       --  For subunits, also retrieve the file name of the unit. Only do so if
       --  unit has an associated compilation unit.
 
-      if Present (Cunit (Uspec))
-        and then Present (Cunit (Unit (File)))
+      if Present (Cunit (Unit (File)))
         and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
       then
          Get_Name_String (Reference_Name (Main_Source_File));