2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>

	* exp_util.adb (Add_Inherited_Tagged_DIC):
	Pass the object parameters of both the parent and the derived
	type DIC procedure to the reference replacement circuitry.
	(Find_DIC_Type): Modify the circuitry to present the partial
	view of a private type in case the private type defines its own
	DIC pragma.
	(Replace_Object_And_Primitive_References): Add two
	optional formal parameters.  Update the comment on usage. Update
	the replacement of references to object parameters.

2017-01-13  Gary Dismukes  <dismukes@adacore.com>

	* einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix.

2017-01-13  Ed Schonberg  <schonberg@adacore.com>

	* sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to
	an out parameter that is a type conversion, independently of th
	range check that may apply to the expression of the conversion,
	for use in GNATProve.

2017-01-13  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb (Gnat1drv): Move the implicit with for System in
	GNATprove_Mode here to Frontend.
	* frontend.adb (Frontend): Move the implicit with for System
	in GNATprove_Mode here as it ismore correct this way; the old
	place only worked by chance, since there were no overloaded names.
	* rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State.
	* sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the
	four attributes identified in SRM 9(18), add an implicit with
	to Ada.Task_Identification.
	* sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper):
	Deal specially with the wrapper introduced for AI05-0071 in GNATprove
	mode.
	* checks.adb (Apply_Discriminant_Check,
	Apply_Selected_Length_Checks, Apply_Selected_Range_Checks):
	In GNATprove mode, we do not apply the checks, but we still
	analyze the expression to possibly issue errors on SPARK
	code when a run-time error can be detected at compile time.
	(Selected_Length_Checks, Selected_Range_Checks): Perform analysis
	in GNATprove mode.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@244398 138bc75d-0d04-0410-961f-82ee72b054a4

12 files changed, 293 insertions, 93 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0569679f841..f9d3a503035 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,50 @@
 2017-01-13  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* exp_util.adb (Add_Inherited_Tagged_DIC):
+	Pass the object parameters of both the parent and the derived
+	type DIC procedure to the reference replacement circuitry.
+	(Find_DIC_Type): Modify the circuitry to present the partial
+	view of a private type in case the private type defines its own
+	DIC pragma.
+	(Replace_Object_And_Primitive_References): Add two
+	optional formal parameters.  Update the comment on usage. Update
+	the replacement of references to object parameters.
+
+2017-01-13  Gary Dismukes  <dismukes@adacore.com>
+
+	* einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix.
+
+2017-01-13  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to
+	an out parameter that is a type conversion, independently of th
+	range check that may apply to the expression of the conversion,
+	for use in GNATProve.
+
+2017-01-13  Yannick Moy  <moy@adacore.com>
+
+	* gnat1drv.adb (Gnat1drv): Move the implicit with for System in
+	GNATprove_Mode here to Frontend.
+	* frontend.adb (Frontend): Move the implicit with for System
+	in GNATprove_Mode here as it ismore correct this way; the old
+	place only worked by chance, since there were no overloaded names.
+	* rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State.
+	* sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the
+	four attributes identified in SRM 9(18), add an implicit with
+	to Ada.Task_Identification.
+	* sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper):
+	Deal specially with the wrapper introduced for AI05-0071 in GNATprove
+	mode.
+	* checks.adb (Apply_Discriminant_Check,
+	Apply_Selected_Length_Checks, Apply_Selected_Range_Checks):
+	In GNATprove mode, we do not apply the checks, but we still
+	analyze the expression to possibly issue errors on SPARK
+	code when a run-time error can be detected at compile time.
+	(Selected_Length_Checks, Selected_Range_Checks): Perform analysis
+	in GNATprove mode.
+
+2017-01-13  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* expander.adb (Expand): Add a warning about using return
 	statements in Ghost management code.
 	* exp_ch3.adb (Freeze_Type): Add a warning about using return
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 1444fcb6dfe..2e56371600b 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -556,7 +556,7 @@ package body Atree is
    --  information for the newly-allocated node is copied from it.
 
    procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
