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 -- 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: 70 -- 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: 87 -- 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: 104 -- 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: 122 -- 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: 132 -- 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: 145 -- 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: 160 -- 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 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 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 195end Contracts; 196