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
29with Types; use Types;
30
31package 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
187end Contracts;
188