-   --  Fixup parent pointers for the syntactic children of Fix_Node after a
+   --  Fix up parent pointers for the syntactic children of Fix_Node after a
    --  copy, setting them to Fix_Node when they pointed to Ref_Node.
 
    procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id);
@@ -1430,7 +1430,7 @@ package body Atree is
 
    procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is
       procedure Fix_Parent (Field : Union_Id);
-      --  Fixup one parent pointer. Field is checked to see if it points to
+      --  Fix up one parent pointer. Field is checked to see if it points to
       --  a node, list, or element list that has a parent that points to
       --  Ref_Node. If so, the parent is reset to point to Fix_Node.
 
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 10dbbaf75e9..6689cb56f07 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -1447,13 +1447,17 @@ package body Checks is
          T_Typ := Typ;
       end if;
 
-      --  Nothing to do if discriminant checks are suppressed or else no code
-      --  is to be generated
-
-      if not Expander_Active
-        or else Discriminant_Checks_Suppressed (T_Typ)
-      then
-         return;
+      --  Only apply checks when generating code and discriminant checks are
+      --  not suppressed. In GNATprove mode, we do not apply the checks, but we
+      --  still analyze the expression to possibly issue errors on SPARK code
+      --  when a run-time error can be detected at compile time.
+
+      if not GNATprove_Mode then
+         if not Expander_Active
+           or else Discriminant_Checks_Suppressed (T_Typ)
+         then
+            return;
+         end if;
       end if;
 
       --  No discriminant checks necessary for an access when expression is
@@ -1690,6 +1694,12 @@ package body Checks is
          end;
       end if;
 
+      --  In GNATprove mode, we do not apply the checks
+
+      if GNATprove_Mode then
+         return;
+      end if;
+
       --  Here we need a discriminant check. First build the expression
       --  for the comparisons of the discriminants:
 
@@ -3075,16 +3085,25 @@ package body Checks is
           or else (not Length_Checks_Suppressed (Target_Typ));
 
    begin
+      --  Only apply checks when generating code. In GNATprove mode, we do
+      --  not apply the checks, but we still call Selected_Length_Checks to
+      --  possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
       --  Note: this means that we lose some useful warnings if the expander
-      --  is not active, and we also lose these warnings in SPARK mode ???
+      --  is not active.
 
-      if not Expander_Active then
+      if not Expander_Active and not GNATprove_Mode then
          return;
       end if;
 
       R_Result :=
         Selected_Length_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
 
+      if GNATprove_Mode then
+         return;
+      end if;
+
       for J in 1 .. 2 loop
          R_Cno := R_Result (J);
          exit when No (R_Cno);
@@ -3186,13 +3205,24 @@ package body Checks is
       R_Result : Check_Result;
 
    begin
-      if not Expander_Active or not Checks_On then
-         return;
+      --  Only apply checks when generating code. In GNATprove mode, we do not
+      --  apply the checks, but we still call Selected_Range_Checks to possibly
+      --  issue errors on SPARK code when a run-time error can be detected at
+      --  compile time.
+
+      if not GNATprove_Mode then
+         if not Expander_Active or not Checks_On then
+            return;
+         end if;
       end if;
 
       R_Result :=
         Selected_Range_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
 
+      if GNATprove_Mode then
+         return;
+      end if;
+
       for J in 1 .. 2 loop
          R_Cno := R_Result (J);
          exit when No (R_Cno);
@@ -9052,7 +9082,12 @@ package body Checks is
    --  Start of processing for Selected_Length_Checks
 
    begin
-      if not Expander_Active then
+      --  Checks will be applied only when generating code. In GNATprove mode,
+      --  we do not apply the checks, but we still call Selected_Length_Checks
+      --  to possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
+      if not Expander_Active and not GNATprove_Mode then
          return Ret_Result;
       end if;
 
@@ -9602,7 +9637,12 @@ package body Checks is
    --  Start of processing for Selected_Range_Checks
 
    begin
