[multiple changes]

2011-08-02  Robert Dewar  <dewar@adacore.com>

	* exp_util.adb, par-ch10.adb, par-ch6.adb, sem.adb, sem_ch6.adb,
	sem_ch6.ads, sinfo.adb, sinfo.ads, sprint.adb: Change parameterized
	expression to expression function.

2011-08-02  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch4.adb: transform simple Ada2012 membership into equality only
	if types are compatible.

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

	* sem_res.adb (Matching_Static_Array_Bounds): new function which
	returns True if its argument array types have same dimension and same
	static bounds at each index.
	(Resolve_Actuals): issue an error in formal mode on actuals passed as
	OUT or IN OUT paramaters which are not view conversions in SPARK.
	(Resolve_Arithmetic_Op): issue an error in formal mode on
	multiplication or division with operands of fixed point types which are
	not qualified or explicitly converted.
	(Resolve_Comparison_Op): issue an error in formal mode on comparisons of
	Boolean or array type (except String) operands.
	(Resolve_Equality_Op): issue an error in formal mode on equality
	operators for array types other than String with non-matching static
	bounds.
	(Resolve_Logical_Op): issue an error in formal mode on logical operators
	for array types with non-matching static bounds. Factorize the code in
	Matching_Static_Array_Bounds.
	(Resolve_Qualified_Expression): issue an error in formal mode on
	qualified expressions for array types with non-matching static bounds.
	(Resolve_Type_Conversion): issue an error in formal mode on type
	conversion for array types with non-matching static bounds

From-SVN: r177089

12 files changed, 461 insertions, 295 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e9e0cce..b7a2c5e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,39 @@
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 
+	* exp_util.adb, par-ch10.adb, par-ch6.adb, sem.adb, sem_ch6.adb,
+	sem_ch6.ads, sinfo.adb, sinfo.ads, sprint.adb: Change parameterized
+	expression to expression function.
+
+2011-08-02  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch4.adb: transform simple Ada2012 membership into equality only
+	if types are compatible.
+
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Matching_Static_Array_Bounds): new function which
+	returns True if its argument array types have same dimension and same
+	static bounds at each index.
+	(Resolve_Actuals): issue an error in formal mode on actuals passed as
+	OUT or IN OUT paramaters which are not view conversions in SPARK.
+	(Resolve_Arithmetic_Op): issue an error in formal mode on
+	multiplication or division with operands of fixed point types which are
+	not qualified or explicitly converted.
+	(Resolve_Comparison_Op): issue an error in formal mode on comparisons of
+	Boolean or array type (except String) operands.
+	(Resolve_Equality_Op): issue an error in formal mode on equality
+	operators for array types other than String with non-matching static
+	bounds.
+	(Resolve_Logical_Op): issue an error in formal mode on logical operators
+	for array types with non-matching static bounds. Factorize the code in
+	Matching_Static_Array_Bounds.
+	(Resolve_Qualified_Expression): issue an error in formal mode on
+	qualified expressions for array types with non-matching static bounds.
+	(Resolve_Type_Conversion): issue an error in formal mode on type
+	conversion for array types with non-matching static bounds
+
+2011-08-02  Robert Dewar  <dewar@adacore.com>
+
 	* par-ch10.adb: Minor code reorganization (use Nkind_In).
 
 2011-08-02  Ed Schonberg  <schonberg@adacore.com>
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 74e916f..03e41c9 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -2592,6 +2592,7 @@ package body Exp_Util is
                N_Entry_Body                             |
                N_Exception_Declaration                  |
                N_Exception_Renaming_Declaration         |
+               N_Expression_Function                    |
                N_Formal_Abstract_Subprogram_Declaration |
                N_Formal_Concrete_Subprogram_Declaration |
                N_Formal_Object_Declaration              |
@@ -2613,7 +2614,6 @@ package body Exp_Util is
                N_Package_Declaration                    |
                N_Package_Instantiation                  |
                N_Package_Renaming_Declaration           |
-               N_Parameterized_Expression               |
                N_Private_Extension_Declaration          |
                N_Private_Type_Declaration               |
                N_Procedure_Instantiation                |
diff --git a/gcc/ada/par-ch10.adb b/gcc/ada/par-ch10.adb
index 6958209..08553dd 100644
--- a/gcc/ada/par-ch10.adb
+++ b/gcc/ada/par-ch10.adb
@@ -562,9 +562,9 @@ package body Ch10 is
          then
             Name_Node := Defining_Unit_Name (Unit_Node);
 
-         elsif Nkind (Unit_Node) = N_Parameterized_Expression then
+         elsif Nkind (Unit_Node) = N_Expression_Function then
             Error_Msg_SP
-              ("parameterized expression cannot be used as compilation unit");
+              ("expression function cannot be used as compilation unit");
             return Comp_Unit_Node;
 
          --  Anything else is a serious error, abandon scan
diff --git a/gcc/ada/par-ch6.adb b/gcc/ada/par-ch6.adb
index 6fe1dea..fae8304 100644
--- a/gcc/ada/par-ch6.adb
+++ b/gcc/ada/par-ch6.adb
@@ -82,7 +82,7 @@ package body Ch6 is
 
    --  This routine scans out a subprogram declaration, subprogram body,
    --  subprogram renaming declaration or subprogram generic instantiation.
-   --  It also handles the new Ada 2012 parameterized expression form
+   --  It also handles the new Ada 2012 expression function form
 
    --  SUBPROGRAM_DECLARATION ::=
    --    SUBPROGRAM_SPECIFICATION
@@ -126,7 +126,7 @@ package body Ch6 is
    --  is classified as a basic declarative item, but it is parsed here, with
    --  other subprogram constructs.
 
