mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-03-24 08:50:26 +08:00
Code Issues Packages Projects Releases Wiki Activity

[multiple changes]

Browse Source 
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.

From-SVN: r244398
This commit is contained in:
Arnaud Charlet 2017-01-13 10:59:17 +01:00
parent 9574e75fb0
commit 27bb794147
12 changed files with 293 additions and 93 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
gcc/ada/ChangeLog
View File

@ -1,3 +1,48 @@
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

4
gcc/ada/atree.adb
View File

@ -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.

66
gcc/ada/checks.adb
View File

@ -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
-- 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 Expander_Active
or else Discriminant_Checks_Suppressed (T_Typ)
then
return;
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
-- Note: this means that we lose some useful warnings if the expander
-- is not active, and we also lose these warnings in SPARK mode ???
-- 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.
if not Expander_Active then
-- Note: this means that we lose some useful warnings if the expander
-- is not active.
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;

8
gcc/ada/einfo.adb
View File

@ -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);

82
gcc/ada/exp_util.adb
View File

@ -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;

13
gcc/ada/frontend.adb
View File

@ -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;

13
gcc/ada/gnat1drv.adb
View File

@ -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

2
gcc/ada/rtsfind.ads
View File

@ -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,

21
gcc/ada/sem_attr.adb
View File

@ -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

8
gcc/ada/sem_ch6.adb
View File

@ -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))

106
gcc/ada/sem_ch8.adb
View File

@ -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

18
gcc/ada/sem_res.adb
View File

@ -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