+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
projects / gcc.git / commitdiff