-   --  PARAMETERIZED_EXPRESSION ::=
+   --  EXPRESSION_FUNCTION ::=
    --    FUNCTION SPECIFICATION IS (EXPRESSION);
 
    --  The value in Pf_Flags indicates which of these possible declarations
@@ -137,7 +137,7 @@ package body Ch6 is
    --    Pf_Flags.Pbod                 Set if proper body OK
    --    Pf_Flags.Rnam                 Set if renaming declaration OK
    --    Pf_Flags.Stub                 Set if body stub OK
-   --    Pf_Flags.Pexp                 Set if parameterized expression OK
+   --    Pf_Flags.Pexp                 Set if expression function OK
 
    --  If an inappropriate form is encountered, it is scanned out but an
    --  error message indicating that it is appearing in an inappropriate
@@ -598,7 +598,7 @@ package body Ch6 is
          end if;
       end if;
 
-      --  Processing for stub or subprogram body or parameterized expression
+      --  Processing for stub or subprogram body or expression function
 
       <<Subprogram_Body>>
 
@@ -623,21 +623,21 @@ package body Ch6 is
             TF_Semicolon;
             return Stub_Node;
 
-         --  Subprogram body or parameterized expression case
+         --  Subprogram body or expression function case
 
          else
-            Scan_Body_Or_Parameterized_Expression : declare
+            Scan_Body_Or_Expression_Function : declare
 
-               function Likely_Parameterized_Expression return Boolean;
-               --  Returns True if we have a probably case of a parameterized
-               --  expression omitting the parentheses, if so, returns True
+               function Likely_Expression_Function return Boolean;
+               --  Returns True if we have a probable case of an expression
+               --  function omitting the parentheses, if so, returns True
                --  and emits an appropriate error message, else returns False.
 
-               -------------------------------------
-               -- Likely_Parameterized_Expression --
-               -------------------------------------
+               --------------------------------
+               -- Likely_Expression_Function --
+               --------------------------------
 
-               function Likely_Parameterized_Expression return Boolean is
+               function Likely_Expression_Function return Boolean is
                begin
                   --  If currently pointing to BEGIN or a declaration keyword
                   --  or a pragma, then we definitely have a subprogram body.
@@ -650,15 +650,15 @@ package body Ch6 is
                      return False;
 
                   --  Test for tokens which could only start an expression and
-                  --  thus signal the case of a parameterized expression.
+                  --  thus signal the case of a expression function.
 
-                  elsif Token in Token_Class_Literal
+                  elsif Token     in Token_Class_Literal
                     or else Token in Token_Class_Unary_Addop
-                    or else Token = Tok_Left_Paren
-                    or else Token = Tok_Abs
-                    or else Token = Tok_Null
-                    or else Token = Tok_New
-                    or else Token = Tok_Not
+                    or else Token =  Tok_Left_Paren
+                    or else Token =  Tok_Abs
+                    or else Token =  Tok_Null
+                    or else Token =  Tok_New
+                    or else Token =  Tok_Not
                   then
                      null;
 
@@ -680,12 +680,13 @@ package body Ch6 is
                      --  Otherwise we have to scan ahead. If the identifier is
                      --  followed by a colon or a comma, it is a declaration
                      --  and hence we have a subprogram body. Otherwise assume
-                     --  a parameterized expression.
+                     --  a expression function.
 
                      else
                         declare
                            Scan_State : Saved_Scan_State;
                            Tok        : Token_Type;
+
                         begin
                            Save_Scan_State (Scan_State);
                            Scan; -- past identifier
@@ -699,43 +700,41 @@ package body Ch6 is
                      end if;
                   end if;
 
-                  --  Fall through if we have a likely parameterized expression
+                  --  Fall through if we have a likely expression function
 
                   Error_Msg_SC
-                    ("parameterized expression must be "
-                     & "enclosed in parentheses");
+                    ("expression function must be enclosed in parentheses");
                   return True;
-               end Likely_Parameterized_Expression;
+               end Likely_Expression_Function;
 
-            --  Start of processing for Scan_Body_Or_Parameterized_Expression
+            --  Start of processing for Scan_Body_Or_Expression_Function
 
             begin
-               --  Parameterized_Expression case
+               --  Expression_Function case
 
                if Token = Tok_Left_Paren
-                 or else Likely_Parameterized_Expression
+                 or else Likely_Expression_Function
                then
-                  --  Check parameterized expression allowed here
+                  --  Check expression function allowed here
 
                   if not Pf_Flags.Pexp then
-                     Error_Msg_SC
-                       ("parameterized expression not allowed here!");
+                     Error_Msg_SC ("expression function not allowed here!");
                   end if;
 
                   --  Check we are in Ada 2012 mode
 
                   if Ada_Version < Ada_2012 then
                      Error_Msg_SC
-                       ("parameterized expression is an Ada 2012 feature!");
+                       ("expression function is an Ada 2012 feature!");
                      Error_Msg_SC
                        ("\unit must be compiled with -gnat2012 switch!");
                   end if;
 
-                  --  Parse out expression and build parameterized expression
+                  --  Parse out expression and build expression function
 
                   Body_Node :=
                     New_Node
-                      (N_Parameterized_Expression, Sloc (Specification_Node));
+                      (N_Expression_Function, Sloc (Specification_Node));
                   Set_Specification (Body_Node, Specification_Node);
                   Set_Expression (Body_Node, P_Expression);
                   T_Semicolon;
@@ -775,7 +774,7 @@ package body Ch6 is
                end if;
 
                return Body_Node;
-            end Scan_Body_Or_Parameterized_Expression;
+            end Scan_Body_Or_Expression_Function;
          end if;
 
       --  Processing for subprogram declaration
diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb
index 0061d6b..5b43499 100644
--- a/gcc/ada/sem.adb
+++ b/gcc/ada/sem.adb
@@ -223,6 +223,9 @@ package body Sem is
          when N_Explicit_Dereference =>
             Analyze_Explicit_Dereference (N);
 
+         when N_Expression_Function =>
+            Analyze_Expression_Function (N);
+
          when N_Expression_With_Actions =>
             Analyze_Expression_With_Actions (N);
 
@@ -439,9 +442,6 @@ package body Sem is
          when N_Parameter_Association =>
             Analyze_Parameter_Association (N);
 
-         when N_Parameterized_Expression =>
-            Analyze_Parameterized_Expression (N);
-
          when N_Pragma =>
             Analyze_Pragma (N);
 
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index b5a8e18..8b737ab 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -2475,7 +2475,8 @@ package body Sem_Ch4 is
          end if;
 
       --  If not a range, it can be a subtype mark, or else it is a degenerate
-      --  membership test with a singleton value, i.e. a test for equality.
+      --  membership test with a singleton value, i.e. a test for equality,
+      --  if the types are compatible.
 
       else
          Analyze (R);
@@ -2485,7 +2486,9 @@ package body Sem_Ch4 is
             Find_Type (R);
             Check_Fully_Declared (Entity (R), R);
 
-         elsif Ada_Version >= Ada_2012 then
+         elsif Ada_Version >= Ada_2012
+           and then Has_Compatible_Type (R, Etype (L))
+         then
             if Nkind (N) = N_In then
                Rewrite (N,
                  Make_Op_Eq (Loc,
@@ -2502,8 +2505,8 @@ package body Sem_Ch4 is
             return;
 
          else
-            --  In previous version of the language this is an error that will
-            --  be diagnosed below.
+            --  In all versions of the language, if we reach this point there
+            --  is a previous error that will be diagnosed below.
 
             Find_Type (R);
          end if;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 72a1529..af20ffa 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -215,141 +215,6 @@ package body Sem_Ch6 is
    --  setting the proper validity status for this entity, which depends on
    --  the kind of parameter and the validity checking mode.
 
-   ------------------------------
-   -- Analyze_Return_Statement --
-   ------------------------------
-
-   procedure Analyze_Return_Statement (N : Node_Id) is
-
-      pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
-                                  N_Extended_Return_Statement));
-
-      Returns_Object : constant Boolean :=
-                         Nkind (N) = N_Extended_Return_Statement
-                           or else
-                            (Nkind (N) = N_Simple_Return_Statement
-                              and then Present (Expression (N)));
-      --  True if we're returning something; that is, "return <expression>;"
-      --  or "return Result : T [:= ...]". False for "return;". Used for error
-      --  checking: If Returns_Object is True, N should apply to a function
-      --  body; otherwise N should apply to a procedure body, entry body,
-      --  accept statement, or extended return statement.
-
-      function Find_What_It_Applies_To return Entity_Id;
-      --  Find the entity representing the innermost enclosing body, accept
-      --  statement, or extended return statement. If the result is a callable
-      --  construct or extended return statement, then this will be the value
-      --  of the Return_Applies_To attribute. Otherwise, the program is
-      --  illegal. See RM-6.5(4/2).
-
-      -----------------------------
-      -- Find_What_It_Applies_To --
-      -----------------------------
-
-      function Find_What_It_Applies_To return Entity_Id is
-         Result : Entity_Id := Empty;
-
-      begin
-         --  Loop outward through the Scope_Stack, skipping blocks and loops
-
-         for J in reverse 0 .. Scope_Stack.Last loop
-            Result := Scope_Stack.Table (J).Entity;
-            exit when Ekind (Result) /= E_Block and then
-                      Ekind (Result) /= E_Loop;
-         end loop;
-
-         pragma Assert (Present (Result));
-         return Result;
-      end Find_What_It_Applies_To;
-
-      --  Local declarations
-
-      Scope_Id   : constant Entity_Id   := Find_What_It_Applies_To;
-      Kind       : constant Entity_Kind := Ekind (Scope_Id);
-      Loc        : constant Source_Ptr  := Sloc (N);
-      Stm_Entity : constant Entity_Id   :=
-                     New_Internal_Entity
-                       (E_Return_Statement, Current_Scope, Loc, 'R');
-
-   --  Start of processing for Analyze_Return_Statement
-
-   begin
-      Set_Return_Statement_Entity (N, Stm_Entity);
-
-      Set_Etype (Stm_Entity, Standard_Void_Type);
-      Set_Return_Applies_To (Stm_Entity, Scope_Id);
-
-      --  Place Return entity on scope stack, to simplify enforcement of 6.5
-      --  (4/2): an inner return statement will apply to this extended return.
-
-      if Nkind (N) = N_Extended_Return_Statement then
-         Push_Scope (Stm_Entity);
-      end if;
-
-      --  Check that pragma No_Return is obeyed. Don't complain about the
-      --  implicitly-generated return that is placed at the end.
-
-      if No_Return (Scope_Id) and then Comes_From_Source (N) then
-         Error_Msg_N ("RETURN statement not allowed (No_Return)", N);
-      end if;
-
-      --  Warn on any unassigned OUT parameters if in procedure
-
-      if Ekind (Scope_Id) = E_Procedure then
-         Warn_On_Unassigned_Out_Parameter (N, Scope_Id);
-      end if;
-
-      --  Check that functions return objects, and other things do not
-
-      if Kind = E_Function or else Kind = E_Generic_Function then
-         if not Returns_Object then
-            Error_Msg_N ("missing expression in return from function", N);
-         end if;
-
-      elsif Kind = E_Procedure or else Kind = E_Generic_Procedure then
-         if Returns_Object then
-            Error_Msg_N ("procedure cannot return value (use function)", N);
-         end if;
-
-      elsif Kind = E_Entry or else Kind = E_Entry_Family then
-         if Returns_Object then
-            if Is_Protected_Type (Scope (Scope_Id)) then
-               Error_Msg_N ("entry body cannot return value", N);
-            else
-               Error_Msg_N ("accept statement cannot return value", N);
-            end if;
-         end if;
-
-      elsif Kind = E_Return_Statement then
-
-         --  We are nested within another return statement, which must be an
-         --  extended_return_statement.
-
-         if Returns_Object then
-            Error_Msg_N
-              ("extended_return_statement cannot return value; " &
-               "use `""RETURN;""`", N);
-         end if;
-
-      else
-         Error_Msg_N ("illegal context for return statement", N);
-      end if;
-
-      if Ekind_In (Kind, E_Function, E_Generic_Function) then
-         Analyze_Function_Return (N);
-
-      elsif Ekind_In (Kind, E_Procedure, E_Generic_Procedure) then
-         Set_Return_Present (Scope_Id);
-      end if;
-
-      if Nkind (N) = N_Extended_Return_Statement then
-         End_Scope;
-      end if;
-
-      Kill_Current_Values (Last_Assignment_Only => True);
-      Check_Unreachable_Code (N);
-   end Analyze_Return_Statement;
-
    ---------------------------------------------
    -- Analyze_Abstract_Subprogram_Declaration --
    ---------------------------------------------
