par-ch6.adb: Correct obsolete name in comments

2011-08-02  Yannick Moy  <moy@adacore.com>

	* par-ch6.adb: Correct obsolete name in comments
	* restrict.adb, restrict.ads (Check_Formal_Restriction): new function
	which takes two message arguments (existing function takes one), with
	second message used for continuation.
	* sem_ch5.adb (Analyze_Block_Statement): in formal mode, only reject
	block statements that originate from a source block statement, not
	generated block statements
	* sem_ch6.adb (Analyze_Function_Call): rename L into Actuals, for
	symmetry with procedure case
	* sem_ch7.adb (Check_One_Tagged_Type_Or_Extension_At_Most): new
	function to issue an error in formal mode if a package specification
	contains more than one tagged type or type extension.
	* sem_res.adb (Resolve_Actuals): in formal mode, check that actual
	parameters matching formals of tagged types are objects (or ancestor
	type conversions of objects), not general expressions. Issue an error
	on view conversions that are not involving ancestor conversion of an
	extended type.
	(Resolve_Type_Conversion): in formal mode, issue an error on the
	operand of an ancestor type conversion which is not an object
	* sem_util.adb, sem_util.ads (Find_Actual): extend the behavior of the
	procedure so that it works also for actuals of function calls
	(Is_Actual_Tagged_Parameter): new function which determines if its
	argument is an actual parameter of a formal of tagged type in a
	subprogram call
	(Is_SPARK_Object_Reference): new function which determines if the tree
	referenced by its argument represents an object in SPARK

From-SVN: r177125

10 files changed, 237 insertions, 33 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 712f5f7..6507dea 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,32 @@
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* par-ch6.adb: Correct obsolete name in comments
+	* restrict.adb, restrict.ads (Check_Formal_Restriction): new function
+	which takes two message arguments (existing function takes one), with
+	second message used for continuation.
+	* sem_ch5.adb (Analyze_Block_Statement): in formal mode, only reject
+	block statements that originate from a source block statement, not
+	generated block statements
+	* sem_ch6.adb (Analyze_Function_Call): rename L into Actuals, for
+	symmetry with procedure case
+	* sem_ch7.adb (Check_One_Tagged_Type_Or_Extension_At_Most): new
+	function to issue an error in formal mode if a package specification
+	contains more than one tagged type or type extension.
+	* sem_res.adb (Resolve_Actuals): in formal mode, check that actual
+	parameters matching formals of tagged types are objects (or ancestor
+	type conversions of objects), not general expressions. Issue an error
+	on view conversions that are not involving ancestor conversion of an
+	extended type.
+	(Resolve_Type_Conversion): in formal mode, issue an error on the
+	operand of an ancestor type conversion which is not an object
+	* sem_util.adb, sem_util.ads (Find_Actual): extend the behavior of the
+	procedure so that it works also for actuals of function calls
+	(Is_Actual_Tagged_Parameter): new function which determines if its
+	argument is an actual parameter of a formal of tagged type in a
+	subprogram call
+	(Is_SPARK_Object_Reference): new function which determines if the tree
+	referenced by its argument represents an object in SPARK
+
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 
 	* sem_ch3.adb: Minor reformatting
diff --git a/gcc/ada/par-ch6.adb b/gcc/ada/par-ch6.adb
index fae8304..bcb6161 100644
--- a/gcc/ada/par-ch6.adb
+++ b/gcc/ada/par-ch6.adb
@@ -1492,25 +1492,25 @@ package body Ch6 is
    -- 6.4  Function Call --
    ------------------------
 
-   --  Parsed by P_Call_Or_Name (4.1)
+   --  Parsed by P_Name (4.1)
 
    --------------------------------
    -- 6.4  Actual Parameter Part --
    --------------------------------
 
-   --  Parsed by P_Call_Or_Name (4.1)
+   --  Parsed by P_Name (4.1)
 
    --------------------------------
    -- 6.4  Parameter Association --
    --------------------------------
 
-   --  Parsed by P_Call_Or_Name (4.1)
+   --  Parsed by P_Name (4.1)
 
    ------------------------------------
    -- 6.4  Explicit Actual Parameter --
    ------------------------------------
 
-   --  Parsed by P_Call_Or_Name (4.1)
+   --  Parsed by P_Name (4.1)
 
    ---------------------------
    -- 6.5  Return Statement --
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 42746f1..5a9f0b2 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -118,6 +118,18 @@ package body Restrict is
       end if;
    end Check_Formal_Restriction;
 
