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-2019, 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 -- 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 -- Test_Case (stand alone subprogram body) 81 82 procedure Analyze_Entry_Or_Subprogram_Contract 83 (Subp_Id : Entity_Id; 84 Freeze_Id : Entity_Id := Empty); 85 -- Analyze all delayed pragmas chained on the contract of entry or 86 -- subprogram Subp_Id as if they appeared at the end of a declarative 87 -- region. The pragmas in question are: 88 -- 89 -- Contract_Cases 90 -- Depends 91 -- Global 92 -- Postcondition 93 -- Precondition 94 -- Test_Case 95 -- 96 -- Freeze_Id is the entity of a [generic] package body or a [generic] 97 -- subprogram body which "freezes" the contract of Subp_Id. 98 99 procedure Analyze_Object_Contract 100 (Obj_Id : Entity_Id; 101 Freeze_Id : Entity_Id := Empty); 102 -- Analyze all delayed pragmas chained on the contract of object Obj_Id as 103 -- if they appeared at the end of the declarative region. The pragmas to be 104 -- considered are: 105 -- 106 -- Async_Readers 107 -- Async_Writers 108 -- Depends (single concurrent object) 109 -- Effective_Reads 110 -- Effective_Writes 111 -- Global (single concurrent object) 112 -- Part_Of 113 -- 114 -- Freeze_Id is the entity of a [generic] package body or a [generic] 115 -- subprogram body which "freezes" the contract of Obj_Id. 116 117 procedure Analyze_Package_Body_Contract 118 (Body_Id : Entity_Id; 119 Freeze_Id : Entity_Id := Empty); 120 -- Analyze all delayed pragmas chained on the contract of package body 121 -- Body_Id as if they appeared at the end of a declarative region. The 122 -- pragmas that are considered are: 123 -- 124 -- Refined_State 125 -- 126 -- Freeze_Id is the entity of a [generic] package body or a [generic] 127 -- subprogram body which "freezes" the contract of Body_Id. 128 129 procedure Analyze_Package_Contract (Pack_Id : Entity_Id); 130 -- Analyze all delayed pragmas chained on the contract of package Pack_Id 131 -- as if they appeared at the end of a declarative region. The pragmas 132 -- that are considered are: 133 -- 134 -- Initial_Condition 135 -- Initializes 136 137 procedure Analyze_Protected_Contract (Prot_Id : Entity_Id); 138 -- Analyze all delayed pragmas chained on the contract of protected unit 139 -- Prot_Id if they appeared at the end of a declarative region. Currently 140 -- there are no such pragmas. 141 142 procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id); 143 -- Analyze all delayed pragmas chained on the contract of subprogram body 144 -- stub Stub_Id as if they appeared at the end of a declarative region. The 145 -- pragmas in question are: 146 -- 147 -- Contract_Cases 148 -- Depends 149 -- Global 150 -- Postcondition 151 -- Precondition 152 -- Refined_Depends 153 -- Refined_Global 154 -- Refined_Post 155 -- Test_Case 156 157 procedure Analyze_Task_Contract (Task_Id : Entity_Id); 158 -- Analyze all delayed pragmas chained on the contract of task unit Task_Id 159 -- as if they appeared at the end of a declarative region. The pragmas in 160 -- question are: 161 -- 162 -- Depends 163 -- Global 164 165 procedure Create_Generic_Contract (Unit : Node_Id); 166 -- Create a contract node for a generic package, generic subprogram, or a 167 -- generic body denoted by Unit by collecting all source contract-related 168 -- pragmas in the contract of the unit. 169 170 procedure Freeze_Previous_Contracts (Body_Decl : Node_Id); 171 -- Freeze the contracts of all source constructs found in the declarative 172 -- list which contains entry, package, protected, subprogram, or task body 173 -- denoted by Body_Decl. In addition, freeze the contract of the nearest 174 -- enclosing package body. 175 176 procedure Inherit_Subprogram_Contract 177 (Subp : Entity_Id; 178 From_Subp : Entity_Id); 179 -- Inherit relevant contract items from source subprogram From_Subp. Subp 180 -- denotes the destination subprogram. The inherited items are: 181 -- Extensions_Visible 182 -- ??? it would be nice if this routine handles Pre'Class and Post'Class 183 184 procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id); 185 -- Instantiate all source pragmas found in the contract of the generic 186 -- subprogram declaration template denoted by Templ. The instantiated 187 -- pragmas are added to list L. 188 189 procedure Save_Global_References_In_Contract 190 (Templ : Node_Id; 191 Gen_Id : Entity_Id); 192 -- Save all global references found within the aspect specifications and 193 -- the contract-related source pragmas assocated with generic template 194 -- Templ. Gen_Id denotes the entity of the analyzed generic copy. 195 196end Contracts; 197