@@ -398,6 +263,55 @@ package body Sem_Ch6 is
       Analyze_Aspect_Specifications (N, Designator, Aspect_Specifications (N));
    end Analyze_Abstract_Subprogram_Declaration;
 
+   ---------------------------------
+   -- Analyze_Expression_Function --
+   ---------------------------------
+
+   procedure Analyze_Expression_Function (N : Node_Id) is
+      Loc      : constant Source_Ptr := Sloc (N);
+      LocX     : constant Source_Ptr := Sloc (Expression (N));
+      Def_Id   : constant Entity_Id  := Defining_Entity (Specification (N));
+      New_Body : Node_Id;
+
+      Prev : constant Entity_Id := Current_Entity_In_Scope (Def_Id);
+      --  If the expression is a completion, Prev is the entity whose
+      --  declaration is completed.
+
+   begin
+      --  This is one of the occasions on which we transform the tree during
+      --  semantic analysis. Transform the expression function into an
+      --  equivalent subprogram body, and then analyze that.
+
+      New_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification              => Specification (N),
+          Declarations               => Empty_List,
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (LocX,
+              Statements => New_List (
+                Make_Simple_Return_Statement (LocX,
+                  Expression => Expression (N)))));
+
+      if Present (Prev)
+        and then Ekind (Prev) = E_Generic_Function
+      then
+         --  If the expression completes a generic subprogram, we must create a
+         --  separate node for the body, because at instantiation the original
+         --  node of the generic copy must be a generic subprogram body, and
+         --  cannot be a expression function. Otherwise we just rewrite the
+         --  expression with the non-generic body.
+
+         Insert_After (N, New_Body);
+         Rewrite (N, Make_Null_Statement (Loc));
+         Analyze (N);
+         Analyze (New_Body);
+
+      else
+         Rewrite (N, New_Body);
+         Analyze (N);
+      end if;
+   end Analyze_Expression_Function;
+
    ----------------------------------------
    -- Analyze_Extended_Return_Statement  --
    ----------------------------------------
@@ -1095,55 +1009,6 @@ package body Sem_Ch6 is
       Analyze (Explicit_Actual_Parameter (N));
    end Analyze_Parameter_Association;
 
-   --------------------------------------
-   -- Analyze_Parameterized_Expression --
-   --------------------------------------
-
-   procedure Analyze_Parameterized_Expression (N : Node_Id) is
-      Loc      : constant Source_Ptr := Sloc (N);
-      LocX     : constant Source_Ptr := Sloc (Expression (N));
-      Def_Id   : constant Entity_Id  := Defining_Entity (Specification (N));
-      New_Body : Node_Id;
-
-      Prev : constant Entity_Id := Current_Entity_In_Scope (Def_Id);
-      --  If the expression is a completion, Prev is the entity whose
-      --  declaration is completed.
-
-   begin
-      --  This is one of the occasions on which we transform the tree during
-      --  semantic analysis. Transform the parameterized expression into an
-      --  equivalent subprogram body, and then analyze that.
-
-      New_Body :=
-        Make_Subprogram_Body (Loc,
-          Specification              => Specification (N),
-          Declarations               => Empty_List,
-          Handled_Statement_Sequence =>
-            Make_Handled_Sequence_Of_Statements (LocX,
-              Statements => New_List (
-                Make_Simple_Return_Statement (LocX,
-                  Expression => Expression (N)))));
-
-      if Present (Prev)
-        and then Ekind (Prev) = E_Generic_Function
-      then
-         --  If the expression completes a generic subprogram, we must create
-         --  a separate node for the body, because at instantiation the
-         --  original node of the generic copy must be a generic subprogram
-         --  body, and cannot be a parameterized expression. Otherwise we
-         --  just rewrite the expression with the non-generic body.
-
-         Insert_After (N, New_Body);
-         Rewrite (N, Make_Null_Statement (Loc));
-         Analyze (N);
-         Analyze (New_Body);
-
-      else
-         Rewrite (N, New_Body);
-         Analyze (N);
-      end if;
-   end Analyze_Parameterized_Expression;
-
    ----------------------------
    -- Analyze_Procedure_Call --
    ----------------------------
@@ -1372,6 +1237,141 @@ package body Sem_Ch6 is
       end if;
    end Analyze_Procedure_Call;
 
