File : contracts.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- C O N T R A C T S --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2015, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
20 -- --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
23 -- --
24 ------------------------------------------------------------------------------
25
26 -- This package contains routines that perform analysis and expansion of
27 -- various contracts.
28
29 with Types; use Types;
30
31 package Contracts is
32
33 procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
34 -- Add pragma Prag to the contract of a constant, entry, entry family,
35 -- [generic] package, package body, protected unit, [generic] subprogram,
36 -- subprogram body, variable or task unit denoted by Id. The following are
37 -- valid pragmas:
38 -- Abstract_State
39 -- Async_Readers
40 -- Async_Writers
41 -- Attach_Handler
42 -- Constant_After_Elaboration
43 -- Contract_Cases
44 -- Depends
45 -- Effective_Reads
46 -- Effective_Writes
47 -- Extensions_Visible
48 -- Global
49 -- Initial_Condition
50 -- Initializes
51 -- Interrupt_Handler
52 -- Part_Of
53 -- Postcondition
54 -- Precondition
55 -- Refined_Depends
56 -- Refined_Global
57 -- Refined_Post
58 -- Refined_States
59 -- Test_Case
60 -- Volatile_Function
61
62 procedure Analyze_Contracts (L : List_Id);
63 -- Analyze the contracts of all eligible constructs found in list L
64
65 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
66 -- Analyze all delayed pragmas chained on the contract of entry or
67 -- subprogram body Body_Id as if they appeared at the end of a declarative
68 -- region. Pragmas in question are:
69 -- Contract_Cases (stand alone subprogram body)
70 -- Depends (stand alone subprogram body)
71 -- Global (stand alone subprogram body)
72 -- Postcondition (stand alone subprogram body)
73 -- Precondition (stand alone subprogram body)
74 -- Refined_Depends
75 -- Refined_Global
76 -- Refined_Post
77 -- Test_Case (stand alone subprogram body)
78
79 procedure Analyze_Entry_Or_Subprogram_Contract
80 (Subp_Id : Entity_Id;
81 Freeze_Id : Entity_Id := Empty);
82 -- Analyze all delayed pragmas chained on the contract of entry or
83 -- subprogram Subp_Id as if they appeared at the end of a declarative
84 -- region. The pragmas in question are:
85 -- Contract_Cases
86 -- Depends
87 -- Global
88 -- Postcondition
89 -- Precondition
90 -- Test_Case
91 --
92 -- Freeze_Id is the entity of a [generic] package body or a [generic]
93 -- subprogram body which "freezes" the contract of Subp_Id.
94
95 procedure Analyze_Object_Contract
96 (Obj_Id : Entity_Id;
97 Freeze_Id : Entity_Id := Empty);
98 -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
99 -- if they appeared at the end of the declarative region. The pragmas to be
100 -- considered are:
101 -- Async_Readers
102 -- Async_Writers
103 -- Depends (single concurrent object)
104 -- Effective_Reads
105 -- Effective_Writes
106 -- Global (single concurrent object)
107 -- Part_Of
108 --
109 -- Freeze_Id is the entity of a [generic] package body or a [generic]
110 -- subprogram body which "freezes" the contract of Obj_Id.
111
112 procedure Analyze_Package_Body_Contract
113 (Body_Id : Entity_Id;
114 Freeze_Id : Entity_Id := Empty);
115 -- Analyze all delayed pragmas chained on the contract of package body
116 -- Body_Id as if they appeared at the end of a declarative region. The
117 -- pragmas that are considered are:
118 -- Refined_State
119 --
120 -- Freeze_Id is the entity of a [generic] package body or a [generic]
121 -- subprogram body which "freezes" the contract of Body_Id.
122
123 procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
124 -- Analyze all delayed pragmas chained on the contract of package Pack_Id
125 -- as if they appeared at the end of a declarative region. The pragmas
126 -- that are considered are:
127 -- Initial_Condition
128 -- Initializes
129 -- Part_Of
130
131 procedure Analyze_Previous_Contracts (Body_Decl : Node_Id);
132 -- Analyze the contracts of all source constructs found in the declarative
133 -- list which contains entry, package, protected, subprogram, or task body
134 -- denoted by Body_Decl. The analysis stops once Body_Decl is reached.
135
136 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
137 -- Analyze all delayed pragmas chained on the contract of protected unit
138 -- Prot_Id if they appeared at the end of a declarative region. Currently
139 -- there are no such pragmas.
140
141 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
142 -- Analyze all delayed pragmas chained on the contract of subprogram body
143 -- stub Stub_Id as if they appeared at the end of a declarative region. The
144 -- pragmas in question are:
145 -- Contract_Cases
146 -- Depends
147 -- Global
148 -- Postcondition
149 -- Precondition
150 -- Refined_Depends
151 -- Refined_Global
152 -- Refined_Post
153 -- Test_Case
154
155 procedure Analyze_Task_Contract (Task_Id : Entity_Id);
156 -- Analyze all delayed pragmas chained on the contract of task unit Task_Id
157 -- as if they appeared at the end of a declarative region. The pragmas in
158 -- question are:
159 -- Depends
160 -- Global
161
162 procedure Create_Generic_Contract (Unit : Node_Id);
163 -- Create a contract node for a generic package, generic subprogram, or a
164 -- generic body denoted by Unit by collecting all source contract-related
165 -- pragmas in the contract of the unit.
166
167 procedure Inherit_Subprogram_Contract
168 (Subp : Entity_Id;
169 From_Subp : Entity_Id);
170 -- Inherit relevant contract items from source subprogram From_Subp. Subp
171 -- denotes the destination subprogram. The inherited items are:
172 -- Extensions_Visible
173 -- ??? it would be nice if this routine handles Pre'Class and Post'Class
174
175 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id);
176 -- Instantiate all source pragmas found in the contract of the generic
177 -- subprogram declaration template denoted by Templ. The instantiated
178 -- pragmas are added to list L.
179
180 procedure Save_Global_References_In_Contract
181 (Templ : Node_Id;
182 Gen_Id : Entity_Id);
183 -- Save all global references found within the aspect specifications and
184 -- the contract-related source pragmas assocated with generic template
185 -- Templ. Gen_Id denotes the entity of the analyzed generic copy.
186
187 end Contracts;