-- of the return object to the specific type on assignments to the
-- individual components.
+ procedure Check_Against_Result_Level (Level : Node_Id);
+ -- Check the given accessibility level against the level
+ -- determined by the point of call. (AI05-0234).
+
+ --------------------------------
+ -- Check_Against_Result_Level --
+ --------------------------------
+
+ procedure Check_Against_Result_Level (Level : Node_Id) is
+ begin
+ Insert_Action (N,
+ Make_Raise_Program_Error (Loc,
+ Condition =>
+ Make_Op_Gt (Loc,
+ Left_Opnd => Level,
+ Right_Opnd =>
+ New_Occurrence_Of
+ (Extra_Accessibility_Of_Result (Scope_Id), Loc)),
+ Reason => PE_Accessibility_Check_Failed));
+ end Check_Against_Result_Level;
+
+ -- Start of processing for Expand_Simple_Function_Return
begin
if Is_Class_Wide_Type (R_Type)
and then not Is_Class_Wide_Type (Exptyp)
Suppress => All_Checks);
end if;
+ -- Determine if the special rules within RM 3.10.2 for explicitly
+ -- aliased formals apply to Exp - in which case we require a dynamic
+ -- check to be generated.
+
+ if Is_Special_Aliased_Formal_Access (Exp, Scope_Id) then
+ Check_Against_Result_Level
+ (Make_Integer_Literal (Loc,
+ Object_Access_Level (Entity (Ultimate_Prefix (Prefix (Exp))))));
+ end if;
+
-- AI05-0234: RM 6.5(21/3). Check access discriminants to
-- ensure that the function result does not outlive an
-- object designated by one of it discriminants.
then
declare
Discrim_Source : Node_Id;
-
- procedure Check_Against_Result_Level (Level : Node_Id);
- -- Check the given accessibility level against the level
- -- determined by the point of call. (AI05-0234).
-
- --------------------------------
- -- Check_Against_Result_Level --
- --------------------------------
-
- procedure Check_Against_Result_Level (Level : Node_Id) is
- begin
- Insert_Action (N,
- Make_Raise_Program_Error (Loc,
- Condition =>
- Make_Op_Gt (Loc,
- Left_Opnd => Level,
- Right_Opnd =>
- New_Occurrence_Of
- (Extra_Accessibility_Of_Result (Scope_Id), Loc)),
- Reason => PE_Accessibility_Check_Failed));
- end Check_Against_Result_Level;
-
begin
Discrim_Source := Exp;
while Nkind (Discrim_Source) = N_Qualified_Expression loop
Control =>
(Controlled with
Container.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Position,
Old_Key => new Key_Type'(Key (Position))))
do
Control =>
(Controlled with
Container.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Find (Container, Key),
Old_Key => new Key_Type'(Key)))
do
Control =>
(Controlled with
HT.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Index => HT_Ops.Index (HT, Position.Node),
Old_Pos => Position,
Old_Hash => Hash (Key (Position))))
Control =>
(Controlled with
HT.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Index => HT_Ops.Index (HT, P.Node),
Old_Pos => P,
Old_Hash => Hash (Key)))
Control =>
(Controlled with
Tree.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Position,
Old_Key => new Key_Type'(Key (Position))))
do
Control =>
(Controlled with
Tree.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Find (Container, Key),
Old_Key => new Key_Type'(Key)))
do
Control =>
(Controlled with
Tree.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Position,
Old_Key => new Key_Type'(Key (Position))))
do
Control =>
(Controlled with
Tree.TC'Unrestricted_Access,
- Container => Container'Access,
+ Container => Container'Unchecked_Access,
Pos => Find (Container, Key),
Old_Key => new Key_Type'(Key)))
do
or else Nkind (Associated_Node_For_Itype (Btyp)) =
N_Object_Declaration)
+ and then Attr_Id = Attribute_Access
+
+ -- Verify that static checking is OK (namely that we aren't
+ -- in a specific context requiring dynamic checks on
+ -- expicitly aliased parameters), and then check the level.
+
+ -- Otherwise a check will be generated later when the return
+ -- statement gets expanded.
+
+ and then not Is_Special_Aliased_Formal_Access
+ (N, Current_Scope)
and then
Object_Access_Level (P) > Deepest_Type_Access_Level (Btyp)
- and then Attr_Id = Attribute_Access
then
-- In an instance, this is a runtime check, but one we know
-- will fail, so generate an appropriate warning. As usual,
then
-- Obtain the object to perform static checks on by moving
-- up the prefixes in the expression taking into account
- -- named access types.
+ -- named access types and renamed objects within the
+ -- expression.
Obj := Original_Node (Prefix (Expr));
- while Nkind_In (Obj, N_Explicit_Dereference,
- N_Indexed_Component,
- N_Selected_Component)
loop
- -- When we encounter a named access type then we can
- -- ignore accessibility checks on the dereference.
+ while Nkind_In (Obj, N_Explicit_Dereference,
+ N_Indexed_Component,
+ N_Selected_Component)
+ loop
+ -- When we encounter a named access type then we can
+ -- ignore accessibility checks on the dereference.
- if Ekind (Etype (Original_Node (Prefix (Obj))))
- in E_Access_Type ..
- E_Access_Protected_Subprogram_Type
- then
- if Nkind (Obj) = N_Selected_Component then
- Obj := Selector_Name (Obj);
- else
- Obj := Original_Node (Prefix (Obj));
+ if Ekind (Etype (Original_Node (Prefix (Obj))))
+ in E_Access_Type ..
+ E_Access_Protected_Subprogram_Type
+ then
+ if Nkind (Obj) = N_Selected_Component then
+ Obj := Selector_Name (Obj);
+ else
+ Obj := Original_Node (Prefix (Obj));
+ end if;
+ exit;
end if;
- exit;
+
+ Obj := Original_Node (Prefix (Obj));
+ end loop;
+
+ if Nkind (Obj) = N_Selected_Component then
+ Obj := Selector_Name (Obj);
end if;
- Obj := Original_Node (Prefix (Obj));
- end loop;
+ -- Check for renamings
- if Nkind (Obj) = N_Selected_Component then
- Obj := Selector_Name (Obj);
- end if;
+ pragma Assert (Is_Entity_Name (Obj));
+
+ if Present (Renamed_Object (Entity (Obj))) then
+ Obj := Renamed_Object (Entity (Obj));
+ else
+ exit;
+ end if;
+ end loop;
-- Do not check aliased formals or function calls. A
-- run-time check may still be needed ???
- pragma Assert (Is_Entity_Name (Obj));
-
if Is_Formal (Entity (Obj))
and then Is_Aliased (Entity (Obj))
then
end if;
end Is_SPARK_05_Object_Reference;
+ --------------------------------------
+ -- Is_Special_Aliased_Formal_Access --
+ --------------------------------------
+
+ function Is_Special_Aliased_Formal_Access
+ (Exp : Node_Id;
+ Scop : Entity_Id) return Boolean is
+ begin
+ -- Verify the expression is an access reference to 'Access within a
+ -- return statement as this is the only time an explicitly aliased
+ -- formal has different semantics.
+
+ if Nkind (Exp) /= N_Attribute_Reference
+ or else Get_Attribute_Id (Attribute_Name (Exp)) /= Attribute_Access
+ or else Nkind (Parent (Exp)) /= N_Simple_Return_Statement
+ then
+ return False;
+ end if;
+
+ -- Check if the prefix of the reference is indeed an explicitly aliased
+ -- formal parameter for the function Scop. Additionally, we must check
+ -- that Scop returns an anonymous access type, otherwise the special
+ -- rules dictating a need for a dynamic check are not in effect.
+
+ declare
+ P_Ult : constant Node_Id := Ultimate_Prefix (Prefix (Exp));
+ begin
+ return Is_Entity_Name (P_Ult)
+ and then Is_Aliased (Entity (P_Ult))
+ and then Is_Formal (Entity (P_Ult))
+ and then Scope (Entity (P_Ult)) = Scop
+ and then Ekind_In (Scop, E_Function,
+ E_Operator,
+ E_Subprogram_Type)
+ and then Present (Extra_Accessibility_Of_Result (Scop));
+ end;
+ end Is_Special_Aliased_Formal_Access;
+
-----------------------------
-- Is_Specific_Tagged_Type --
-----------------------------
return Type_Access_Level (Scope (E)) + 1;
else
- -- Aliased formals of functions take their access level from the
- -- point of call, i.e. require a dynamic check. For static check
- -- purposes, this is smaller than the level of the subprogram
- -- itself. For procedures the aliased makes no difference.
-
- if Is_Formal (E)
- and then Is_Aliased (E)
- and then Ekind (Scope (E)) = E_Function
- then
- return Type_Access_Level (Etype (E));
-
- else
- return Scope_Depth (Enclosing_Dynamic_Scope (E));
- end if;
+ return Scope_Depth (Enclosing_Dynamic_Scope (E));
end if;
elsif Nkind_In (Obj, N_Indexed_Component, N_Selected_Component) then
-- constants, formal parameters, and selected_components of those are
-- valid objects in SPARK 2005.
+ function Is_Special_Aliased_Formal_Access
+ (Exp : Node_Id;
+ Scop : Entity_Id) return Boolean;
+ -- Determines whether a dynamic check must be generated for explicitly
+ -- aliased formals within a function Scop for the expression Exp.
+
+ -- More specially, Is_Special_Aliased_Formal_Access checks that Exp is a
+ -- 'Access attribute reference within a return statement where the ultimate
+ -- prefix is an aliased formal of Scop and that Scop returns an anonymous
+ -- access type. See RM 3.10.2 for more details.
+
function Is_Specific_Tagged_Type (Typ : Entity_Id) return Boolean;
-- Determine whether an arbitrary [private] type is specifically tagged