-      if not Expander_Active then
+      --  Checks will be applied only when generating code. In GNATprove mode,
+      --  we do not apply the checks, but we still call Selected_Range_Checks
+      --  to possibly issue errors on SPARK code when a run-time error can be
+      --  detected at compile time.
+
+      if not Expander_Active and not GNATprove_Mode then
          return Ret_Result;
       end if;
 
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index c2146756843..f007c2a4e3d 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -2093,7 +2093,7 @@ package body Einfo is
 
    function Is_Checked_Ghost_Entity (Id : E) return B is
    begin
-      --  Allow this attribute to appear on non-analyzed entities
+      --  Allow this attribute to appear on unanalyzed entities
 
       pragma Assert (Nkind (Id) in N_Entity
         or else Ekind (Id) = E_Void);
@@ -2283,7 +2283,7 @@ package body Einfo is
 
    function Is_Ignored_Ghost_Entity (Id : E) return B is
    begin
-      --  Allow this attribute to appear on non-analyzed entities
+      --  Allow this attribute to appear on unanalyzed entities
 
       pragma Assert (Nkind (Id) in N_Entity
         or else Ekind (Id) = E_Void);
@@ -5167,7 +5167,7 @@ package body Einfo is
 
    procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is
    begin
-      --  Allow this attribute to appear on non-analyzed entities
+      --  Allow this attribute to appear on unanalyzed entities
 
       pragma Assert (Nkind (Id) in N_Entity
         or else Ekind (Id) = E_Void);
@@ -5372,7 +5372,7 @@ package body Einfo is
 
    procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is
    begin
-      --  Allow this attribute to appear on non-analyzed entities
+      --  Allow this attribute to appear on unanalyzed entities
 
       pragma Assert (Nkind (Id) in N_Entity
         or else Ekind (Id) = E_Void);
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 3d09a963865..ea71e38fe0b 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1237,14 +1237,17 @@ package body Exp_Util is
       procedure Replace_Object_And_Primitive_References
         (Expr      : Node_Id;
          Par_Typ   : Entity_Id;
-         Deriv_Typ : Entity_Id);
+         Deriv_Typ : Entity_Id;
+         Par_Obj   : Entity_Id := Empty;
+         Deriv_Obj : Entity_Id := Empty);
       --  Expr denotes an arbitrary expression. Par_Typ is a parent type in a
-      --  type hierarchy. Deriv_Typ is a type derived from Par_Typ. Perform the
-      --  following substitutions:
+      --  type hierarchy. Deriv_Typ is a type derived from Par_Typ. Par_Obj is
+      --  the formal parameter which emulates the current instance of Par_Typ.
+      --  Deriv_Obj is the formal parameter which emulates the current instance
+      --  of Deriv_Typ. Perform the following substitutions:
       --
-      --    * Replace a reference to the _object parameter of the parent type's
-      --      DIC procedure with a reference to the _object parameter of the
-      --      derived type's DIC procedure.
+      --    * Replace a reference to Par_Obj with a reference to Deriv_Obj if
+      --      applicable.
       --
       --    * Replace a call to an overridden parent primitive with a call to
       --      the overriding derived type primitive.
@@ -1340,11 +1343,13 @@ package body Exp_Util is
          Deriv_Typ : Entity_Id;
          Stmts     : in out List_Id)
       is
-         DIC_Args : constant List_Id :=
-                      Pragma_Argument_Associations (DIC_Prag);
-         DIC_Arg  : constant Node_Id := First (DIC_Args);
-         DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg);
-         Typ_Decl : constant Node_Id := Declaration_Node (Deriv_Typ);
+         Deriv_Decl : constant Node_Id   := Declaration_Node (Deriv_Typ);
+         Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
+         DIC_Args   : constant List_Id   :=
+                        Pragma_Argument_Associations (DIC_Prag);
+         DIC_Arg    : constant Node_Id   := First (DIC_Args);
+         DIC_Expr   : constant Node_Id   := Expression_Copy (DIC_Arg);
+         Par_Proc   : constant Entity_Id := DIC_Procedure (Par_Typ);
 
          Expr : Node_Id;
 