+   ------------------------------
+   -- Analyze_Return_Statement --
+   ------------------------------
+
+   procedure Analyze_Return_Statement (N : Node_Id) is
+
+      pragma Assert (Nkind_In (N, N_Simple_Return_Statement,
+                                  N_Extended_Return_Statement));
+
+      Returns_Object : constant Boolean :=
+                         Nkind (N) = N_Extended_Return_Statement
+                           or else
+                            (Nkind (N) = N_Simple_Return_Statement
+                              and then Present (Expression (N)));
+      --  True if we're returning something; that is, "return <expression>;"
+      --  or "return Result : T [:= ...]". False for "return;". Used for error
+      --  checking: If Returns_Object is True, N should apply to a function
+      --  body; otherwise N should apply to a procedure body, entry body,
+      --  accept statement, or extended return statement.
+
+      function Find_What_It_Applies_To return Entity_Id;
+      --  Find the entity representing the innermost enclosing body, accept
+      --  statement, or extended return statement. If the result is a callable
+      --  construct or extended return statement, then this will be the value
+      --  of the Return_Applies_To attribute. Otherwise, the program is
+      --  illegal. See RM-6.5(4/2).
+
+      -----------------------------
+      -- Find_What_It_Applies_To --
+      -----------------------------
+
+      function Find_What_It_Applies_To return Entity_Id is
+         Result : Entity_Id := Empty;
+
+      begin
+         --  Loop outward through the Scope_Stack, skipping blocks and loops
+
+         for J in reverse 0 .. Scope_Stack.Last loop
+            Result := Scope_Stack.Table (J).Entity;
+            exit when Ekind (Result) /= E_Block and then
+                      Ekind (Result) /= E_Loop;
+         end loop;
+
+         pragma Assert (Present (Result));
+         return Result;
+      end Find_What_It_Applies_To;
+
+      --  Local declarations
+
+      Scope_Id   : constant Entity_Id   := Find_What_It_Applies_To;
+      Kind       : constant Entity_Kind := Ekind (Scope_Id);
+      Loc        : constant Source_Ptr  := Sloc (N);
+      Stm_Entity : constant Entity_Id   :=
+                     New_Internal_Entity
+                       (E_Return_Statement, Current_Scope, Loc, 'R');
+
+   --  Start of processing for Analyze_Return_Statement
+
+   begin
+      Set_Return_Statement_Entity (N, Stm_Entity);
+
+      Set_Etype (Stm_Entity, Standard_Void_Type);
+      Set_Return_Applies_To (Stm_Entity, Scope_Id);
+
+      --  Place Return entity on scope stack, to simplify enforcement of 6.5
+      --  (4/2): an inner return statement will apply to this extended return.
+
+      if Nkind (N) = N_Extended_Return_Statement then
+         Push_Scope (Stm_Entity);
+      end if;
+
+      --  Check that pragma No_Return is obeyed. Don't complain about the
+      --  implicitly-generated return that is placed at the end.
+
+      if No_Return (Scope_Id) and then Comes_From_Source (N) then
+         Error_Msg_N ("RETURN statement not allowed (No_Return)", N);
+      end if;
+
+      --  Warn on any unassigned OUT parameters if in procedure
+
+      if Ekind (Scope_Id) = E_Procedure then
+         Warn_On_Unassigned_Out_Parameter (N, Scope_Id);
+      end if;
+
+      --  Check that functions return objects, and other things do not
+
+      if Kind = E_Function or else Kind = E_Generic_Function then
+         if not Returns_Object then
+            Error_Msg_N ("missing expression in return from function", N);
+         end if;
+
+      elsif Kind = E_Procedure or else Kind = E_Generic_Procedure then
+         if Returns_Object then
+            Error_Msg_N ("procedure cannot return value (use function)", N);
+         end if;
+
+      elsif Kind = E_Entry or else Kind = E_Entry_Family then
+         if Returns_Object then
+            if Is_Protected_Type (Scope (Scope_Id)) then
+               Error_Msg_N ("entry body cannot return value", N);
+            else
+               Error_Msg_N ("accept statement cannot return value", N);
+            end if;
+         end if;
+
+      elsif Kind = E_Return_Statement then
+
+         --  We are nested within another return statement, which must be an
+         --  extended_return_statement.
+
+         if Returns_Object then
+            Error_Msg_N
+              ("extended_return_statement cannot return value; " &
+               "use `""RETURN;""`", N);
+         end if;
+
+      else
+         Error_Msg_N ("illegal context for return statement", N);
+      end if;
+
+      if Ekind_In (Kind, E_Function, E_Generic_Function) then
+         Analyze_Function_Return (N);
+
+      elsif Ekind_In (Kind, E_Procedure, E_Generic_Procedure) then
+         Set_Return_Present (Scope_Id);
+      end if;
+
+      if Nkind (N) = N_Extended_Return_Statement then
+         End_Scope;
+      end if;
+
+      Kill_Current_Values (Last_Assignment_Only => True);
+      Check_Unreachable_Code (N);
+   end Analyze_Return_Statement;
+
    -------------------------------------
    -- Analyze_Simple_Return_Statement --
    -------------------------------------
@@ -2449,9 +2449,9 @@ package body Sem_Ch6 is
 
            and then not In_Instance
 
-           --  No warnings for parameterized expressions
+           --  No warnings for expression functions
 
-           and then Nkind (Original_Node (N)) /= N_Parameterized_Expression
+           and then Nkind (Original_Node (N)) /= N_Expression_Function
          then
             Style.Body_With_No_Spec (N);
          end if;
diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads
index 90fd520..96d967b 100644
--- a/gcc/ada/sem_ch6.ads
+++ b/gcc/ada/sem_ch6.ads
@@ -35,11 +35,11 @@ package Sem_Ch6 is
    --  type is stronger than the ones preceding it.
 
    procedure Analyze_Abstract_Subprogram_Declaration (N : Node_Id);