+   procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
+   begin
+      pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+      then
+         Error_Msg_F ("|~~" & Msg1, N);
+         Error_Msg_F (Msg2, N);
+      end if;
+   end Check_Formal_Restriction;
+
    -----------------------------------------
    -- Check_Implicit_Dynamic_Code_Allowed --
    -----------------------------------------
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads
index c491ca9..c006fd6 100644
--- a/gcc/ada/restrict.ads
+++ b/gcc/ada/restrict.ads
@@ -225,6 +225,10 @@ package Restrict is
    --  "|~~" (error not serious, language prepended). Call has no effect if
    --  not in formal mode, or if N does not come originally from source.
 
+   procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id);
+   --  Same as Check_Formal_Restriction except there is a continuation message
+   --  Msg2 following the initial message Msg1.
+
    procedure Check_Implicit_Dynamic_Code_Allowed (N : Node_Id);
    --  Tests to see if dynamic code generation (dynamically generated
    --  trampolines, in particular) is allowed by the current restrictions
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 0780140..2bf3383 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -807,7 +807,12 @@ package body Sem_Ch5 is
       HSS   : constant Node_Id := Handled_Statement_Sequence (N);
 
    begin
-      Check_Formal_Restriction ("block statement is not allowed", N);
+      --  Only reject block statements that originate from a source block
+      --  statement, in formal mode.
+
+      if Nkind (Original_Node (N)) = N_Block_Statement then
+         Check_Formal_Restriction ("block statement is not allowed", N);
+      end if;
 
       --  If no handled statement sequence is present, things are really messed
       --  up, and we just return immediately (defence against previous errors).
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 140113c..c0b17fe 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -325,9 +325,9 @@ package body Sem_Ch6 is
    ----------------------------
 
    procedure Analyze_Function_Call (N : Node_Id) is
-      P      : constant Node_Id := Name (N);
-      L      : constant List_Id := Parameter_Associations (N);
-      Actual : Node_Id;
+      P       : constant Node_Id := Name (N);
+      Actuals : constant List_Id := Parameter_Associations (N);
+      Actual  : Node_Id;
 
    begin
       Analyze (P);
@@ -353,8 +353,8 @@ package body Sem_Ch6 is
 
       --  Otherwise analyze the parameters
 
-      if Present (L) then
-         Actual := First (L);
+      if Present (Actuals) then
+         Actual := First (Actuals);
          while Present (Actual) loop
             Analyze (Actual);
             Check_Parameterless_Call (Actual);
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index b36c600..1fbaacd 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -43,6 +43,7 @@ with Nmake;    use Nmake;
 with Nlists;   use Nlists;
 with Opt;      use Opt;
 with Output;   use Output;
+with Restrict; use Restrict;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
 with Sem_Cat;  use Sem_Cat;
@@ -873,6 +874,11 @@ package body Sem_Ch7 is
       --  private_with_clauses, and remove them at the end of the nested
       --  package.
 
+      procedure Check_One_Tagged_Type_Or_Extension_At_Most;
+      --  Issue an error in formal mode if a package specification contains
+      --  more than one tagged type or type extension. This is a restriction of
+      --  SPARK.
+
       procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
       --  Clears constant indications (Never_Set_In_Source, Constant_Value, and
       --  Is_True_Constant) on all variables that are entities of Id, and on