@@ -1373,15 +1378,19 @@ package body Exp_Util is
          --  handled by the overriding/inheritance mechanism and do not require
          --  an extra replacement pass.
 
+         pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
+
          Replace_Object_And_Primitive_References
            (Expr      => Expr,
             Par_Typ   => Par_Typ,
-            Deriv_Typ => Deriv_Typ);
+            Deriv_Typ => Deriv_Typ,
+            Par_Obj   => First_Formal (Par_Proc),
+            Deriv_Obj => First_Formal (Deriv_Proc));
 
          --  Preanalyze the DIC expression to detect errors and at the same
          --  time capture the visibility of the proper package part.
 
-         Set_Parent (Expr, Typ_Decl);
+         Set_Parent (Expr, Deriv_Decl);
          Preanalyze_Assert_Expression (Expr, Any_Boolean);
 
          --  Once the DIC assertion expression is fully processed, add a check
@@ -1514,14 +1523,10 @@ package body Exp_Util is
       procedure Replace_Object_And_Primitive_References
         (Expr      : Node_Id;
          Par_Typ   : Entity_Id;
-         Deriv_Typ : Entity_Id)
+         Deriv_Typ : Entity_Id;
+         Par_Obj   : Entity_Id := Empty;
+         Deriv_Obj : Entity_Id := Empty)
       is
-         Deriv_Obj : Entity_Id;
-         --  The _object parameter of the derived type's DIC procedure
-
-         Par_Obj : Entity_Id;
-         --  The _object parameter of the parent type's DIC procedure
-
          function Replace_Ref (Ref : Node_Id) return Traverse_Result;
          --  Substitute a reference to an entity with a reference to the
          --  corresponding entity stored in in table Primitives_Mapping.
@@ -1556,7 +1561,10 @@ package body Exp_Util is
                --  The reference mentions the _object parameter of the parent
                --  type's DIC procedure.
 
-               elsif Ref_Id = Par_Obj then
+               elsif Present (Par_Obj)
+                 and then Present (Deriv_Obj)
+                 and then Ref_Id = Par_Obj
+               then
                   New_Ref := New_Occurrence_Of (Deriv_Obj, Loc);
 
                   --  The reference to _object acts as an actual parameter in a
@@ -1624,19 +1632,9 @@ package body Exp_Util is
 
          procedure Replace_Refs is new Traverse_Proc (Replace_Ref);
 
-         --  Local variables
-
-         Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
-         Par_Proc   : constant Entity_Id := DIC_Procedure (Par_Typ);
-
       --  Start of processing for Replace_Object_And_Primitive_References
 
       begin
-         pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
-
-         Deriv_Obj := First_Entity (Deriv_Proc);
-         Par_Obj   := First_Entity (Par_Proc);
-
          --  Map each primitive operation of the parent type to the proper
          --  primitive of the derived type.
 
@@ -3908,7 +3906,15 @@ package body Exp_Util is
 
    function Find_DIC_Type (Typ : Entity_Id) return Entity_Id is
       Curr_Typ : Entity_Id;
-      DIC_Typ  : Entity_Id;
+      --  The current type being examined in the parent hierarchy traversal
+
+      DIC_Typ : Entity_Id;
+      --  The type which carries the DIC pragma. This variable denotes the
+      --  partial view when private types are involved.
+
+      Par_Typ : Entity_Id;
+      --  The parent type of the current type. This variable denotes the full
+      --  view when private types are involved.
 
    begin
       --  The input type defines its own DIC pragma, therefore it is the owner
@@ -3933,19 +3939,21 @@ package body Exp_Util is
             --  Look at the full view of a private type because the type may
             --  have a hidden parent introduced in the full view.
 
-            if Is_Private_Type (DIC_Typ)
-              and then Present (Full_View (DIC_Typ))
+            Par_Typ := DIC_Typ;
+
+            if Is_Private_Type (Par_Typ)
+              and then Present (Full_View (Par_Typ))
             then
