par-ch6.adb: Correct obsolete name in comments

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

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

From-SVN: r177125
This commit is contained in:
Yannick Moy 2011-08-02 10:21:47 +00:00 committed by Arnaud Charlet
parent 176dadf639
commit e24329cdf0
10 changed files with 237 additions and 33 deletions

View File

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

View File

@ -1492,25 +1492,25 @@ package body Ch6 is
-- 6.4 Function Call --
------------------------
-- Parsed by P_Call_Or_Name (4.1)
-- Parsed by P_Name (4.1)
--------------------------------
-- 6.4 Actual Parameter Part --
--------------------------------
-- Parsed by P_Call_Or_Name (4.1)
-- Parsed by P_Name (4.1)
--------------------------------
-- 6.4 Parameter Association --
--------------------------------
-- Parsed by P_Call_Or_Name (4.1)
-- Parsed by P_Name (4.1)
------------------------------------
-- 6.4 Explicit Actual Parameter --
------------------------------------
-- Parsed by P_Call_Or_Name (4.1)
-- Parsed by P_Name (4.1)
---------------------------
-- 6.5 Return Statement --

View File

@ -118,6 +118,18 @@ package body Restrict is
end if;
end Check_Formal_Restriction;
procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
begin
pragma Assert (Msg2'Length /= 0 and then Msg2 (Msg2'First) = '\');
if Formal_Verification_Mode
and then Comes_From_Source (Original_Node (N))
then
Error_Msg_F ("|~~" & Msg1, N);
Error_Msg_F (Msg2, N);
end if;
end Check_Formal_Restriction;
-----------------------------------------
-- Check_Implicit_Dynamic_Code_Allowed --
-----------------------------------------

View File

@ -225,6 +225,10 @@ package Restrict is
-- "|~~" (error not serious, language prepended). Call has no effect if
-- not in formal mode, or if N does not come originally from source.
procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id);
-- Same as Check_Formal_Restriction except there is a continuation message
-- Msg2 following the initial message Msg1.
procedure Check_Implicit_Dynamic_Code_Allowed (N : Node_Id);
-- Tests to see if dynamic code generation (dynamically generated
-- trampolines, in particular) is allowed by the current restrictions

View File

@ -807,7 +807,12 @@ package body Sem_Ch5 is
HSS : constant Node_Id := Handled_Statement_Sequence (N);
begin
Check_Formal_Restriction ("block statement is not allowed", N);
-- Only reject block statements that originate from a source block
-- statement, in formal mode.
if Nkind (Original_Node (N)) = N_Block_Statement then
Check_Formal_Restriction ("block statement is not allowed", N);
end if;
-- If no handled statement sequence is present, things are really messed
-- up, and we just return immediately (defence against previous errors).

View File

@ -325,9 +325,9 @@ package body Sem_Ch6 is
----------------------------
procedure Analyze_Function_Call (N : Node_Id) is
P : constant Node_Id := Name (N);
L : constant List_Id := Parameter_Associations (N);
Actual : Node_Id;
P : constant Node_Id := Name (N);
Actuals : constant List_Id := Parameter_Associations (N);
Actual : Node_Id;
begin
Analyze (P);
@ -353,8 +353,8 @@ package body Sem_Ch6 is
-- Otherwise analyze the parameters
if Present (L) then
Actual := First (L);
if Present (Actuals) then
Actual := First (Actuals);
while Present (Actual) loop
Analyze (Actual);
Check_Parameterless_Call (Actual);

View File

