sem_aux.adb, [...] (Get_Called_Entity): New function to return the entity associated with the call.

2017-09-08  Yannick Moy  <moy@adacore.com>

	* sem_aux.adb, sem_aux.ads (Get_Called_Entity): New function to
	return the entity associated with the call.
	* sem_util.adb, sem_util.ads (Check_Function_Writable_Actuals):
	Replace the internal Get_Function_Id with the new
	Sem_Aux.Get_Called_Entity.
	(Iterate_Call_Parameters): New
	procedure to iterate on formals and actuals at the same time.
	* sem_ch12.adb (Analyze_Subprogram_Instantiation):
	Set SPARK_Mode from spec when set, for analysis
	of instance. Restore after analysis of instance.
	(Instantiate_Subprogram_Body): Set SPARK_Mode from body when
	set, for analysis of body instance. Restored automatically at
	the end of the subprogram.
	* gnat1drv.adb (Adjust_Global_Switches): Set
	Check_Validity_Of_Parameters to False in GNATprove mode.
	* opt.ads (Check_Validity_Of_Parameters): Document switch to
	set option.

From-SVN: r251900

gcc/ada/ChangeLog

+2017-09-08  Yannick Moy  <moy@adacore.com>
+
+	* sem_aux.adb, sem_aux.ads (Get_Called_Entity): New function to
+	return the entity associated with the call.
+	* sem_util.adb, sem_util.ads (Check_Function_Writable_Actuals):
+	Replace the internal Get_Function_Id with the new
+	Sem_Aux.Get_Called_Entity.
+	(Iterate_Call_Parameters): New
+	procedure to iterate on formals and actuals at the same time.
+	* sem_ch12.adb (Analyze_Subprogram_Instantiation):
+	Set SPARK_Mode from spec when set, for analysis
+	of instance. Restore after analysis of instance.
+	(Instantiate_Subprogram_Body): Set SPARK_Mode from body when
+	set, for analysis of body instance. Restored automatically at
+	the end of the subprogram.
+	* gnat1drv.adb (Adjust_Global_Switches): Set
+	Check_Validity_Of_Parameters to False in GNATprove mode.
+	* opt.ads (Check_Validity_Of_Parameters): Document switch to
+	set option.
+
 2017-09-08  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* sem_util.adb (NCT_Tables_In_Use): Move to library level from...

gcc/ada/sem_aux.adb

@@ -459,6 +459,32 @@ package body Sem_Aux is
       end case;
    end Get_Binary_Nkind;
 
+   -----------------------
+   -- Get_Called_Entity --
+   -----------------------
+
+   function Get_Called_Entity (Call : Node_Id) return Entity_Id is
+      Nam : constant Node_Id := Name (Call);
+      Id  : Entity_Id;
+
+   begin
+      if Nkind (Nam) = N_Explicit_Dereference then
+         Id := Etype (Nam);
+         pragma Assert (Ekind (Id) = E_Subprogram_Type);
+
+      elsif Nkind (Nam) = N_Selected_Component then
+         Id := Entity (Selector_Name (Nam));
+
+      elsif Nkind (Nam) = N_Indexed_Component then
+         Id := Entity (Selector_Name (Prefix (Nam)));
+
+      else
+         Id := Entity (Nam);
+      end if;
+
+      return Id;
+   end Get_Called_Entity;
+
    -------------------
    -- Get_Low_Bound --
    -------------------

gcc/ada/sem_aux.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -161,8 +161,11 @@ package Sem_Aux is
    --  referencing this entity. It is an error to call this function if Ekind
    --  (Op) /= E_Operator.
 
+   function Get_Called_Entity (Call : Node_Id) return Entity_Id;
+   --  Returns the entity associated with the call
+
    function Get_Low_Bound (E : Entity_Id) return Node_Id;
-   --  For an index subtype or string literal subtype, return its low bound
+   --  For an index subtype or string literal subtype, returns its low bound
 
    function Get_Unary_Nkind (Op : Entity_Id) return Node_Kind;
    --  Op must be an entity with an Ekind of E_Operator. This function returns

gcc/ada/sem_ch12.adb

@@ -5445,8 +5445,30 @@ package body Sem_Ch12 is
             Ignore_SPARK_Mode_Pragmas_In_Instance := True;
          end if;
 
+         --  If the context of an instance is not subject to SPARK_Mode "off",
+         --  and the generic spec is subject to an explicit SPARK_Mode pragma,
+         --  the latter should be the one applicable to the instance.
+
+         if not Ignore_SPARK_Mode_Pragmas_In_Instance
+           and then Saved_SM /= Off
+           and then Present (SPARK_Pragma (Gen_Unit))
+         then
+            Set_SPARK_Mode (Gen_Unit);
+         end if;
+
          Analyze_Instance_And_Renamings;
 