-               DIC_Typ := Full_View (DIC_Typ);
+               Par_Typ := Full_View (Par_Typ);
             end if;
 
             --  Stop the climb once the nearest parent type which defines a DIC
             --  pragma of its own is encountered or when the root of the parent
             --  chain is reached.
 
-            exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = DIC_Typ;
+            exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = Par_Typ;
 
-            Curr_Typ := DIC_Typ;
+            Curr_Typ := Par_Typ;
          end loop;
       end if;
 
diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb
index ff5418a1340..c71c78e40c4 100644
--- a/gcc/ada/frontend.adb
+++ b/gcc/ada/frontend.adb
@@ -460,6 +460,19 @@ begin
       end if;
    end if;
 
+   --  In GNATprove mode, force loading of a few RTE units.
+
+   if GNATprove_Mode then
+      declare
+         Unused_E : Entity_Id;
+      begin
+         --  Ensure that System.Interrupt_Priority is available to
+         --  GNATprove for the generation of VCs related to ceiling
+         --  priority.
+         Unused_E := RTE (RE_Interrupt_Priority);
+      end;
+   end if;
+
    --  Qualify all entity names in inner packages, package bodies, etc.
 
    Exp_Dbug.Qualify_All_Entity_Names;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 1bf10b6b4b4..a2e6e897b74 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1071,19 +1071,6 @@ begin
       Original_Operating_Mode := Operating_Mode;
       Frontend;
 
-      --  In GNATprove mode, force loading of System unit to ensure that
-      --  System.Interrupt_Priority is available to GNATprove for the
-      --  generation of VCs related to ceiling priority.
-
-      if GNATprove_Mode then
-         declare
-            Unused_E : constant Entity_Id :=
-                         Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority);
-         begin
-            null;
-         end;
-      end if;
-
       --  Exit with errors if the main source could not be parsed
 
       if Sinput.Main_Source_File = No_Source_File then
diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads
index a79064644d9..f3dfd3191a0 100644
--- a/gcc/ada/rtsfind.ads
+++ b/gcc/ada/rtsfind.ads
@@ -704,6 +704,7 @@ package Rtsfind is
      RE_Abort_Task,                      -- Ada.Task_Identification
      RE_Current_Task,                    -- Ada.Task_Identification
      RO_AT_Task_Id,                      -- Ada.Task_Identification
+     RE_Tasking_State,                   -- Ada.Task_Identification
 
      RE_Decimal_IO,                      -- Ada.Text_IO
      RE_Fixed_IO,                        -- Ada.Text_IO
@@ -1936,6 +1937,7 @@ package Rtsfind is
      RE_Abort_Task                       => Ada_Task_Identification,
      RE_Current_Task                     => Ada_Task_Identification,
      RO_AT_Task_Id                       => Ada_Task_Identification,
+     RE_Tasking_State                    => Ada_Task_Identification,
 
      RE_Decimal_IO                       => Ada_Text_IO,
      RE_Fixed_IO                         => Ada_Text_IO,
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 494579ac9f8..9adbe7a2e55 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -7109,6 +7109,27 @@ package body Sem_Attr is
 
       end case;
 
