-- The four volatility refinement pragmas are ok for all types.
-- Part_Of is ok for task types and protected types.
-- Depends and Global are ok for task types.
+ --
+ -- Precondition and Postcondition are added separately; they are allowed
+ -- for access-to-subprogram types.
elsif Is_Type (Id) then
declare
- Is_OK : constant Boolean :=
+ Is_OK_Classification : constant Boolean :=
Prag_Nam in Name_Async_Readers
| Name_Async_Writers
| Name_Effective_Reads
| Name_Global)
or else (Ekind (Id) = E_Protected_Type
and Prag_Nam = Name_Part_Of);
+
begin
- if Is_OK then
+ if Is_OK_Classification then
Add_Classification;
+
+ elsif Ekind (Id) in Access_Subprogram_Kind
+ and then Prag_Nam in Name_Precondition
+ | Name_Postcondition
+ then
+ Add_Pre_Post_Condition;
else
-- The pragma is not a proper contract item
begin
Check_Type_Or_Object_External_Properties
(Type_Or_Obj_Id => Type_Id);
+
+ -- Analyze Pre/Post on access-to-subprogram type
+
+ if Is_Access_Subprogram_Type (Type_Id) then
+ Analyze_Entry_Or_Subprogram_Contract (Type_Id);
+ end if;
end Analyze_Type_Contract;
---------------------------------------
-- Async_Writers
-- Effective_Reads
-- Effective_Writes
+ -- Postcondition
+ -- Precondition
--
-- In the case of a protected or task type, there will also be
-- a call to Analyze_Protected_Contract or Analyze_Task_Contract.
elsif Nkind (Subp_Decl) not in N_Abstract_Subprogram_Declaration
| N_Entry_Declaration
| N_Expression_Function
+ | N_Full_Type_Declaration
| N_Generic_Subprogram_Declaration
| N_Subprogram_Body
| N_Subprogram_Body_Stub
("incorrect prefix for attribute %, expected %", P);
end if;
+ -- If the prefix is an access-to-subprogram type, then it must
+ -- be the same as the annotated type.
+
+ elsif Is_Access_Subprogram_Type (Pref_Id) then
+ if Pref_Id = Spec_Id then
+ Set_Etype (N, Etype (Designated_Type (Spec_Id)));
+ else
+ Error_Msg_Name_2 := Chars (Spec_Id);
+ Error_Attr
+ ("incorrect prefix for attribute %, expected %", P);
+ end if;
+
-- Otherwise the prefix denotes some other form of subprogram
-- entity.
declare
Asp : Node_Id;
A_Id : Aspect_Id;
- Cond : Node_Id;
- Expr : Node_Id;
begin
Asp := First (Aspect_Specifications (Decl));
while Present (Asp) loop
A_Id := Get_Aspect_Id (Chars (Identifier (Asp)));
if A_Id = Aspect_Pre or else A_Id = Aspect_Post then
- Cond := Asp;
- Expr := Expression (Cond);
- Replace_Type_Name (Expr);
- Next (Asp);
-
- Remove (Cond);
- Append (Cond, Contracts);
-
- else
- Next (Asp);
+ Append (New_Copy_Tree (Asp), Contracts);
+ Replace_Type_Name (Expression (Last (Contracts)));
end if;
+ Next (Asp);
end loop;
end;
then
null;
- -- An access-to-subprogram type can have pre/postconditions, but
- -- these are transferred to the generated subprogram wrapper and
- -- analyzed there.
+ -- An access-to-subprogram type can have pre/postconditions, which
+ -- are both analyzed when attached to the type and copied to the
+ -- generated subprogram wrapper and analyzed there.
+
+ elsif Nkind (Subp_Decl) = N_Full_Type_Declaration
+ and then Nkind (Type_Definition (Subp_Decl)) in
+ N_Access_To_Subprogram_Definition
+ then
+ if Ada_Version < Ada_2022 then
+ Error_Msg_Ada_2022_Feature
+ ("pre/postcondition access-to-subprogram", Loc);
+ raise Pragma_Exit;
+ end if;
-- Otherwise the placement of the pragma is illegal
if not In_Open_Scopes (Spec_Id) then
Restore_Scope := True;
- Push_Scope (Spec_Id);
if Is_Generic_Subprogram (Spec_Id) then
+ Push_Scope (Spec_Id);
Install_Generic_Formals (Spec_Id);
+ elsif Is_Access_Subprogram_Type (Spec_Id) then
+ Push_Scope (Designated_Type (Spec_Id));
+ Install_Formals (Designated_Type (Spec_Id));
else
+ Push_Scope (Spec_Id);
Install_Formals (Spec_Id);
end if;
end if;