@@ -901,6 +907,56 @@ package body Sem_Ch7 is
       --  private part rather than being done in Sem_Ch12.Install_Parent
       --  (which is where the parents' visible declarations are installed).
 
+      ------------------------------------------------
+      -- Check_One_Tagged_Type_Or_Extension_At_Most --
+      ------------------------------------------------
+
+      procedure Check_One_Tagged_Type_Or_Extension_At_Most is
+         Previous : Node_Id;
+
+         procedure Check_Decls (Decls : List_Id);
+         --  Check that either Previous is Empty and Decls does not contain
+         --  more than one tagged type or type extension, or Previous is
+         --  already set and Decls contains no tagged type or type extension.
+
+         -----------------
+         -- Check_Decls --
+         -----------------
+
+         procedure Check_Decls (Decls : List_Id) is
+            Decl : Node_Id;
+         begin
+            Decl := First (Decls);
+            while Present (Decl) loop
+               if Nkind (Decl) = N_Full_Type_Declaration
+                 and then Is_Tagged_Type (Defining_Identifier (Decl))
+               then
+                  if No (Previous) then
+                     Previous := Decl;
+                  else
+                     Error_Msg_Sloc := Sloc (Previous);
+                     Check_Formal_Restriction
+                       ("at most one tagged type or type extension allowed",
+                        "\\ previous declaration#",
+                        Decl);
+                  end if;
+               end if;
+
+               Next (Decl);
+            end loop;
+         end Check_Decls;
+
+      --  Start of processing for Check_One_Tagged_Type_Or_Extension_At_Most
+
+      begin
+         Previous := Empty;
+         Check_Decls (Vis_Decls);
+
+         if Present (Priv_Decls) then
+            Check_Decls (Priv_Decls);
+         end if;
+      end Check_One_Tagged_Type_Or_Extension_At_Most;
+
       ---------------------
       -- Clear_Constants --
       ---------------------
@@ -1383,6 +1439,8 @@ package body Sem_Ch7 is
          Clear_Constants (Id, First_Entity (Id));
          Clear_Constants (Id, First_Private_Entity (Id));
       end if;
+
+      Check_One_Tagged_Type_Or_Extension_At_Most;
    end Analyze_Package_Specification;
 
    --------------------------------------
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index a94ecc2..fa938c1 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3585,29 +3585,70 @@ package body Sem_Res is
             A_Typ := Etype (A);
             F_Typ := Etype (F);
 
-            --  In SPARK or ALFA, the only view conversions are those involving
-            --  ancestor conversion of an extended type.
-
-            if Nkind (A) = N_Type_Conversion
-              and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
+            if Comes_From_Source (Original_Node (N))
+              and then Nkind_In (Original_Node (N),
+                                 N_Function_Call,
+                                 N_Procedure_Call_Statement)
             then
-               declare
-                  Operand     : constant Node_Id   := Expression (A);
-                  Operand_Typ : constant Entity_Id := Etype (Operand);
-                  Target_Typ  : constant Entity_Id := A_Typ;
+               --  In formal mode, check that actual parameters matching
+               --  formals of tagged types are objects (or ancestor type
+               --  conversions of objects), not general expressions.
 
-               begin
-                  if not (Is_Tagged_Type (Target_Typ)
+               if Is_Actual_Tagged_Parameter (A) then
+                  if Is_SPARK_Object_Reference (A) then
+                     null;
+
+                  elsif Nkind (A) = N_Type_Conversion then
+                     declare
+                        Operand     : constant Node_Id   := Expression (A);
+                        Operand_Typ : constant Entity_Id := Etype (Operand);
+                        Target_Typ  : constant Entity_Id := A_Typ;
+
+                     begin
+                        if not Is_SPARK_Object_Reference (Operand) then
+                           Check_Formal_Restriction
+                             ("object required", Operand);
+
+                        --  In formal mode, the only view conversions are those
+                        --  involving ancestor conversion of an extended type.
+
+                        elsif not
+                          (Is_Tagged_Type (Target_Typ)
                            and then not Is_Class_Wide_Type (Target_Typ)
                            and then Is_Tagged_Type (Operand_Typ)
                            and then not Is_Class_Wide_Type (Operand_Typ)
                            and then Is_Ancestor (Target_Typ, Operand_Typ))
-                  then
-                     Check_Formal_Restriction
-                       ("ancestor conversion is the only permitted view "
-                        & "conversion", A);
+                        then
+                           if Ekind_In
+                             (F, E_Out_Parameter, E_In_Out_Parameter)
+                           then
+                              Check_Formal_Restriction
+                                ("ancestor conversion is the only permitted "
+                                 & "view conversion", A);
+                           else
+                              Check_Formal_Restriction
+                                ("ancestor conversion required", A);
+                           end if;
+
+                        else
+                           null;
+                        end if;
+                     end;
+
+                  else
+                     Check_Formal_Restriction ("object required", A);
                   end if;
-               end;
+
+               --  In formal mode, the only view conversions are those
+               --  involving ancestor conversion of an extended type.
+
+               elsif Nkind (A) = N_Type_Conversion
+                 and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
+               then
+                  Check_Formal_Restriction
+                    ("ancestor conversion is the only permitted view "
+                     & "conversion", A);
+               end if;
             end if;
 
             --  Save actual for subsequent check on order dependence, and
@@ -9056,6 +9097,19 @@ package body Sem_Res is
            ("array types should have matching static bounds", N);
       end if;
 
+      --  In formal mode, the operand of an ancestor type conversion must be an
+      --  object (not an expression).
+
+      if Is_Tagged_Type (Target_Typ)
+        and then not Is_Class_Wide_Type (Target_Typ)
+        and then Is_Tagged_Type (Operand_Typ)
+        and then not Is_Class_Wide_Type (Operand_Typ)
+        and then Is_Ancestor (Target_Typ, Operand_Typ)
+        and then not Is_SPARK_Object_Reference (Operand)
+      then
+         Check_Formal_Restriction ("object required", Operand);
+      end if;
+
       --  Note: we do the Eval_Type_Conversion call before applying the
       --  required checks for a subtype conversion. This is important, since
       --  both are prepared under certain circumstances to change the type
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 14824ca..15e978f 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -3359,7 +3359,7 @@ package body Sem_Util is
       then
          Call := Parent (Parnt);
 
-      elsif Nkind (Parnt) = N_Procedure_Call_Statement then
+      elsif Nkind_In (Parnt, N_Procedure_Call_Statement, N_Function_Call) then
          Call := Parnt;
 
       else
@@ -5883,6 +5883,18 @@ package body Sem_Util is
       end case;
    end Is_Actual_Parameter;
 
+   --------------------------------
+   -- Is_Actual_Tagged_Parameter --
+   --------------------------------
+
+   function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean is
+      Formal : Entity_Id;
+      Call   : Node_Id;
+   begin
+      Find_Actual (N, Formal, Call);
+      return Present (Formal) and then Is_Tagged_Type (Etype (Formal));
+   end Is_Actual_Tagged_Parameter;
+
    ---------------------
    -- Is_Aliased_View --
    ---------------------
@@ -6833,6 +6845,29 @@ package body Sem_Util is
       end if;
    end Is_Object_Reference;
 
+   -------------------------------
+   -- Is_SPARK_Object_Reference --
+   -------------------------------
+
+   function Is_SPARK_Object_Reference (N : Node_Id) return Boolean is
+   begin
+      if Is_Entity_Name (N) then
+         return Present (Entity (N))
+           and then
+             (Ekind_In (Entity (N), E_Constant, E_Variable)
+              or else Ekind (Entity (N)) in Formal_Kind);
+
+      else
+         case Nkind (N) is
+            when N_Selected_Component =>
+               return Is_SPARK_Object_Reference (Prefix (N));
+
+            when others =>
+               return False;
+         end case;
+      end if;
+   end Is_SPARK_Object_Reference;
+
    -----------------------------------
    -- Is_OK_Variable_For_Out_Formal --
    -----------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 6410db4..c908d88 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -353,12 +353,12 @@ package Sem_Util is
      (N      : Node_Id;
       Formal : out Entity_Id;
       Call   : out Node_Id);
-   --  Determines if the node N is an actual parameter of a procedure call. If
-   --  so, then Formal points to the entity for the formal (whose Ekind is one
-   --  of E_In_Parameter, E_Out_Parameter, E_In_Out_Parameter) and Call is set
-   --  to the node for the corresponding call. If the node N is not an actual
-   --  parameter, or is an actual parameter of a function call, then Formal and
-   --  Call are set to Empty.
+   --  Determines if the node N is an actual parameter of a function of a
+   --  procedure call. If so, then Formal points to the entity for the formal
+   --  (whose Ekind is one of E_In_Parameter, E_Out_Parameter,
+   --  E_In_Out_Parameter) and Call is set to the node for the corresponding
+   --  call. If the node N is not an actual parameter then Formal and Call are
+   --  set to Empty.
 
    function Find_Corresponding_Discriminant
      (Id   : Node_Id;
@@ -677,6 +677,10 @@ package Sem_Util is
    function Is_Actual_Parameter (N : Node_Id) return Boolean;
    --  Determines if N is an actual parameter in a subprogram call
 
+   function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean;
+   --  Determines if N is an actual parameter of a formal of tagged type in a
+   --  subprogram call.
+
    function Is_Aliased_View (Obj : Node_Id) return Boolean;
    --  Determine if Obj is an aliased view, i.e. the name of an object to which
    --  'Access or 'Unchecked_Access can apply.
@@ -763,6 +767,9 @@ package Sem_Util is
    --  Determines if the tree referenced by N represents an object. Both
    --  variable and constant objects return True (compare Is_Variable).
 
+   function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
+   --  Determines if the tree referenced by N represents an object in SPARK.
+
    function Is_OK_Variable_For_Out_Formal (AV : Node_Id) return Boolean;
    --  Used to test if AV is an acceptable formal for an OUT or IN OUT formal.
    --  Note that the Is_Variable function is not quite the right test because