+      --  In SPARK some attribute references depend on Tasking_State, so we
+      --  need to make sure we load this so that gnat2why has the entity
+      --  available. See SPARK RM 9(18) for the relevant rule.
+
+      if GNATprove_Mode then
+         declare
+            Unused : Entity_Id;
+         begin
+            case Attr_Id is
+               when Attribute_Callable   |
+                    Attribute_Caller     |
+                    Attribute_Count      |
+                    Attribute_Terminated =>
+                  Unused := RTE (RE_Tasking_State);
+
+               when others =>
+                  null;
+            end case;
+         end;
+      end if;
+
    --  All errors raise Bad_Attribute, so that we get out before any further
    --  damage occurs when an error is detected (for example, if we check for
    --  one attribute expression, and the check succeeds, we want to be able
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 33233bdb854..d092134d73d 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -8408,7 +8408,7 @@ package body Sem_Ch6 is
    --  Start of processing for Fully_Conformant_Expressions
 
    begin
-      --  Non-conformant if paren count does not match. Note: if some idiot
+      --  Nonconformant if paren count does not match. Note: if some idiot
       --  complains that we don't do this right for more than 3 levels of
       --  parentheses, they will be treated with the respect they deserve.
 
@@ -8423,14 +8423,14 @@ package body Sem_Ch6 is
             return Entity (E1) = Entity (E2)
 
               --  One may be a discriminant that has been replaced by
-              --  the correspondding discriminal
+              --  the corresponding discriminal.
 
               or else (Chars (Entity (E1)) = Chars (Entity (E2))
                         and then Ekind (Entity (E1)) = E_Discriminant
                         and then Ekind (Entity (E2)) = E_In_Parameter)
 
-             --  AI12-050 : the loop variables of quantified expressions
-             --  match if the have the same identifier, even though they
+             --  AI12-050 : The loop variables of quantified expressions
+             --  match if they have the same identifier, even though they
              --  are different entities.
 
               or else (Chars (Entity (E1)) = Chars (Entity (E2))
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 86eed89bd7b..1ba49628396 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -1934,6 +1934,14 @@ package body Sem_Ch8 is
       is
          Loc : constant Source_Ptr := Sloc (N);
 
+         function Build_Expr_Fun_Call
+           (Subp_Id : Entity_Id;
+            Params  : List_Id) return Node_Id;
+         --  Create a dispatching call to invoke function Subp_Id with actuals
+         --  built from the parameter specifications of list Params. Return
+         --  directly the call, so that it can be used inside an expression
+         --  function. This is a specificity of the GNATprove mode.
+
          function Build_Call
            (Subp_Id : Entity_Id;
             Params  : List_Id) return Node_Id;
@@ -2004,6 +2012,38 @@ package body Sem_Ch8 is
             end if;
          end Build_Call;
 
+         -------------------------
+         -- Build_Expr_Fun_Call --
+         -------------------------
+
+         function Build_Expr_Fun_Call
+           (Subp_Id : Entity_Id;
+            Params  : List_Id) return Node_Id
+         is
+            Actuals  : constant List_Id := New_List;
+            Call_Ref : constant Node_Id := New_Occurrence_Of (Subp_Id, Loc);
+            Formal   : Node_Id;
+
+         begin
+            --  Build the actual parameters of the call
+
+            Formal := First (Params);
+            while Present (Formal) loop
+               Append_To (Actuals,
+                 Make_Identifier (Loc, Chars (Defining_Identifier (Formal))));
+               Next (Formal);
+            end loop;
+
+            --  Generate:
+            --    Subp_Id (Actuals);
+
+            pragma Assert (Ekind_In (Subp_Id, E_Function, E_Operator));
+
+            return Make_Function_Call (Loc,
+              Name                   => Call_Ref,
+              Parameter_Associations => Actuals);
+         end Build_Expr_Fun_Call;
+
          ----------------
          -- Build_Spec --
          ----------------
@@ -2199,6 +2239,7 @@ package body Sem_Ch8 is
          Formal    : Node_Id;
          Prim_Op   : Entity_Id;
          Spec_Decl : Node_Id;
+         New_Spec  : Node_Id;
 
       --  Start of processing for Build_Class_Wide_Wrapper
 
@@ -2334,31 +2375,62 @@ package body Sem_Ch8 is
          --  Step 3: Create the declaration and the body of the wrapper, insert
          --  all the pieces into the tree.
 
-         Spec_Decl :=
-           Make_Subprogram_Declaration (Loc,
-             Specification => Build_Spec (Ren_Id));
-         Insert_Before_And_Analyze (N, Spec_Decl);
+         --  In GNATprove mode, create a function wrapper in the form of an
+         --  expression function, so that an implicit postcondition relating
+         --  the result of calling the wrapper function and the result of the
+         --  dispatching call to the wrapped function is known during proof.
+
+         if GNATprove_Mode
+           and then Ekind_In (Ren_Id, E_Function, E_Operator)
+         then
+            New_Spec := Build_Spec (Ren_Id);
+            Body_Decl :=
+              Make_Expression_Function (Loc,
+                Specification => New_Spec,
+                Expression    => Build_Expr_Fun_Call
+                  (Subp_Id => Prim_Op,
+                   Params  => Parameter_Specifications (New_Spec)));
+
+            Wrap_Id := Defining_Entity (Body_Decl);
+
+         --  Otherwise, create separate spec and body for the subprogram
+
+         else
+            Spec_Decl :=
+              Make_Subprogram_Declaration (Loc,
+                Specification => Build_Spec (Ren_Id));
+            Insert_Before_And_Analyze (N, Spec_Decl);
+
+            Wrap_Id := Defining_Entity (Spec_Decl);
+
+            Body_Decl :=
+              Make_Subprogram_Body (Loc,
+                Specification              => Build_Spec (Ren_Id),
+                Declarations               => New_List,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements => New_List (
+                      Build_Call
+                        (Subp_Id => Prim_Op,
+                         Params  =>
+                           Parameter_Specifications
+                             (Specification (Spec_Decl))))));
+
+            Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl));
+         end if;
 
          --  If the operator carries an Eliminated pragma, indicate that the
          --  wrapper is also to be eliminated, to prevent spurious error when
          --  using gnatelim on programs that include box-initialization of
          --  equality operators.
 