+   procedure Analyze_Expression_Function             (N : Node_Id);
    procedure Analyze_Extended_Return_Statement       (N : Node_Id);
    procedure Analyze_Function_Call                   (N : Node_Id);
    procedure Analyze_Operator_Symbol                 (N : Node_Id);
    procedure Analyze_Parameter_Association           (N : Node_Id);
-   procedure Analyze_Parameterized_Expression        (N : Node_Id);
    procedure Analyze_Procedure_Call                  (N : Node_Id);
    procedure Analyze_Simple_Return_Statement         (N : Node_Id);
    procedure Analyze_Subprogram_Declaration          (N : Node_Id);
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 319b2ff..495b260 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -92,6 +92,12 @@ package body Sem_Res is
 
    --  Note that Resolve_Attribute is separated off in Sem_Attr
 
+   function Matching_Static_Array_Bounds
+     (L_Typ : Node_Id;
+      R_Typ : Node_Id) return Boolean;
+   --  L_Typ and R_Typ are two array types. Returns True when they have the
+   --  same dimension, and, for each index position, the same static bounds.
+
    function Bad_Unordered_Enumeration_Reference
      (N : Node_Id;
       T : Entity_Id) return Boolean;
@@ -1571,6 +1577,65 @@ package body Sem_Res is
       end if;
    end Make_Call_Into_Operator;
 
+   ----------------------------------
+   -- Matching_Static_Array_Bounds --
+   ----------------------------------
+
+   function Matching_Static_Array_Bounds
+     (L_Typ : Node_Id;
+      R_Typ : Node_Id) return Boolean
+   is
+      L_Ndims : constant Nat := Number_Dimensions (L_Typ);
+      R_Ndims : constant Nat := Number_Dimensions (R_Typ);
+
+      L_Index : Node_Id;
+      R_Index : Node_Id;
+      L_Low   : Node_Id;
+      L_High  : Node_Id;
+      R_Low   : Node_Id;
+      R_High  : Node_Id;
+
+   begin
+      if L_Ndims /= R_Ndims then
+         return False;
+      end if;
+
+      --  Unconstrained types do not have static bounds
+
+      if not Is_Constrained (L_Typ) or else not Is_Constrained (R_Typ) then
+         return False;
+      end if;
+
+      L_Index := First_Index (L_Typ);
+      R_Index := First_Index (R_Typ);
+
+      for Indx in 1 .. L_Ndims loop
+         Get_Index_Bounds (L_Index, L_Low, L_High);
+         Get_Index_Bounds (R_Index, R_Low, R_High);
+
+         if True
+           and then Is_Static_Expression (L_Low)
+           and then Is_Static_Expression (L_High)
+           and then Is_Static_Expression (R_Low)
+           and then Is_Static_Expression (R_High)
+           and then Expr_Value (L_Low)  = Expr_Value (R_Low)
+           and then Expr_Value (L_High) = Expr_Value (R_High)
+         then
+            --  Matching so far, continue with next index
+
+            null;
+
+         else
+            return False;
+         end if;
+
+         Next (L_Index);
+         Next (R_Index);
+      end loop;
+
+      return True;
+   end Matching_Static_Array_Bounds;
+
    -------------------
    -- Operator_Kind --
    -------------------
@@ -1582,6 +1647,8 @@ package body Sem_Res is
       Kind : Node_Kind;
 
    begin
+      --  Use CASE statement or array???
+
       if Is_Binary then
          if    Op_Name =  Name_Op_And      then
             Kind := N_Op_And;
@@ -3555,6 +3622,31 @@ 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 Formal_Verification_Mode
+              and then Comes_From_Source (Original_Node (A))
+              and then Nkind (A) = N_Type_Conversion
+              and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
+            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_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
+                     Error_Msg_F ("|~~ancestor conversion is the only "
+                                  & "view conversion", A);
+                  end if;
+               end;
+            end if;
+
             --  Save actual for subsequent check on order dependence, and
             --  indicate whether actual is modifiable. For AI05-0144-2.
 
@@ -4795,6 +4887,21 @@ package body Sem_Res is
       Generate_Operator_Reference (N, Typ);
       Eval_Arithmetic_Op (N);
 
+      --  In SPARK and ALFA, a multiplication or division with operands of
+      --  fixed point types shall be qualified or explicitly converted to
+      --  identify the result type.
+
+      if Formal_Verification_Mode
+        and then (Is_Fixed_Point_Type (Etype (L))
+                  or else Is_Fixed_Point_Type (Etype (R)))
+        and then Nkind_In (N, N_Op_Multiply, N_Op_Divide)
+        and then
+          not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
+      then
+         Error_Msg_F
+           ("|~~operation should be qualified or explicitly converted", N);
+      end if;
+
       --  Set overflow and division checking bit. Much cleverer code needed
       --  here eventually and perhaps the Resolve routines should be separated
       --  for the various arithmetic operations, since they will need
@@ -5792,6 +5899,22 @@ package body Sem_Res is
       Generate_Operator_Reference (N, T);
       Check_Low_Bound_Tested (N);
 
+      --  In SPARK or ALFA, ordering operators <, <=, >, >= are not defined
+      --  for Boolean types or array types except String.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+      then
+         if Is_Boolean_Type (T) then
+            Error_Msg_F ("|~~comparison is not defined on Boolean type", N);
+         elsif Is_Array_Type (T)
+           and then Base_Type (T) /= Standard_String
+         then
+            Error_Msg_F
+              ("|~~comparison is not defined on array type except String", N);
+         end if;
+      end if;
+
       --  Check comparison on unordered enumeration
 
       if Comes_From_Source (N)
@@ -6635,6 +6758,20 @@ package body Sem_Res is
          Resolve (L, T);
          Resolve (R, T);
 
