a1023434a8
gcc/ada/ * contracts.adb, contracts.ads (Build_Postconditions_Procedure): Add declarations for Postcond_Enabled, Result_Object_For_Postcondition, and Return_Success_For_Postcond, and place all postconditions within an if statement to control their execution for interactions when cleanup actions get generated. (Get_Postcond_Enabled): Created to fetch object declared to handle new expansion of postconditions. (Get_Result_Object_For_Postcond): Created to fetch object declared to handle new expansion of postconditions. (Get_Return_Success_For_Postcond): Created to fetch object declared to handle new expansion of postconditions. * einfo.adb, einfo.ads: Modify flag Stores_Attribute_Old_Prefix to apply to constants, variables, and types. * exp_ch6.adb (Add_Return): Add assignment to Return_Success_For_Postcond. (Expand_Non_Function_Return): Add assignment to Return_Success_For_Postcond (Expand_Simple_Function_Return): Add assignment to Result_Object_For_Postcond and Return_Success_For_Postcond. * exp_ch7.adb (Build_Finalization_Master): Mark finalization masters which finalize types created store 'Old objects as storing 'Old objects. (Build_Finalizer): Created to generated a unified and special expansion for finalization when postconditions are present. (Build_Finalizer_Helper): Renamed Build_Finalizer and added parameter to facilitate the creation of separate finalization routines for 'Old objects and general objects. (Create_Finalizer): Add condition for the insertion of the finalizer spec to avoid malformed trees. (Expand_Cleanup_Actions): Move _postconditions and related declarations to the new declarative section. Fix the loop to properly stop at the subprogram declaration for the postconditions procedure and exclude its body from being moved to the new list of declarations to avoid freezing issues. * exp_prag.adb (Expand_Attributes): Mark temporary created to store 'Old objects as storing a 'Old attribute. * sem_ch6.adb (Find_What_Applies_To): Remove strange exception to postconditions when traversing the scope stack. * sem_prag.adb (Find_Related_Declaration_Or_Body): Use the newly created Enclosing_HSS function to find the HSS for a potentially nested statement. * sem_util.adb, sem_util.ads (Declare_Indirect_Temp): Mark types created to store 'Old objects as storing 'Old attributes. (Enclosing_HSS): Created to find the enclosing handled sequence of statements for a given statement. * snames.ads-tmpl: Add multiple names to aid in the expansion of finalization and to control the evaluation of postconditions. Including _finalization_controller, a new routine to centralize finalization actions and postcondition evaluation.
227 lines
9.4 KiB
Ada
227 lines
9.4 KiB
Ada
------------------------------------------------------------------------------
|
|
-- --
|
|
-- GNAT COMPILER COMPONENTS --
|
|
-- --
|
|
-- C O N T R A C T S --
|
|
-- --
|
|
-- S p e c --
|
|
-- --
|
|
-- Copyright (C) 2015-2020, 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, task unit, or type 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
|
|
-- Subprogram_Variant (stand alone subprogram body)
|
|
-- 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
|
|
-- Subprogram_Variant
|
|
-- 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_Type_Contract (Type_Id : Entity_Id);
|
|
-- 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
|
|
-- Effective_Reads
|
|
-- Effective_Writes
|
|
--
|
|
-- In the case of a protected or task type, there will also be
|
|
-- a call to Analyze_Protected_Contract or Analyze_Task_Contract.
|
|
|
|
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.
|
|
|
|
function Get_Postcond_Enabled (Subp : Entity_Id) return Entity_Id;
|
|
-- Get the defining identifier for a subprogram's Postcond_Enabled
|
|
-- object created during the expansion of the subprogram's postconditions.
|
|
|
|
function Get_Result_Object_For_Postcond (Subp : Entity_Id) return Entity_Id;
|
|
-- Get the defining identifier for a subprogram's
|
|
-- Result_Object_For_Postcond object created during the expansion of the
|
|
-- subprogram's postconditions.
|
|
|
|
function Get_Return_Success_For_Postcond
|
|
(Subp : Entity_Id) return Entity_Id;
|
|
-- Get the defining identifier for a subprogram's
|
|
-- Return_Success_For_Postcond object created during the expansion of the
|
|
-- subprogram's postconditions.
|
|
|
|
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;
|