-         Wrap_Id := Defining_Entity (Spec_Decl);
          Set_Is_Eliminated (Wrap_Id, Is_Eliminated (Prim_Op));
 
-         Body_Decl :=
-           Make_Subprogram_Body (Loc,
-             Specification              => Build_Spec (Ren_Id),
-             Declarations               => New_List,
-             Handled_Statement_Sequence =>
-               Make_Handled_Sequence_Of_Statements (Loc,
-                 Statements => New_List (
-                   Build_Call
-                     (Subp_Id => Prim_Op,
-                      Params  =>
-                        Parameter_Specifications
-                          (Specification (Spec_Decl))))));
+         --  In GNATprove mode, insert the body in the tree for analysis
+
+         if GNATprove_Mode then
+            Insert_Before_And_Analyze (N, Body_Decl);
+         end if;
 
          --  The generated body does not freeze and must be analyzed when the
          --  class-wide wrapper is frozen. The body is only needed if expansion
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index fc377a952fd..235a535c7f9 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4328,24 +4328,36 @@ package body Sem_Res is
 
             if Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) then
 
-               --  If there is a type conversion, to make sure the return value
+               --  If there is a type conversion, make sure the return value
                --  meets the constraints of the variable before the conversion.
 
                if Nkind (A) = N_Type_Conversion then
                   if Is_Scalar_Type (A_Typ) then
                      Apply_Scalar_Range_Check
                        (Expression (A), Etype (Expression (A)), A_Typ);
+
+                     --  In addition, the returned value of the parameter
+                     --  must satisfy the bounds of the object type (see
+                     --  comment below).
+
+                     Apply_Scalar_Range_Check (A, A_Typ, F_Typ);
+
                   else
                      Apply_Range_Check
                        (Expression (A), Etype (Expression (A)), A_Typ);
                   end if;
 
-               --  If no conversion apply scalar range checks and length checks
-               --  base on the subtype of the actual (NOT that of the formal).
+               --  If no conversion, apply scalar range checks and length check
+               --  based on the subtype of the actual (NOT that of the formal).
+               --  This indicates that the check takes place on return from the
+               --  call. During expansion the required constraint checks are
+               --  inserted. In GNATprove mode, in the absence of expansion,
+               --  the flag indicates that the returned value is valid.
 
                else
                   if Is_Scalar_Type (F_Typ) then
                      Apply_Scalar_Range_Check (A, A_Typ, F_Typ);
+
                   elsif Is_Array_Type (F_Typ)
                     and then Ekind (F) = E_Out_Parameter
                   then