+         --  In SPARK or ALFA, equality operators = and /= for array types
+         --  other than String are only defined when, for each index position,
+         --  the operands have equal static bounds.
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (Original_Node (N))
+           and then Is_Array_Type (T)
+           and then Base_Type (T) /= Standard_String
+           and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
+         then
+            Error_Msg_F
+              ("|~~array types should have matching static bounds", N);
+         end if;
+
          --  If the unique type is a class-wide type then it will be expanded
          --  into a dispatching call to the predefined primitive. Therefore we
          --  check here for potential violation of such restriction.
@@ -7163,48 +7300,11 @@ package body Sem_Res is
 
       if Formal_Verification_Mode
         and then Comes_From_Source (Original_Node (N))
-        and then Is_Array_Type (Etype (N))
+        and then Is_Array_Type (B_Typ)
+        and then not Matching_Static_Array_Bounds (Etype (Left_Opnd (N)),
+                                                   Etype (Right_Opnd (N)))
       then
-         declare
-            L_Index : Node_Id;
-            R_Index : Node_Id;
-            L_Low   : Node_Id;
-            L_High  : Node_Id;
-            R_Low   : Node_Id;
-            R_High  : Node_Id;
-
-            L_Typ : constant Node_Id := Etype (Left_Opnd (N));
-            R_Typ : constant Node_Id := Etype (Right_Opnd (N));
-
-         begin
-            L_Index := First_Index (L_Typ);
-            R_Index := First_Index (R_Typ);
-
-            Get_Index_Bounds (L_Index, L_Low, L_High);
-            Get_Index_Bounds (R_Index, R_Low, R_High);
-
-            --  Another error is issued for constrained array types with
-            --  non-static bounds elsewhere, so only deal with different
-            --  constrained types, or unconstrained types.
-
-            if L_Typ /= R_Typ or else not Is_Constrained (L_Typ) then
-               if not Is_Static_Expression (L_Low)
-                 or else not Is_Static_Expression (R_Low)
-                 or else Expr_Value (L_Low) /= Expr_Value (R_Low)
-               then
-                  Error_Msg_F ("|~~operation defined only when both operands "
-                               & "have the same static lower bound", N);
-               end if;
-
-               if not Is_Static_Expression (L_High)
-                 or else not Is_Static_Expression (R_High)
-                 or else Expr_Value (L_High) /= Expr_Value (R_High)
-               then
-                  Error_Msg_F ("|~~operation defined only when both operands "
-                               & "have the same static higher bound", N);
-               end if;
-            end if;
-         end;
+         Error_Msg_F ("|~~array types should have matching static bounds", N);
       end if;
 
    end Resolve_Logical_Op;
@@ -7857,6 +7957,15 @@ package body Sem_Res is
    begin
       Resolve (Expr, Target_Typ);
 
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+        and then Is_Array_Type (Target_Typ)
+        and then Is_Array_Type (Etype (Expr))
+        and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr))
+      then
+         Error_Msg_F ("|~~array types should have matching static bounds", N);
+      end if;
+
       --  A qualified expression requires an exact match of the type,
       --  class-wide matching is not allowed. However, if the qualifying
       --  type is specific and the expression has a class-wide type, it
@@ -8971,6 +9080,18 @@ package body Sem_Res is
 
       Resolve (Operand);
 
+      --  In SPARK or ALFA, a type conversion between array types should be
+      --  restricted to types which have matching static bounds.
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (Original_Node (N))
+        and then Is_Array_Type (Target_Typ)
+        and then Is_Array_Type (Operand_Typ)
+        and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
+      then
+         Error_Msg_F ("|~~array types should have matching static bounds", N);
+      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/sinfo.adb b/gcc/ada/sinfo.adb
index 3a67e72..4242142 100644
--- a/gcc/ada/sinfo.adb
+++ b/gcc/ada/sinfo.adb
@@ -1223,6 +1223,7 @@ package body Sinfo is
         or else NT (N).Nkind = N_Discriminant_Association
         or else NT (N).Nkind = N_Discriminant_Specification
         or else NT (N).Nkind = N_Exception_Declaration
+        or else NT (N).Nkind = N_Expression_Function
         or else NT (N).Nkind = N_Expression_With_Actions
         or else NT (N).Nkind = N_Free_Statement
         or else NT (N).Nkind = N_Mod_Clause
@@ -1230,7 +1231,6 @@ package body Sinfo is
         or else NT (N).Nkind = N_Number_Declaration
         or else NT (N).Nkind = N_Object_Declaration
         or else NT (N).Nkind = N_Parameter_Specification
-        or else NT (N).Nkind = N_Parameterized_Expression
         or else NT (N).Nkind = N_Pragma_Argument_Association
         or else NT (N).Nkind = N_Qualified_Expression
         or else NT (N).Nkind = N_Raise_Statement
@@ -2797,12 +2797,12 @@ package body Sinfo is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Abstract_Subprogram_Declaration
+        or else NT (N).Nkind = N_Expression_Function
         or else NT (N).Nkind = N_Formal_Abstract_Subprogram_Declaration
         or else NT (N).Nkind = N_Formal_Concrete_Subprogram_Declaration
         or else NT (N).Nkind = N_Generic_Package_Declaration
         or else NT (N).Nkind = N_Generic_Subprogram_Declaration
         or else NT (N).Nkind = N_Package_Declaration
-        or else NT (N).Nkind = N_Parameterized_Expression
         or else NT (N).Nkind = N_Subprogram_Body
         or else NT (N).Nkind = N_Subprogram_Body_Stub
         or else NT (N).Nkind = N_Subprogram_Declaration