+         --  Restore SPARK_Mode from the context after analysis of the package
+         --  declaration, so that the SPARK_Mode on the generic spec does not
+         --  apply to the pending instance for the instance body.
+
+         if not Ignore_SPARK_Mode_Pragmas_In_Instance
+           and then Saved_SM /= Off
+           and then Present (SPARK_Pragma (Gen_Unit))
+         then
+            Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+         end if;
+
          --  If the generic is marked Import (Intrinsic), then so is the
          --  instance. This indicates that there is no body to instantiate. If
          --  generic is marked inline, so it the instance, and the anonymous
@@ -11511,7 +11533,9 @@ package body Sem_Ch12 is
       Opt.Ada_Version_Pragma   := Body_Info.Version_Pragma;
       Restore_Warnings (Body_Info.Warnings);
 
-      --  Install the SPARK mode which applies to the subprogram body
+      --  Install the SPARK mode which applies to the subprogram body from the
+      --  instantiation context. This may be refined further if an explicit
+      --  SPARK_Mode pragma applies to the generic body.
 
       Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
 
@@ -11573,6 +11597,17 @@ package body Sem_Ch12 is
             Ignore_SPARK_Mode_Pragmas_In_Instance := True;
          end if;
 
+         --  If the context of an instance is not subject to SPARK_Mode "off",
+         --  and the generic body is subject to an explicit SPARK_Mode pragma,
+         --  the latter should be the one applicable to the instance.
+
+         if not Ignore_SPARK_Mode_Pragmas_In_Instance
+           and then SPARK_Mode /= Off
+           and then Present (SPARK_Pragma (Gen_Body_Id))
+         then
+            Set_SPARK_Mode (Gen_Body_Id);
+         end if;
+
          Current_Sem_Unit := Body_Info.Current_Sem_Unit;
          Create_Instantiation_Source
            (Inst_Node,

gcc/ada/sem_util.adb

@@ -2122,9 +2122,6 @@ package body Sem_Util is
       --  second occurrence, the error is reported, and the tree traversal
       --  is abandoned.
 
-      function Get_Function_Id (Call : Node_Id) return Entity_Id;
-      --  Return the entity associated with the function call
-
       procedure Preanalyze_Without_Errors (N : Node_Id);
       --  Preanalyze N without reporting errors. Very dubious, you can't just
       --  go analyzing things more than once???
@@ -2212,7 +2209,7 @@ package body Sem_Util is
                      Formal : Node_Id;
 
                   begin
-                     Id := Get_Function_Id (Call);
+                     Id := Get_Called_Entity (Call);
 
                      --  In case of previous error, no check is possible
 
@@ -2358,32 +2355,6 @@ package body Sem_Util is
          Do_Traversal (N);
       end Collect_Identifiers;
 
-      ---------------------
-      -- Get_Function_Id --
-      ---------------------
-
-      function Get_Function_Id (Call : Node_Id) return Entity_Id is
-         Nam : constant Node_Id := Name (Call);
-         Id  : Entity_Id;
-
-      begin
-         if Nkind (Nam) = N_Explicit_Dereference then
-            Id := Etype (Nam);
-            pragma Assert (Ekind (Id) = E_Subprogram_Type);
-
-         elsif Nkind (Nam) = N_Selected_Component then
-            Id := Entity (Selector_Name (Nam));
-
-         elsif Nkind (Nam) = N_Indexed_Component then
-            Id := Entity (Selector_Name (Prefix (Nam)));
-
-         else
-            Id := Entity (Nam);
-         end if;
-
-         return Id;
-      end Get_Function_Id;
-
       -------------------------------
       -- Preanalyze_Without_Errors --
       -------------------------------
@@ -2523,7 +2494,7 @@ package body Sem_Util is
             | N_Subprogram_Call
          =>
             declare
-               Id     : constant Entity_Id := Get_Function_Id (N);
+               Id     : constant Entity_Id := Get_Called_Entity (N);
                Formal : Node_Id;
                Actual : Node_Id;
 
@@ -16391,6 +16362,22 @@ package body Sem_Util is
       end if;
    end Is_Volatile_Object;
 
+   -----------------------------
+   -- Iterate_Call_Parameters --
+   -----------------------------
+
+   procedure Iterate_Call_Parameters (Call : Node_Id) is
+      Formal : Entity_Id := First_Formal (Get_Called_Entity (Call));
+      Actual : Node_Id   := First_Actual (Call);
+
+   begin
+      while Present (Formal) and then Present (Actual) loop
+         Handle_Parameter (Formal, Actual);
+         Formal := Next_Formal (Formal);
+         Actual := Next_Actual (Actual);
+      end loop;
+   end Iterate_Call_Parameters;
+
    ---------------------------
    -- Itype_Has_Declaration --
    ---------------------------

gcc/ada/sem_util.ads

@@ -1943,6 +1943,12 @@ package Sem_Util is
    --  for something actually declared as volatile, not for an object that gets
    --  treated as volatile (see Einfo.Treat_As_Volatile).
 
+   generic
+      with procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id);
+   procedure Iterate_Call_Parameters (Call : Node_Id);
+   --  Calls Handle_Parameter for each pair of formal and actual parameters of
+   --  a function, procedure, or entry call.
+
    function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
    --  Applies to Itypes. True if the Itype is attached to a declaration for
    --  the type through its Parent field, which may or not be present in the