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-2020, 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, task unit, or type denoted by Id. 37 -- The following are valid pragmas: 38 -- 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 -- No_Caching 54 -- Part_Of 55 -- Postcondition 56 -- Precondition 57 -- Refined_Depends 58 -- Refined_Global 59 -- Refined_Post 60 -- Refined_States 61 -- Test_Case 62 -- Volatile_Function 63 64 procedure Analyze_Contracts (L : List_Id); 65 -- Analyze the contracts of all eligible constructs found in list L 66 67 procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id); 68 -- Analyze all delayed pragmas chained on the contract of entry or 69 -- subprogram body Body_Id as if they appeared at the end of a declarative 70 -- region. Pragmas in question are: 71 -- 72 -- Contract_Cases (stand alone subprogram body) 73 -- Depends (stand alone subprogram body) 74 -- Global (stand alone subprogram body) 75 -- Postcondition (stand alone subprogram body) 76 -- Precondition (stand alone subprogram body) 77 -- Refined_Depends 78 -- Refined_Global 79 -- Refined_Post 80 -- Subprogram_Variant (stand alone subprogram body) 81 -- Test_Case (stand alone subprogram body) 82 83 procedure Analyze_Entry_Or_Subprogram_Contract 84 (Subp_Id : Entity_Id; 85 Freeze_Id : Entity_Id := Empty); 86 -- Analyze all delayed pragmas chained on the contract of entry or 87 -- subprogram Subp_Id as if they appeared at the end of a declarative 88 -- region. The pragmas in question are: 89 -- 90 -- Contract_Cases 91 -- Depends 92 -- Global 93 -- Postcondition 94 -- Precondition 95 -- Subprogram_Variant 96 -- Test_Case 97 -- 98 -- Freeze_Id is the entity of a [generic] package body or a [generic] 99 -- subprogram body which "freezes" the contract of Subp_Id. 100 101 procedure Analyze_Object_Contract 102 (Obj_Id : Entity_Id; 103 Freeze_Id : Entity_Id := Empty); 104 -- Analyze all delayed pragmas chained on the contract of object Obj_Id as 105 -- if they appeared at the end of the declarative region. The pragmas to be 106 -- considered are: 107 -- 108 -- Async_Readers 109 -- Async_Writers 110 -- Depends (single concurrent object) 111 -- Effective_Reads 112 -- Effective_Writes 113 -- Global (single concurrent object) 114 -- Part_Of 115 -- 116 -- Freeze_Id is the entity of a [generic] package body or a [generic] 117 -- subprogram body which "freezes" the contract of Obj_Id. 118 119 procedure Analyze_Type_Contract (Type_Id : Entity_Id); 120 -- Analyze all delayed pragmas chained on the contract of object Obj_Id as 121 -- if they appeared at the end of the declarative region. The pragmas to be 122 -- considered are: 123 -- 124 -- Async_Readers 125 -- Async_Writers 126 -- Effective_Reads 127 -- Effective_Writes 128 -- 129 -- In the case of a protected or task type, there will also be 130 -- a call to Analyze_Protected_Contract or Analyze_Task_Contract. 131 132 procedure Analyze_Package_Body_Contract 133 (Body_Id : Entity_Id; 134 Freeze_Id : Entity_Id := Empty); 135 -- Analyze all delayed pragmas chained on the contract of package body 136 -- Body_Id as if they appeared at the end of a declarative region. The 137 -- pragmas that are considered are: 138 -- 139 -- Refined_State 140 -- 141 -- Freeze_Id is the entity of a [generic] package body or a [generic] 142 -- subprogram body which "freezes" the contract of Body_Id. 143 144 procedure Analyze_Package_Contract (Pack_Id : Entity_Id); 145 -- Analyze all delayed pragmas chained on the contract of package Pack_Id 146 -- as if they appeared at the end of a declarative region. The pragmas 147 -- that are considered are: 148 -- 149 -- Initial_Condition 150 -- Initializes 151 152 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id); 153 -- Analyze all delayed pragmas chained on the contract of protected unit 154 -- Prot_Id if they appeared at the end of a declarative region. Currently 155 -- there are no such pragmas. 156 157 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id); 158 -- Analyze all delayed pragmas chained on the contract of subprogram body 159 -- stub Stub_Id as if they appeared at the end of a declarative region. The 160 -- pragmas in question are: 161 -- 162 -- Contract_Cases 163 -- Depends 164 -- Global 165 -- Postcondition 166 -- Precondition 167 -- Refined_Depends 168 -- Refined_Global 169 -- Refined_Post 170 -- Test_Case 171 172 procedure Analyze_Task_Contract (Task_Id : Entity_Id); 173 -- Analyze all delayed pragmas chained on the contract of task unit Task_Id 174 -- as if they appeared at the end of a declarative region. The pragmas in 175 -- question are: 176 -- 177 -- Depends 178 -- Global 179 180 procedure Create_Generic_Contract (Unit : Node_Id); 181 -- Create a contract node for a generic package, generic subprogram, or a 182 -- generic body denoted by Unit by collecting all source contract-related 183 -- pragmas in the contract of the unit. 184 185 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id); 186 -- Freeze the contracts of all source constructs found in the declarative 187 -- list which contains entry, package, protected, subprogram, or task body 188 -- denoted by Body_Decl. In addition, freeze the contract of the nearest 189 -- enclosing package body. 190 191 function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id; 192 -- Get the defining identifier for a subprogram's Postcond_Enabled 193 -- object created during the expansion of the subprogram's postconditions. 194 195 function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id; 196 -- Get the defining identifier for a subprogram's 197 -- Result_Object_For_Postcond object created during the expansion of the 198 -- subprogram's postconditions. 199 200 function Get_Return_Success_For_Postcond 201 (Subp : Entity_Id) return Entity_Id; 202 -- Get the defining identifier for a subprogram's 203 -- Return_Success_For_Postcond object created during the expansion of the 204 -- subprogram's postconditions. 205 206 procedure Inherit_Subprogram_Contract 207 (Subp : Entity_Id; 208 From_Subp : Entity_Id); 209 -- Inherit relevant contract items from source subprogram From_Subp. Subp 210 -- denotes the destination subprogram. The inherited items are: 211 -- Extensions_Visible 212 -- ??? it would be nice if this routine handles Pre'Class and Post'Class 213 214 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id); 215 -- Instantiate all source pragmas found in the contract of the generic 216 -- subprogram declaration template denoted by Templ. The instantiated 217 -- pragmas are added to list L. 218 219 procedure Save_Global_References_In_Contract 220 (Templ : Node_Id; 221 Gen_Id : Entity_Id); 222 -- Save all global references found within the aspect specifications and 223 -- the contract-related source pragmas assocated with generic template 224 -- Templ. Gen_Id denotes the entity of the analyzed generic copy. 225 226end Contracts; 227