[thirdparty/gcc.git] / gcc / ada / contracts.ads

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                            C O N T R A C T S                             --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 2015-2019, Free Software Foundation, Inc.         --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

--  This package contains routines that perform analysis and expansion of
--  various contracts.

with Types; use Types;

package Contracts is

   procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
   --  Add pragma Prag to the contract of a constant, entry, entry family,
   --  [generic] package, package body, protected unit, [generic] subprogram,
   --  subprogram body, variable or task unit denoted by Id. The following are
   --  valid pragmas:
   --
   --    Abstract_State
   --    Async_Readers
   --    Async_Writers
   --    Attach_Handler
   --    Constant_After_Elaboration
   --    Contract_Cases
   --    Depends
   --    Effective_Reads
   --    Effective_Writes
   --    Extensions_Visible
   --    Global
   --    Initial_Condition
   --    Initializes
   --    Interrupt_Handler
   --    No_Caching
   --    Part_Of
   --    Postcondition
   --    Precondition
   --    Refined_Depends
   --    Refined_Global
   --    Refined_Post
   --    Refined_States
   --    Test_Case
   --    Volatile_Function

   procedure Analyze_Contracts (L : List_Id);
   --  Analyze the contracts of all eligible constructs found in list L

   procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
   --  Analyze all delayed pragmas chained on the contract of entry or
   --  subprogram body Body_Id as if they appeared at the end of a declarative
   --  region. Pragmas in question are:
   --
   --    Contract_Cases   (stand alone subprogram body)
   --    Depends          (stand alone subprogram body)
   --    Global           (stand alone subprogram body)
   --    Postcondition    (stand alone subprogram body)
   --    Precondition     (stand alone subprogram body)
   --    Refined_Depends
   --    Refined_Global
   --    Refined_Post
   --    Test_Case        (stand alone subprogram body)

   procedure Analyze_Entry_Or_Subprogram_Contract
     (Subp_Id   : Entity_Id;
      Freeze_Id : Entity_Id := Empty);
   --  Analyze all delayed pragmas chained on the contract of entry or
   --  subprogram Subp_Id as if they appeared at the end of a declarative
   --  region. The pragmas in question are:
   --
   --    Contract_Cases
   --    Depends
   --    Global
   --    Postcondition
   --    Precondition
   --    Test_Case
   --
   --  Freeze_Id is the entity of a [generic] package body or a [generic]
   --  subprogram body which "freezes" the contract of Subp_Id.

   procedure Analyze_Object_Contract
     (Obj_Id    : Entity_Id;
      Freeze_Id : Entity_Id := Empty);
   --  Analyze all delayed pragmas chained on the contract of object Obj_Id as
   --  if they appeared at the end of the declarative region. The pragmas to be
   --  considered are:
   --
   --    Async_Readers
   --    Async_Writers
   --    Depends           (single concurrent object)
   --    Effective_Reads
   --    Effective_Writes
   --    Global            (single concurrent object)
   --    Part_Of
   --
   --  Freeze_Id is the entity of a [generic] package body or a [generic]
   --  subprogram body which "freezes" the contract of Obj_Id.

   procedure Analyze_Package_Body_Contract
     (Body_Id   : Entity_Id;
      Freeze_Id : Entity_Id := Empty);
   --  Analyze all delayed pragmas chained on the contract of package body
   --  Body_Id as if they appeared at the end of a declarative region. The
   --  pragmas that are considered are:
   --
   --    Refined_State
   --
   --  Freeze_Id is the entity of a [generic] package body or a [generic]
   --  subprogram body which "freezes" the contract of Body_Id.

   procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
   --  Analyze all delayed pragmas chained on the contract of package Pack_Id
   --  as if they appeared at the end of a declarative region. The pragmas
   --  that are considered are:
   --
   --    Initial_Condition
   --    Initializes

   procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
   --  Analyze all delayed pragmas chained on the contract of protected unit
   --  Prot_Id if they appeared at the end of a declarative region. Currently
   --  there are no such pragmas.

   procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
   --  Analyze all delayed pragmas chained on the contract of subprogram body
   --  stub Stub_Id as if they appeared at the end of a declarative region. The
   --  pragmas in question are:
   --
   --    Contract_Cases
   --    Depends
   --    Global
   --    Postcondition
   --    Precondition
   --    Refined_Depends
   --    Refined_Global
   --    Refined_Post
   --    Test_Case

   procedure Analyze_Task_Contract (Task_Id : Entity_Id);
   --  Analyze all delayed pragmas chained on the contract of task unit Task_Id
   --  as if they appeared at the end of a declarative region. The pragmas in
   --  question are:
   --
   --    Depends
   --    Global

   procedure Create_Generic_Contract (Unit : Node_Id);
   --  Create a contract node for a generic package, generic subprogram, or a
   --  generic body denoted by Unit by collecting all source contract-related
   --  pragmas in the contract of the unit.

   procedure Freeze_Previous_Contracts (Body_Decl : Node_Id);
   --  Freeze the contracts of all source constructs found in the declarative
   --  list which contains entry, package, protected, subprogram, or task body
   --  denoted by Body_Decl. In addition, freeze the contract of the nearest
   --  enclosing package body.

   procedure Inherit_Subprogram_Contract
     (Subp      : Entity_Id;
      From_Subp : Entity_Id);
   --  Inherit relevant contract items from source subprogram From_Subp. Subp
   --  denotes the destination subprogram. The inherited items are:
   --    Extensions_Visible
   --  ??? it would be nice if this routine handles Pre'Class and Post'Class

   procedure Instantiate_Subprogram_Contract (Templ : Node_Id; L : List_Id);
   --  Instantiate all source pragmas found in the contract of the generic
   --  subprogram declaration template denoted by Templ. The instantiated
   --  pragmas are added to list L.

   procedure Save_Global_References_In_Contract
     (Templ  : Node_Id;
      Gen_Id : Entity_Id);
   --  Save all global references found within the aspect specifications and
   --  the contract-related source pragmas assocated with generic template
   --  Templ. Gen_Id denotes the entity of the analyzed generic copy.