@@ -4267,6 +4267,7 @@ package body Sinfo is
         or else NT (N).Nkind = N_Discriminant_Association
         or else NT (N).Nkind = N_Discriminant_Specification
         or else NT (N).Nkind = N_Exception_Declaration
+        or else NT (N).Nkind = N_Expression_Function
         or else NT (N).Nkind = N_Expression_With_Actions
         or else NT (N).Nkind = N_Free_Statement
         or else NT (N).Nkind = N_Mod_Clause
@@ -4274,7 +4275,6 @@ package body Sinfo is
         or else NT (N).Nkind = N_Number_Declaration
         or else NT (N).Nkind = N_Object_Declaration
         or else NT (N).Nkind = N_Parameter_Specification
-        or else NT (N).Nkind = N_Parameterized_Expression
         or else NT (N).Nkind = N_Pragma_Argument_Association
         or else NT (N).Nkind = N_Qualified_Expression
         or else NT (N).Nkind = N_Raise_Statement
@@ -5842,12 +5842,12 @@ package body Sinfo is
    begin
       pragma Assert (False
         or else NT (N).Nkind = N_Abstract_Subprogram_Declaration
+        or else NT (N).Nkind = N_Expression_Function
         or else NT (N).Nkind = N_Formal_Abstract_Subprogram_Declaration
         or else NT (N).Nkind = N_Formal_Concrete_Subprogram_Declaration
         or else NT (N).Nkind = N_Generic_Package_Declaration
         or else NT (N).Nkind = N_Generic_Subprogram_Declaration
         or else NT (N).Nkind = N_Package_Declaration
-        or else NT (N).Nkind = N_Parameterized_Expression
         or else NT (N).Nkind = N_Subprogram_Body
         or else NT (N).Nkind = N_Subprogram_Body_Stub
         or else NT (N).Nkind = N_Subprogram_Declaration
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index fb8f203..a4ccd62e 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -4591,17 +4591,17 @@ package Sinfo is
       --  Has_Relative_Deadline_Pragma (Flag9-Sem)
       --  Has_Pragma_CPU (Flag14-Sem)
 
-      ------------------------------
-      -- Parameterized Expression --
-      ------------------------------
+      -------------------------
+      -- Expression Function --
+      -------------------------
 
       --  This is an Ada 2012 extension, we put it here for now, to be labeled
       --  and put in its proper section when we know exactly where that is!
 
-      --  PARAMETERIZED_EXPRESSION ::=
+      --  EXPRESSION_FUNCTION ::=
       --    FUNCTION SPECIFICATION IS (EXPRESSION);
 
-      --  N_Parameterized_Expression
+      --  N_Expression_Function
       --  Sloc points to FUNCTION
       --  Specification (Node1)
       --  Expression (Node3)
@@ -7591,6 +7591,7 @@ package Sinfo is
 
       N_Component_Declaration,
       N_Entry_Declaration,
+      N_Expression_Function,
       N_Formal_Object_Declaration,
       N_Formal_Type_Declaration,
       N_Full_Type_Declaration,
@@ -7598,7 +7599,6 @@ package Sinfo is
       N_Iterator_Specification,
       N_Loop_Parameter_Specification,
       N_Object_Declaration,
-      N_Parameterized_Expression,
       N_Protected_Type_Declaration,
       N_Private_Extension_Declaration,
       N_Private_Type_Declaration,
@@ -10818,7 +10818,7 @@ package Sinfo is
         4 => True,    --  Handled_Statement_Sequence (Node4)
         5 => False),  --  Corresponding_Spec (Node5-Sem)
 
-     N_Parameterized_Expression =>
+     N_Expression_Function =>
        (1 => True,    --  Specification (Node1)
         2 => False,   --  unused
         3 => True,    --  Expression (Node3)
@@ -12317,8 +12317,18 @@ package Sinfo is
    pragma Inline (Set_Withed_Body);
    pragma Inline (Set_Zero_Cost_Handling);
 
+   --------------
+   -- Synonyms --
+   --------------
+
+   --  These synonyms are to aid in transition, they should eventually be
+   --  removed when all remaining references to the obsolete name are gone.
+
    N_Simple_Return_Statement : constant Node_Kind := N_Return_Statement;
    --  Rename N_Return_Statement to be N_Simple_Return_Statement. Clients
    --  should refer to N_Simple_Return_Statement.
 
+   N_Parameterized_Expression : constant Node_Kind := N_Expression_Function;
+   --  Old name for expression functions (used during Ada 2012 transition)
+
 end Sinfo;
diff --git a/gcc/ada/sprint.adb b/gcc/ada/sprint.adb
index 7c069165..63bfd54 100644
--- a/gcc/ada/sprint.adb
+++ b/gcc/ada/sprint.adb
@@ -1620,6 +1620,16 @@ package body Sprint is
             Indent_End;
             Write_Indent;
 
+         when N_Expression_Function =>
+            Write_Indent;
+            Sprint_Node_Sloc (Specification (Node));
+            Write_Str (" is");
+            Indent_Begin;
+            Write_Indent;
+            Sprint_Node (Expression (Node));
+            Write_Char (';');
+            Indent_End;
+
          when N_Extended_Return_Statement =>
             Write_Indent_Str_Sloc ("return ");
             Sprint_Node_List (Return_Object_Declarations (Node));
@@ -2488,17 +2498,6 @@ package body Sprint is
                Write_Str (", ");
             end if;
 
-         when N_Parameterized_Expression =>
-            Write_Indent;
-            Sprint_Node_Sloc (Specification (Node));
-
-            Write_Str (" is");
-            Indent_Begin;
-            Write_Indent;
-            Sprint_Node (Expression (Node));
-            Write_Char (';');
-            Indent_End;
-
          when N_Pop_Constraint_Error_Label =>
             Write_Indent_Str ("%pop_constraint_error_label");