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