|
111
|
1 ------------------------------------------------------------------------------
|
|
|
2 -- --
|
|
|
3 -- GNAT COMPILER COMPONENTS --
|
|
|
4 -- --
|
|
|
5 -- C O N T R A C T S --
|
|
|
6 -- --
|
|
|
7 -- S p e c --
|
|
|
8 -- --
|
|
131
|
9 -- Copyright (C) 2015-2018, Free Software Foundation, Inc. --
|
|
111
|
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:
|
|
131
|
38 --
|
|
111
|
39 -- Abstract_State
|
|
|
40 -- Async_Readers
|
|
|
41 -- Async_Writers
|
|
|
42 -- Attach_Handler
|
|
|
43 -- Constant_After_Elaboration
|
|
|
44 -- Contract_Cases
|
|
|
45 -- Depends
|
|
|
46 -- Effective_Reads
|
|
|
47 -- Effective_Writes
|
|
|
48 -- Extensions_Visible
|
|
|
49 -- Global
|
|
|
50 -- Initial_Condition
|
|
|
51 -- Initializes
|
|
|
52 -- Interrupt_Handler
|
|
|
53 -- Part_Of
|
|
|
54 -- Postcondition
|
|
|
55 -- Precondition
|
|
|
56 -- Refined_Depends
|
|
|
57 -- Refined_Global
|
|
|
58 -- Refined_Post
|
|
|
59 -- Refined_States
|
|
|
60 -- Test_Case
|
|
|
61 -- Volatile_Function
|
|
|
62
|
|
|
63 procedure Analyze_Contracts (L : List_Id);
|
|
|
64 -- Analyze the contracts of all eligible constructs found in list L
|
|
|
65
|
|
|
66 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
|
|
|
67 -- Analyze all delayed pragmas chained on the contract of entry or
|
|
|
68 -- subprogram body Body_Id as if they appeared at the end of a declarative
|
|
|
69 -- region. Pragmas in question are:
|
|
131
|
70 --
|
|
111
|
71 -- Contract_Cases (stand alone subprogram body)
|
|
|
72 -- Depends (stand alone subprogram body)
|
|
|
73 -- Global (stand alone subprogram body)
|
|
|
74 -- Postcondition (stand alone subprogram body)
|
|
|
75 -- Precondition (stand alone subprogram body)
|
|
|
76 -- Refined_Depends
|
|
|
77 -- Refined_Global
|
|
|
78 -- Refined_Post
|
|
|
79 -- Test_Case (stand alone subprogram body)
|
|
|
80
|
|
|
81 procedure Analyze_Entry_Or_Subprogram_Contract
|
|
|
82 (Subp_Id : Entity_Id;
|
|
|
83 Freeze_Id : Entity_Id := Empty);
|
|
|
84 -- Analyze all delayed pragmas chained on the contract of entry or
|
|
|
85 -- subprogram Subp_Id as if they appeared at the end of a declarative
|
|
|
86 -- region. The pragmas in question are:
|
|
131
|
87 --
|
|
111
|
88 -- Contract_Cases
|
|
|
89 -- Depends
|
|
|
90 -- Global
|
|
|
91 -- Postcondition
|
|
|
92 -- Precondition
|
|
|
93 -- Test_Case
|
|
|
94 --
|
|
|
95 -- Freeze_Id is the entity of a [generic] package body or a [generic]
|
|
|
96 -- subprogram body which "freezes" the contract of Subp_Id.
|
|
|
97
|
|
|
98 procedure Analyze_Object_Contract
|
|
|
99 (Obj_Id : Entity_Id;
|
|
|
100 Freeze_Id : Entity_Id := Empty);
|
|
|
101 -- Analyze all delayed pragmas chained on the contract of object Obj_Id as
|
|
|
102 -- if they appeared at the end of the declarative region. The pragmas to be
|
|
|
103 -- considered are:
|
|
131
|
104 --
|
|
111
|
105 -- Async_Readers
|
|
|
106 -- Async_Writers
|
|
|
107 -- Depends (single concurrent object)
|
|
|
108 -- Effective_Reads
|
|
|
109 -- Effective_Writes
|
|
|
110 -- Global (single concurrent object)
|
|
|
111 -- Part_Of
|
|
|
112 --
|
|
|
113 -- Freeze_Id is the entity of a [generic] package body or a [generic]
|
|
|
114 -- subprogram body which "freezes" the contract of Obj_Id.
|
|
|
115
|
|
|
116 procedure Analyze_Package_Body_Contract
|
|
|
117 (Body_Id : Entity_Id;
|
|
|
118 Freeze_Id : Entity_Id := Empty);
|
|
|
119 -- Analyze all delayed pragmas chained on the contract of package body
|
|
|
120 -- Body_Id as if they appeared at the end of a declarative region. The
|
|
|
121 -- pragmas that are considered are:
|
|
131
|
122 --
|
|
111
|
123 -- Refined_State
|
|
|
124 --
|
|
|
125 -- Freeze_Id is the entity of a [generic] package body or a [generic]
|
|
|
126 -- subprogram body which "freezes" the contract of Body_Id.
|
|
|
127
|
|
|
128 procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
|
|
|
129 -- Analyze all delayed pragmas chained on the contract of package Pack_Id
|
|
|
130 -- as if they appeared at the end of a declarative region. The pragmas
|
|
|
131 -- that are considered are:
|
|
131
|
132 --
|
|
111
|
133 -- Initial_Condition
|
|
|
134 -- Initializes
|
|
|
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:
|
|
131
|
145 --
|
|
111
|
146 -- Contract_Cases
|
|
|
147 -- Depends
|
|
|
148 -- Global
|
|
|
149 -- Postcondition
|
|
|
150 -- Precondition
|
|
|
151 -- Refined_Depends
|
|
|
152 -- Refined_Global
|
|
|
153 -- Refined_Post
|
|
|
154 -- Test_Case
|
|
|
155
|
|
|
156 procedure Analyze_Task_Contract (Task_Id : Entity_Id);
|
|
|
157 -- Analyze all delayed pragmas chained on the contract of task unit Task_Id
|
|
|
158 -- as if they appeared at the end of a declarative region. The pragmas in
|
|
|
159 -- question are:
|
|
131
|
160 --
|
|
111
|
161 -- Depends
|
|
|
162 -- Global
|
|
|
163
|
|
|
164 procedure Create_Generic_Contract (Unit : Node_Id);
|
|
|
165 -- Create a contract node for a generic package, generic subprogram, or a
|
|
|
166 -- generic body denoted by Unit by collecting all source contract-related
|
|
|
167 -- pragmas in the contract of the unit.
|
|
|
168
|
|
131
|
169 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id);
|
|
|
170 -- Freeze the contracts of all source constructs found in the declarative
|
|
|
171 -- list which contains entry, package, protected, subprogram, or task body
|
|
|
172 -- denoted by Body_Decl. In addition, freeze the contract of the nearest
|
|
|
173 -- enclosing package body.
|
|
|
174
|
|
111
|
175 procedure Inherit_Subprogram_Contract
|
|
|
176 (Subp : Entity_Id;
|
|
|
177 From_Subp : Entity_Id);
|
|
|
178 -- Inherit relevant contract items from source subprogram From_Subp. Subp
|
|
|
179 -- denotes the destination subprogram. The inherited items are:
|
|
|
180 -- Extensions_Visible
|
|
|
181 -- ??? it would be nice if this routine handles Pre'Class and Post'Class
|
|
|
182
|
|
|
183 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id);
|
|
|
184 -- Instantiate all source pragmas found in the contract of the generic
|
|
|
185 -- subprogram declaration template denoted by Templ. The instantiated
|
|
|
186 -- pragmas are added to list L.
|
|
|
187
|
|
|
188 procedure Save_Global_References_In_Contract
|
|
|
189 (Templ : Node_Id;
|
|
|
190 Gen_Id : Entity_Id);
|
|
|
191 -- Save all global references found within the aspect specifications and
|
|
|
192 -- the contract-related source pragmas assocated with generic template
|
|
|
193 -- Templ. Gen_Id denotes the entity of the analyzed generic copy.
|
|
|
194
|
|
|
195 end Contracts;
|