@ -43,6 +43,7 @@ with Nmake; use Nmake;
with Nlists; use Nlists;
with Opt; use Opt;
with Output; use Output;
with Restrict; use Restrict;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Cat; use Sem_Cat;
@ -873,6 +874,11 @@ package body Sem_Ch7 is
-- private_with_clauses, and remove them at the end of the nested
-- package.
procedure Check_One_Tagged_Type_Or_Extension_At_Most;
-- Issue an error in formal mode if a package specification contains
-- more than one tagged type or type extension. This is a restriction of
-- SPARK.
procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-- Clears constant indications (Never_Set_In_Source, Constant_Value, and
-- Is_True_Constant) on all variables that are entities of Id, and on
@ -901,6 +907,56 @@ package body Sem_Ch7 is
-- private part rather than being done in Sem_Ch12.Install_Parent
-- (which is where the parents' visible declarations are installed).
------------------------------------------------
-- Check_One_Tagged_Type_Or_Extension_At_Most --
------------------------------------------------
procedure Check_One_Tagged_Type_Or_Extension_At_Most is
Previous : Node_Id;
procedure Check_Decls (Decls : List_Id);
-- Check that either Previous is Empty and Decls does not contain
-- more than one tagged type or type extension, or Previous is
-- already set and Decls contains no tagged type or type extension.
-----------------
-- Check_Decls --
-----------------
procedure Check_Decls (Decls : List_Id) is
Decl : Node_Id;
begin
Decl := First (Decls);
while Present (Decl) loop
if Nkind (Decl) = N_Full_Type_Declaration
and then Is_Tagged_Type (Defining_Identifier (Decl))
then
if No (Previous) then
Previous := Decl;
else
Error_Msg_Sloc := Sloc (Previous);
Check_Formal_Restriction
("at most one tagged type or type extension allowed",
"\\ previous declaration#",
Decl);
end if;
end if;
Next (Decl);
end loop;
end Check_Decls;
-- Start of processing for Check_One_Tagged_Type_Or_Extension_At_Most
begin
Previous := Empty;
Check_Decls (Vis_Decls);
if Present (Priv_Decls) then
Check_Decls (Priv_Decls);
end if;
end Check_One_Tagged_Type_Or_Extension_At_Most;
---------------------
-- Clear_Constants --
---------------------
@ -1383,6 +1439,8 @@ package body Sem_Ch7 is
Clear_Constants (Id, First_Entity (Id));
Clear_Constants (Id, First_Private_Entity (Id));
end if;
Check_One_Tagged_Type_Or_Extension_At_Most;
end Analyze_Package_Specification;
--------------------------------------

View File

@ -3585,29 +3585,70 @@ package body Sem_Res is
A_Typ := Etype (A);
F_Typ := Etype (F);
-- In SPARK or ALFA, the only view conversions are those involving
-- ancestor conversion of an extended type.
if Nkind (A) = N_Type_Conversion
and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
if Comes_From_Source (Original_Node (N))
and then Nkind_In (Original_Node (N),
N_Function_Call,
N_Procedure_Call_Statement)
then
declare
Operand : constant Node_Id := Expression (A);
Operand_Typ : constant Entity_Id := Etype (Operand);
Target_Typ : constant Entity_Id := A_Typ;
-- In formal mode, check that actual parameters matching
-- formals of tagged types are objects (or ancestor type
-- conversions of objects), not general expressions.
begin
if not (Is_Tagged_Type (Target_Typ)
if Is_Actual_Tagged_Parameter (A) then
if Is_SPARK_Object_Reference (A) then
null;
elsif Nkind (A) = N_Type_Conversion then
declare
Operand : constant Node_Id := Expression (A);
Operand_Typ : constant Entity_Id := Etype (Operand);
Target_Typ : constant Entity_Id := A_Typ;
begin
if not Is_SPARK_Object_Reference (Operand) then
Check_Formal_Restriction
("object required", Operand);
-- In formal mode, the only view conversions are those
-- involving ancestor conversion of an extended type.
elsif not
(Is_Tagged_Type (Target_Typ)
and then not Is_Class_Wide_Type (Target_Typ)
and then Is_Tagged_Type (Operand_Typ)
and then not Is_Class_Wide_Type (Operand_Typ)
and then Is_Ancestor (Target_Typ, Operand_Typ))
then
Check_Formal_Restriction
("ancestor conversion is the only permitted view "
& "conversion", A);
then
if Ekind_In
(F, E_Out_Parameter, E_In_Out_Parameter)
then
Check_Formal_Restriction
("ancestor conversion is the only permitted "
& "view conversion", A);
else
Check_Formal_Restriction
("ancestor conversion required", A);
end if;
else
null;
end if;
end;
else
Check_Formal_Restriction ("object required", A);
end if;
end;
-- In formal mode, the only view conversions are those
-- involving ancestor conversion of an extended type.
elsif Nkind (A) = N_Type_Conversion
and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
then
Check_Formal_Restriction
("ancestor conversion is the only permitted view "
& "conversion", A);
end if;
end if;
-- Save actual for subsequent check on order dependence, and
@ -9056,6 +9097,19 @@ package body Sem_Res is
("array types should have matching static bounds", N);
end if;
-- In formal mode, the operand of an ancestor type conversion must be an
-- object (not an expression).
if Is_Tagged_Type (Target_Typ)
and then not Is_Class_Wide_Type (Target_Typ)
and then Is_Tagged_Type (Operand_Typ)
and then not Is_Class_Wide_Type (Operand_Typ)
and then Is_Ancestor (Target_Typ, Operand_Typ)
and then not Is_SPARK_Object_Reference (Operand)
then
Check_Formal_Restriction ("object required", Operand);
end if;
-- Note: we do the Eval_Type_Conversion call before applying the
-- required checks for a subtype conversion. This is important, since
-- both are prepared under certain circumstances to change the type

View File

@ -3359,7 +3359,7 @@ package body Sem_Util is
then
Call := Parent (Parnt);
elsif Nkind (Parnt) = N_Procedure_Call_Statement then
elsif Nkind_In (Parnt, N_Procedure_Call_Statement, N_Function_Call) then
Call := Parnt;
else
@ -5883,6 +5883,18 @@ package body Sem_Util is
end case;
end Is_Actual_Parameter;
--------------------------------
-- Is_Actual_Tagged_Parameter --
--------------------------------
function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean is
Formal : Entity_Id;
Call : Node_Id;
begin
Find_Actual (N, Formal, Call);
return Present (Formal) and then Is_Tagged_Type (Etype (Formal));
end Is_Actual_Tagged_Parameter;
---------------------
-- Is_Aliased_View --
---------------------
@ -6833,6 +6845,29 @@ package body Sem_Util is
end if;
end Is_Object_Reference;
-------------------------------
-- Is_SPARK_Object_Reference --
-------------------------------
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean is
begin
if Is_Entity_Name (N) then
return Present (Entity (N))
and then
(Ekind_In (Entity (N), E_Constant, E_Variable)
or else Ekind (Entity (N)) in Formal_Kind);
else
case Nkind (N) is
when N_Selected_Component =>
return Is_SPARK_Object_Reference (Prefix (N));
when others =>
return False;
end case;
end if;
end Is_SPARK_Object_Reference;
-----------------------------------
-- Is_OK_Variable_For_Out_Formal --
-----------------------------------

View File

@ -353,12 +353,12 @@ package Sem_Util is
(N : Node_Id;
Formal : out Entity_Id;
Call : out Node_Id);
-- Determines if the node N is an actual parameter of a procedure call. If
-- so, then Formal points to the entity for the formal (whose Ekind is one
-- of E_In_Parameter, E_Out_Parameter, E_In_Out_Parameter) and Call is set
-- to the node for the corresponding call. If the node N is not an actual
-- parameter, or is an actual parameter of a function call, then Formal and
-- Call are set to Empty.
-- Determines if the node N is an actual parameter of a function of a
-- procedure call. If so, then Formal points to the entity for the formal
-- (whose Ekind is one of E_In_Parameter, E_Out_Parameter,
-- E_In_Out_Parameter) and Call is set to the node for the corresponding
-- call. If the node N is not an actual parameter then Formal and Call are
-- set to Empty.
function Find_Corresponding_Discriminant
(Id : Node_Id;
@ -677,6 +677,10 @@ package Sem_Util is
function Is_Actual_Parameter (N : Node_Id) return Boolean;
-- Determines if N is an actual parameter in a subprogram call
function Is_Actual_Tagged_Parameter (N : Node_Id) return Boolean;
-- Determines if N is an actual parameter of a formal of tagged type in a
-- subprogram call.
function Is_Aliased_View (Obj : Node_Id) return Boolean;
-- Determine if Obj is an aliased view, i.e. the name of an object to which
-- 'Access or 'Unchecked_Access can apply.
@ -763,6 +767,9 @@ package Sem_Util is
-- Determines if the tree referenced by N represents an object. Both
-- variable and constant objects return True (compare Is_Variable).
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK.
function Is_OK_Variable_For_Out_Formal (AV : Node_Id) return Boolean;
-- Used to test if AV is an acceptable formal for an OUT or IN OUT formal.
-- Note that the Is_Variable function is not quite the right test because