* 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
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177125
138bc75d-0d04-0410-961f-
82ee72b054a4
+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
-- 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 --
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 --
-----------------------------------------
-- "|~~" (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
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).
----------------------------
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);
-- 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);
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;
-- 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
-- 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 --
---------------------
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;
--------------------------------------
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
("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
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
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 --
---------------------
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 --
-----------------------------------
(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;
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.
-- 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
OSDN Git Service