end Contracts;
Commit	Line	Data
879ac954 AC	1	------------------------------------------------------------------------------
	2	-- --
	3	-- GNAT COMPILER COMPONENTS --
	4	-- --
	5	-- C O N T R A C T S --
	6	-- --
	7	-- S p e c --
	8	-- --
1d005acc	9	-- Copyright (C) 2015-2019, Free Software Foundation, Inc. --
879ac954 AC	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
	29	with Types; use Types;
	30
	31	package Contracts is
	32
	33	procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
f99ff327	34	-- Add pragma Prag to the contract of a constant, entry, entry family,
75b87c16 AC	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:
96e4fda5	38	--
879ac954 AC	39	-- Abstract_State
	40	-- Async_Readers
	41	-- Async_Writers
c0dd5b38	42	-- Attach_Handler
879ac954 AC	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
c0dd5b38	52	-- Interrupt_Handler
9dfc6c55	53	-- No_Caching
879ac954 AC	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
e645cb39 AC	64	procedure Analyze_Contracts (L : List_Id);
e645cb39 AC	65	-- Analyze the contracts of all eligible constructs found in list L
879ac954	66
f99ff327 AC	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:
96e4fda5	71	--
f99ff327 AC	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
e645cb39 AC	82	procedure Analyze_Entry_Or_Subprogram_Contract
	83	(Subp_Id : Entity_Id;
	84	Freeze_Id : Entity_Id := Empty);
f99ff327 AC	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:
96e4fda5	88	--
f99ff327 AC	89	-- Contract_Cases
	90	-- Depends
	91	-- Global
	92	-- Postcondition
	93	-- Precondition
	94	-- Test_Case
e645cb39 AC	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.
f99ff327	98
e645cb39 AC	99	procedure Analyze_Object_Contract
	100	(Obj_Id : Entity_Id;
	101	Freeze_Id : Entity_Id := Empty);
879ac954 AC	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:
96e4fda5	105	--
879ac954 AC	106	-- Async_Readers
879ac954 AC	107	-- Async_Writers
75b87c16	108	-- Depends (single concurrent object)
879ac954 AC	109	-- Effective_Reads
879ac954 AC	110	-- Effective_Writes
75b87c16	111	-- Global (single concurrent object)
879ac954	112	-- Part_Of
e645cb39 AC	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.
879ac954 AC	116
	117	procedure Analyze_Package_Body_Contract
	118	(Body_Id : Entity_Id;
	119	Freeze_Id : Entity_Id := Empty);
f99ff327	120	-- Analyze all delayed pragmas chained on the contract of package body
879ac954	121	-- Body_Id as if they appeared at the end of a declarative region. The
f99ff327	122	-- pragmas that are considered are:
96e4fda5	123	--
879ac954 AC	124	-- Refined_State
	125	--
	126	-- Freeze_Id is the entity of a [generic] package body or a [generic]
e96b7045	127	-- subprogram body which "freezes" the contract of Body_Id.
879ac954 AC	128
879ac954 AC	129	procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
f99ff327 AC	130	-- Analyze all delayed pragmas chained on the contract of package Pack_Id
f99ff327 AC	131	-- as if they appeared at the end of a declarative region. The pragmas
879ac954	132	-- that are considered are:
96e4fda5	133	--
879ac954 AC	134	-- Initial_Condition
879ac954 AC	135	-- Initializes
879ac954	136
75b87c16 AC	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
879ac954	142	procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
75b87c16	143	-- Analyze all delayed pragmas chained on the contract of subprogram body
879ac954	144	-- stub Stub_Id as if they appeared at the end of a declarative region. The
f99ff327	145	-- pragmas in question are:
96e4fda5	146	--
879ac954 AC	147	-- Contract_Cases
	148	-- Depends
	149	-- Global
	150	-- Postcondition
	151	-- Precondition
	152	-- Refined_Depends
	153	-- Refined_Global
	154	-- Refined_Post
	155	-- Test_Case
	156
f99ff327	157	procedure Analyze_Task_Contract (Task_Id : Entity_Id);
75b87c16 AC	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:
96e4fda5	161	--
f99ff327 AC	162	-- Depends
	163	-- Global
	164
879ac954	165	procedure Create_Generic_Contract (Unit : Node_Id);
e96b7045	166	-- Create a contract node for a generic package, generic subprogram, or a
879ac954 AC	167	-- generic body denoted by Unit by collecting all source contract-related
	168	-- pragmas in the contract of the unit.
	169
65e5747e PMR	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
879ac954 AC	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
	196	end Contracts;