[multiple changes]
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com> * contracts.ads, contracts.adb: New unit. * exp_ch6.adb Add with and use clauses for Contracts. (Expand_Subprogram_Contract): Moved to Contracts. * exp_ch6.ads (Expand_Subprogram_Contract): Moved to Contracts. * sem_ch3.adb Add with and use clauses for Contracts. (Analyze_Object_Contract): Moved to Contracts. (Analyze_Declarations): Remove local variable Pack_Decl. Do not capture global references in contracts. Check the hidden states of a package body. * sem_ch6.adb Add with and use clauses in Contracts. (Analyze_Generic_Subprogram_Body): Do not capture global references in contracts. (Analyze_Subprogram_Body_Contract): Moved to Contracts. (Analyze_Subprogram_Body_Helper): Freeze the contract of the nearest enclosing package body. Always analyze the subprogram body contract. Do not expand the subprogram body contract. (Analyze_Subprogram_Contract): Moved to Contracts. * sem_ch6.ads (Analyze_Subprogram_Body_Contract): Moved to Contracts. (Analyze_Subprogram_Contract): Moved to Contracts. * sem_ch7.adb Add with and use clauses for Contracts. (Analyze_Package_Body_Contract): Moved to Contracts. (Analyze_Package_Body_Helper): Freeze the contract of the nearest enclosing package body. (Analyze_Package_Contract): Moved to Contracts. * sem_ch7.ads (Analyze_Package_Body_Contract): Moved to Contracts. (Analyze_Package_Contract): Moved to Contracts. * sem_ch10.adb Add with and use clauses for Contracts. (Analyze_Compilation_Unit): Do not capture global references in contracts. (Analyze_Subprogram_Body_Stub_Contract): Moved to Contracts. * sem_ch10.ads (Analyze_Subprogram_Body_Stub_Contract): Moved to Contracts. * sem_ch12.adb Add with and use clauses for Contracts. (Analyze_Subprogram_Instantiation): Update the call to Instantiate_Subprogram_Contract. (Instantiate_Package_Body): Do not copy the entity of the spec when creating an entity for the body. Construct a brand new defining identifier for the body and inherit the Comes_From_Source flag from the spec. (Instantiate_Subprogram_Body): Remove Anon_Id to Act_Decl_Id and update all occurrences. Construct a brand new defining identifier for the body and inherit the Comes_From_Source flag from the spec. (Instantiate_Subprogram_Contract): Moved to Contracts. (Save_Global_References_In_Aspects): Moved to the spec of Sem_Ch12. (Save_Global_References_In_Contract): Moved to Contracts. * sem_ch12.ads (Save_Global_References_In_Aspects): Moved from the body of Sem_Ch12. (Save_Global_References_In_Contract): Moved to Contracts. * sem_prag.adb Add with and use clauses for Contracts. (Add_Item): Removed. All references to this routine have been replaced with calls to Append_New_Elmt. (Analyze_Constituent): Add special diagnostics for errors caused by freezing of contracts. (Analyze_Refined_State_In_Decl_Part): Add formal parameter Freeze_Id. Add new global variable Freeze_Posted. (Collect_Body_States): Removed. (Report_Unused_States): Removed. * sem_prag.ads (Analyze_Defined_State_In_Decl_Part): Add formal parameter Freeze_Id and update comment on usage. * sem_util.adb Remove with and use clauses for Sem_Ch12. (Add_Contract_Item): Moved to Contracts. (Check_Unused_Body_States): New routine. (Collect_Body_States): New routine. (Create_Generic_Contract): Moved to Contracts. (Inherit_Subprogram_Contract): Moved to Contracts. (Report_Unused_Body_States): New routine. * sem_util.ads (Add_Contract_Item): Moved to Contracts. (Check_Unused_Body_States): New routine. (Collect_Body_States): New routine. (Create_Generic_Contract): Moved to Contracts. (Inherit_Subprogram_Contract): Moved to Contracts. (Report_Unused_Body_States): New routine. * sinfo.adb (Is_Expanded_Contract): New routine. (Set_Is_Expanded_Contract): New routine. * sinfo.ads New attribute Is_Expanded_Contract along with placement in nodes. (Is_Expanded_Contract): New routine along with pragma Inline. (Set_Is_Expanded_Contract): New routine along with pragma Inline. * gcc-interface/Make-lang.in: Add entry for contracts.o 2015-10-23 Bob Duff <duff@adacore.com> * bindgen.adb, init.c, opt.ads, switch-b.adb: Implement new -Ea and -Es switches. * switch-b.ads: Minor comment fix. * bindusg.adb: Document new -Ea and -Es switches. * s-exctra.ads: Use -Es instead of -E. From-SVN: r229253
This commit is contained in:
Arnaud Charlet
parent
9733088f6a
commit
879ac954ef
|
|
@ -1,3 +1,105 @@
|
|||
2015-10-23 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* contracts.ads, contracts.adb: New unit.
|
||||
* exp_ch6.adb Add with and use clauses for Contracts.
|
||||
(Expand_Subprogram_Contract): Moved to Contracts.
|
||||
* exp_ch6.ads (Expand_Subprogram_Contract): Moved to Contracts.
|
||||
* sem_ch3.adb Add with and use clauses for Contracts.
|
||||
(Analyze_Object_Contract): Moved to Contracts.
|
||||
(Analyze_Declarations): Remove local variable Pack_Decl. Do not
|
||||
capture global references in contracts. Check the hidden states
|
||||
of a package body.
|
||||
* sem_ch6.adb Add with and use clauses in Contracts.
|
||||
(Analyze_Generic_Subprogram_Body): Do not capture global
|
||||
references in contracts.
|
||||
(Analyze_Subprogram_Body_Contract):
|
||||
Moved to Contracts.
|
||||
(Analyze_Subprogram_Body_Helper): Freeze the
|
||||
contract of the nearest enclosing package body. Always analyze
|
||||
the subprogram body contract. Do not expand the subprogram
|
||||
body contract.
|
||||
(Analyze_Subprogram_Contract): Moved to Contracts.
|
||||
* sem_ch6.ads (Analyze_Subprogram_Body_Contract): Moved to Contracts.
|
||||
(Analyze_Subprogram_Contract): Moved to Contracts.
|
||||
* sem_ch7.adb Add with and use clauses for Contracts.
|
||||
(Analyze_Package_Body_Contract): Moved to Contracts.
|
||||
(Analyze_Package_Body_Helper): Freeze the contract of the
|
||||
nearest enclosing package body.
|
||||
(Analyze_Package_Contract): Moved to Contracts.
|
||||
* sem_ch7.ads (Analyze_Package_Body_Contract): Moved to Contracts.
|
||||
(Analyze_Package_Contract): Moved to Contracts.
|
||||
* sem_ch10.adb Add with and use clauses for Contracts.
|
||||
(Analyze_Compilation_Unit): Do not capture global references
|
||||
in contracts.
|
||||
(Analyze_Subprogram_Body_Stub_Contract): Moved to Contracts.
|
||||
* sem_ch10.ads (Analyze_Subprogram_Body_Stub_Contract): Moved
|
||||
to Contracts.
|
||||
* sem_ch12.adb Add with and use clauses for Contracts.
|
||||
(Analyze_Subprogram_Instantiation): Update the call to
|
||||
Instantiate_Subprogram_Contract.
|
||||
(Instantiate_Package_Body):
|
||||
Do not copy the entity of the spec when creating an entity
|
||||
for the body. Construct a brand new defining identifier for
|
||||
the body and inherit the Comes_From_Source flag from the spec.
|
||||
(Instantiate_Subprogram_Body): Remove Anon_Id to Act_Decl_Id
|
||||
and update all occurrences. Construct a brand new defining
|
||||
identifier for the body and inherit the Comes_From_Source
|
||||
flag from the spec.
|
||||
(Instantiate_Subprogram_Contract): Moved
|
||||
to Contracts.
|
||||
(Save_Global_References_In_Aspects): Moved to
|
||||
the spec of Sem_Ch12.
|
||||
(Save_Global_References_In_Contract):
|
||||
Moved to Contracts.
|
||||
* sem_ch12.ads (Save_Global_References_In_Aspects): Moved from
|
||||
the body of Sem_Ch12.
|
||||
(Save_Global_References_In_Contract):
|
||||
Moved to Contracts.
|
||||
* sem_prag.adb Add with and use clauses for Contracts.
|
||||
(Add_Item): Removed. All references to this routine have been
|
||||
replaced with calls to Append_New_Elmt.
|
||||
(Analyze_Constituent):
|
||||
Add special diagnostics for errors caused by freezing of
|
||||
contracts.
|
||||
(Analyze_Refined_State_In_Decl_Part): Add formal
|
||||
parameter Freeze_Id. Add new global variable Freeze_Posted.
|
||||
(Collect_Body_States): Removed.
|
||||
(Report_Unused_States): Removed.
|
||||
* sem_prag.ads (Analyze_Defined_State_In_Decl_Part): Add formal
|
||||
parameter Freeze_Id and update comment on usage.
|
||||
* sem_util.adb Remove with and use clauses for
|
||||
Sem_Ch12.
|
||||
(Add_Contract_Item): Moved to Contracts.
|
||||
(Check_Unused_Body_States): New routine.
|
||||
(Collect_Body_States):
|
||||
New routine.
|
||||
(Create_Generic_Contract): Moved to Contracts.
|
||||
(Inherit_Subprogram_Contract): Moved to Contracts.
|
||||
(Report_Unused_Body_States): New routine.
|
||||
* sem_util.ads (Add_Contract_Item): Moved to Contracts.
|
||||
(Check_Unused_Body_States): New routine.
|
||||
(Collect_Body_States): New routine.
|
||||
(Create_Generic_Contract): Moved to Contracts.
|
||||
(Inherit_Subprogram_Contract): Moved to Contracts.
|
||||
(Report_Unused_Body_States): New routine.
|
||||
* sinfo.adb (Is_Expanded_Contract): New routine.
|
||||
(Set_Is_Expanded_Contract): New routine.
|
||||
* sinfo.ads New attribute Is_Expanded_Contract along with
|
||||
placement in nodes.
|
||||
(Is_Expanded_Contract): New routine along
|
||||
with pragma Inline.
|
||||
(Set_Is_Expanded_Contract): New routine
|
||||
along with pragma Inline.
|
||||
* gcc-interface/Make-lang.in: Add entry for contracts.o
|
||||
|
||||
2015-10-23 Bob Duff <duff@adacore.com>
|
||||
|
||||
* bindgen.adb, init.c, opt.ads, switch-b.adb: Implement new -Ea and
|
||||
-Es switches.
|
||||
* switch-b.ads: Minor comment fix.
|
||||
* bindusg.adb: Document new -Ea and -Es switches.
|
||||
* s-exctra.ads: Use -Es instead of -E.
|
||||
|
||||
2015-10-23 Tristan Gingold <gingold@adacore.com>
|
||||
|
||||
* gcc-interface/utils2.c (build_call_alloc_dealloc): Check no implicit
|
||||
|
|
|
|||
|
|
@ -166,6 +166,7 @@ package body Bindgen is
|
|||
-- Num_Interrupt_States : Integer;
|
||||
-- Unreserve_All_Interrupts : Integer;
|
||||
-- Exception_Tracebacks : Integer;
|
||||
-- Exception_Tracebacks_Symbolic : Integer;
|
||||
-- Detect_Blocking : Integer;
|
||||
-- Default_Stack_Size : Integer;
|
||||
-- Leap_Seconds_Support : Integer;
|
||||
|
|
@ -235,10 +236,13 @@ package body Bindgen is
|
|||
-- Unreserve_All_Interrupts is set to one if at least one unit in the
|
||||
-- partition had a pragma Unreserve_All_Interrupts, and zero otherwise.
|
||||
|
||||
-- Exception_Tracebacks is set to one if the -E parameter was present
|
||||
-- in the bind and to zero otherwise. Note that on some targets exception
|
||||
-- tracebacks are provided by default, so a value of zero for this
|
||||
-- parameter does not necessarily mean no trace backs are available.
|
||||
-- Exception_Tracebacks is set to one if the -Ea or -E parameter was
|
||||
-- present in the bind and to zero otherwise. Note that on some targets
|
||||
-- exception tracebacks are provided by default, so a value of zero for
|
||||
-- this parameter does not necessarily mean no trace backs are available.
|
||||
|
||||
-- Exception_Tracebacks_Symbolic is set to one if the -Es parameter was
|
||||
-- present in the bind and to zero otherwise.
|
||||
|
||||
-- Detect_Blocking indicates whether pragma Detect_Blocking is active or
|
||||
-- not. A value of zero indicates that the pragma is not present, while a
|
||||
|
|
@ -607,10 +611,16 @@ package body Bindgen is
|
|||
WBI (" pragma Import (C, Unreserve_All_Interrupts, " &
|
||||
"""__gl_unreserve_all_interrupts"");");
|
||||
|
||||
if Exception_Tracebacks then
|
||||
if Exception_Tracebacks or Exception_Tracebacks_Symbolic then
|
||||
WBI (" Exception_Tracebacks : Integer;");
|
||||
WBI (" pragma Import (C, Exception_Tracebacks, " &
|
||||
"""__gl_exception_tracebacks"");");
|
||||
|
||||
if Exception_Tracebacks_Symbolic then
|
||||
WBI (" Exception_Tracebacks_Symbolic : Integer;");
|
||||
WBI (" pragma Import (C, Exception_Tracebacks_Symbolic, " &
|
||||
"""__gl_exception_tracebacks_symbolic"");");
|
||||
end if;
|
||||
end if;
|
||||
|
||||
WBI (" Detect_Blocking : Integer;");
|
||||
|
|
@ -795,8 +805,12 @@ package body Bindgen is
|
|||
Set_Char (';');
|
||||
Write_Statement_Buffer;
|
||||
|
||||
if Exception_Tracebacks then
|
||||
if Exception_Tracebacks or Exception_Tracebacks_Symbolic then
|
||||
WBI (" Exception_Tracebacks := 1;");
|
||||
|
||||
if Exception_Tracebacks_Symbolic then
|
||||
WBI (" Exception_Tracebacks_Symbolic := 1;");
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Set_String (" Detect_Blocking := ");
|
||||
|
|
|
|||
|
|
@ -108,7 +108,10 @@ package body Bindusg is
|
|||
|
||||
-- Line for -E switch
|
||||
|
||||
Write_Line (" -E Store tracebacks in exception occurrences");
|
||||
Write_Line (" -Ea Store tracebacks in exception occurrences");
|
||||
Write_Line (" -Es Store tracebacks in exception occurrences,");
|
||||
Write_Line (" and enable symbolic tracebacks");
|
||||
Write_Line (" -E Same as -Ea");
|
||||
|
||||
-- The -f switch is voluntarily omitted, because it is obsolete
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,156 @@
|
|||
------------------------------------------------------------------------------
|
||||
-- --
|
||||
-- GNAT COMPILER COMPONENTS --
|
||||
-- --
|
||||
-- C O N T R A C T S --
|
||||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 2015, 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, package [body],
|
||||
-- subprogram [body] or variable denoted by Id. The following are valid
|
||||
-- pragmas:
|
||||
-- Abstract_State
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
-- Constant_After_Elaboration
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Effective_Reads
|
||||
-- Effective_Writes
|
||||
-- Extensions_Visible
|
||||
-- Global
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Refined_States
|
||||
-- Test_Case
|
||||
-- Volatile_Function
|
||||
|
||||
procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id);
|
||||
-- Analyze the contract of the nearest package body (if any) which encloses
|
||||
-- package or subprogram body Body_Decl.
|
||||
|
||||
procedure Analyze_Object_Contract (Obj_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
|
||||
-- Part_Of
|
||||
|
||||
procedure Analyze_Package_Body_Contract
|
||||
(Body_Id : Entity_Id;
|
||||
Freeze_Id : Entity_Id := Empty);
|
||||
-- Analyze all delayed aspects chained on the contract of package body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects that are considered are:
|
||||
-- Refined_State
|
||||
--
|
||||
-- Freeze_Id is the entity of a [generic] package body or a [generic]
|
||||
-- subprogram body which "feezes" the contract of Body_Id.
|
||||
|
||||
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of package Pack_Id
|
||||
-- as if they appeared at the end of a declarative region. The aspects
|
||||
-- that are considered are:
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of
|
||||
|
||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. Aspects
|
||||
-- in question are:
|
||||
-- Contract_Cases (stand alone body)
|
||||
-- Depends (stand alone body)
|
||||
-- Global (stand alone body)
|
||||
-- Postcondition (stand alone body)
|
||||
-- Precondition (stand alone body)
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case (stand alone body)
|
||||
|
||||
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram
|
||||
-- Subp_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
|
||||
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of a subprogram body
|
||||
-- stub Stub_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case
|
||||
|
||||
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 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;
|
||||
1362
gcc/ada/exp_ch6.adb
1362
gcc/ada/exp_ch6.adb
File diff suppressed because it is too large
Load Diff
|
|
@ -41,12 +41,6 @@ package Exp_Ch6 is
|
|||
-- This procedure contains common processing for Expand_N_Function_Call,
|
||||
-- Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
|
||||
|
||||
procedure Expand_Subprogram_Contract (N : Node_Id);
|
||||
-- Expand the contracts of a subprogram body and its correspoding spec (if
|
||||
-- any). This routine processes all [refined] pre- and postconditions as
|
||||
-- well as Contract_Cases, invariants and predicates. N denotes the body of
|
||||
-- the subprogram.
|
||||
|
||||
procedure Freeze_Subprogram (N : Node_Id);
|
||||
-- generate the appropriate expansions related to Subprogram freeze
|
||||
-- nodes (e.g. the filling of the corresponding Dispatch Table for
|
||||
|
|
|
|||
|
|
@ -243,6 +243,7 @@ GNAT_ADA_OBJS = \
|
|||
ada/casing.o \
|
||||
ada/checks.o \
|
||||
ada/comperr.o \
|
||||
ada/contracts.o \
|
||||
ada/csets.o \
|
||||
ada/cstand.o \
|
||||
ada/debug.o \
|
||||
|
|
|
|||
|
|
@ -110,6 +110,7 @@ char *__gl_interrupt_states = 0;
|
|||
int __gl_num_interrupt_states = 0;
|
||||
int __gl_unreserve_all_interrupts = 0;
|
||||
int __gl_exception_tracebacks = 0;
|
||||
int __gl_exception_tracebacks_symbolic = 0;
|
||||
int __gl_detect_blocking = 0;
|
||||
int __gl_default_stack_size = -1;
|
||||
int __gl_leap_seconds_support = 0;
|
||||
|
|
|
|||
|
|
@ -595,7 +595,12 @@ package Opt is
|
|||
|
||||
Exception_Tracebacks : Boolean := False;
|
||||
-- GNATBIND
|
||||
-- Set to True to store tracebacks in exception occurrences (-E)
|
||||
-- Set to True to store tracebacks in exception occurrences (-Ea or -E)
|
||||
|
||||
Exception_Tracebacks_Symbolic : Boolean := False;
|
||||
-- GNATBIND
|
||||
-- Set to True to store tracebacks in exception occurrences and enable
|
||||
-- symbolic tracebacks (-Es).
|
||||
|
||||
Extensions_Allowed : Boolean := False;
|
||||
-- GNAT
|
||||
|
|
|
|||
|
|
@ -48,6 +48,10 @@
|
|||
-- may return any string output in association with a provided call chain.
|
||||
-- The decorator replaces the default backtrace mentioned above.
|
||||
|
||||
-- On systems that use DWARF debugging output, then if the "-g" compiler
|
||||
-- switch and the "-Es" binder switch are used, the decorator is automatically
|
||||
-- set to Symbolic_Traceback.
|
||||
|
||||
with System.Traceback_Entries;
|
||||
|
||||
package System.Exception_Traces is
|
||||
|
|
@ -89,12 +93,15 @@ package System.Exception_Traces is
|
|||
-- output for a call chain provided by way of a tracebacks array.
|
||||
|
||||
procedure Set_Trace_Decorator (Decorator : Traceback_Decorator);
|
||||
-- Set the decorator to be used for future automatic outputs. Restore
|
||||
-- the default behavior (output of raw addresses) if the provided
|
||||
-- access value is null.
|
||||
-- Set the decorator to be used for future automatic outputs. Restore the
|
||||
-- default behavior if the provided access value is null.
|
||||
--
|
||||
-- Note: System.Traceback.Symbolic.Symbolic_Traceback may be used as the
|
||||
-- Decorator, to get a symbolic traceback. This will cause a significant
|
||||
-- cpu and memory overhead.
|
||||
-- cpu and memory overhead on some platforms.
|
||||
--
|
||||
-- Note: The Decorator is called when constructing the
|
||||
-- Exception_Information; that needs to be taken into account
|
||||
-- if the Decorator has any side effects.
|
||||
|
||||
end System.Exception_Traces;
|
||||
|
|
|
|||
|
|
@ -23,50 +23,50 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Elists; use Elists;
|
||||
with Fname; use Fname;
|
||||
with Fname.UF; use Fname.UF;
|
||||
with Freeze; use Freeze;
|
||||
with Impunit; use Impunit;
|
||||
with Inline; use Inline;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Par_SCO; use Par_SCO;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Snames; use Snames;
|
||||
with Style; use Style;
|
||||
with Stylesw; use Stylesw;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uname; use Uname;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Contracts; use Contracts;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Elists; use Elists;
|
||||
with Fname; use Fname;
|
||||
with Fname.UF; use Fname.UF;
|
||||
with Freeze; use Freeze;
|
||||
with Impunit; use Impunit;
|
||||
with Inline; use Inline;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Par_SCO; use Par_SCO;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Snames; use Snames;
|
||||
with Style; use Style;
|
||||
with Stylesw; use Stylesw;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uname; use Uname;
|
||||
|
||||
package body Sem_Ch10 is
|
||||
|
||||
|
|
@ -940,15 +940,6 @@ package body Sem_Ch10 is
|
|||
N_Subprogram_Declaration)
|
||||
then
|
||||
Analyze_Subprogram_Contract (Defining_Entity (Unit_Node));
|
||||
|
||||
-- Capture all global references in a generic subprogram that acts as
|
||||
-- a compilation unit now that the contract has been analyzed.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Unit_Node) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Unit_Node),
|
||||
Gen_Id => Defining_Entity (Unit_Node));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Generate distribution stubs if requested and no error
|
||||
|
|
@ -2006,39 +1997,6 @@ package body Sem_Ch10 is
|
|||
Restore_Opt_Config_Switches (Opts);
|
||||
end Analyze_Subprogram_Body_Stub;
|
||||
|
||||
-------------------------------------------
|
||||
-- Analyze_Subprogram_Body_Stub_Contract --
|
||||
-------------------------------------------
|
||||
|
||||
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
|
||||
Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id));
|
||||
Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
|
||||
|
||||
begin
|
||||
-- A subprogram body stub may act as its own spec or as the completion
|
||||
-- of a previous declaration. Depending on the context, the contract of
|
||||
-- the stub may contain two sets of pragmas.
|
||||
|
||||
-- The stub is a completion, the applicable pragmas are:
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
|
||||
if Present (Spec_Id) then
|
||||
Analyze_Subprogram_Body_Contract (Stub_Id);
|
||||
|
||||
-- The stub acts as its own spec, the applicable pragmas are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
|
||||
else
|
||||
Analyze_Subprogram_Contract (Stub_Id);
|
||||
end if;
|
||||
end Analyze_Subprogram_Body_Stub_Contract;
|
||||
|
||||
---------------------
|
||||
-- Analyze_Subunit --
|
||||
---------------------
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2015, 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- --
|
||||
|
|
@ -24,6 +24,7 @@
|
|||
------------------------------------------------------------------------------
|
||||
|
||||
with Types; use Types;
|
||||
|
||||
package Sem_Ch10 is
|
||||
procedure Analyze_Compilation_Unit (N : Node_Id);
|
||||
procedure Analyze_With_Clause (N : Node_Id);
|
||||
|
|
@ -33,19 +34,6 @@ package Sem_Ch10 is
|
|||
procedure Analyze_Protected_Body_Stub (N : Node_Id);
|
||||
procedure Analyze_Subunit (N : Node_Id);
|
||||
|
||||
procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of a subprogram body
|
||||
-- stub Stub_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Test_Case
|
||||
|
||||
procedure Install_Context (N : Node_Id);
|
||||
-- Installs the entities from the context clause of the given compilation
|
||||
-- unit into the visibility chains. This is done before analyzing a unit.
|
||||
|
|
|
|||
|
|
@ -23,60 +23,61 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Expander; use Expander;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Fname; use Fname;
|
||||
with Fname.UF; use Fname.UF;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Itypes; use Itypes;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Nlists; use Nlists;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Rident; use Rident;
|
||||
with Restrict; use Restrict;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Elab; use Sem_Elab;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Sinput.L; use Sinput.L;
|
||||
with Snames; use Snames;
|
||||
with Stringt; use Stringt;
|
||||
with Uname; use Uname;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Contracts; use Contracts;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Expander; use Expander;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Fname; use Fname;
|
||||
with Fname.UF; use Fname.UF;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Itypes; use Itypes;
|
||||
with Lib; use Lib;
|
||||
with Lib.Load; use Lib.Load;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Nlists; use Nlists;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Rident; use Rident;
|
||||
with Restrict; use Restrict;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Elab; use Sem_Elab;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Sinput.L; use Sinput.L;
|
||||
with Snames; use Snames;
|
||||
with Stringt; use Stringt;
|
||||
with Uname; use Uname;
|
||||
with Table;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
with Warnsw; use Warnsw;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
with Warnsw; use Warnsw;
|
||||
|
||||
with GNAT.HTable;
|
||||
|
||||
|
|
@ -842,10 +843,6 @@ package body Sem_Ch12 is
|
|||
-- Restore suffix 'P' to primitives of Prims_List and leave Prims_List
|
||||
-- set to No_Elist.
|
||||
|
||||
procedure Save_Global_References_In_Aspects (N : Node_Id);
|
||||
-- Save all global references found within the expressions of all aspects
|
||||
-- that appear on node N.
|
||||
|
||||
procedure Set_Instance_Env
|
||||
(Gen_Unit : Entity_Id;
|
||||
Act_Unit : Entity_Id);
|
||||
|
|
@ -4803,11 +4800,6 @@ package body Sem_Ch12 is
|
|||
-- aspects that appear in the generic. This renaming declaration is
|
||||
-- inserted after the instance declaration which it renames.
|
||||
|
||||
procedure Instantiate_Subprogram_Contract (Templ : Node_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 Renaming_List.
|
||||
|
||||
------------------------------------
|
||||
-- Analyze_Instance_And_Renamings --
|
||||
------------------------------------
|
||||
|
|
@ -5009,53 +5001,6 @@ package body Sem_Ch12 is
|
|||
end if;
|
||||
end Build_Subprogram_Renaming;
|
||||
|
||||
-------------------------------------
|
||||
-- Instantiate_Subprogram_Contract --
|
||||
-------------------------------------
|
||||
|
||||
procedure Instantiate_Subprogram_Contract (Templ : Node_Id) is
|
||||
procedure Instantiate_Pragmas (First_Prag : Node_Id);
|
||||
-- Instantiate all contract-related source pragmas found in the list
|
||||
-- starting with pragma First_Prag. Each instantiated pragma is added
|
||||
-- to list Renaming_List.
|
||||
|
||||
-------------------------
|
||||
-- Instantiate_Pragmas --
|
||||
-------------------------
|
||||
|
||||
procedure Instantiate_Pragmas (First_Prag : Node_Id) is
|
||||
Inst_Prag : Node_Id;
|
||||
Prag : Node_Id;
|
||||
|
||||
begin
|
||||
Prag := First_Prag;
|
||||
while Present (Prag) loop
|
||||
if Is_Generic_Contract_Pragma (Prag) then
|
||||
Inst_Prag :=
|
||||
Copy_Generic_Node (Prag, Empty, Instantiating => True);
|
||||
|
||||
Set_Analyzed (Inst_Prag, False);
|
||||
Append_To (Renaming_List, Inst_Prag);
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
end Instantiate_Pragmas;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Items : constant Node_Id := Contract (Defining_Entity (Templ));
|
||||
|
||||
-- Start of processing for Instantiate_Subprogram_Contract
|
||||
|
||||
begin
|
||||
if Present (Items) then
|
||||
Instantiate_Pragmas (Pre_Post_Conditions (Items));
|
||||
Instantiate_Pragmas (Contract_Test_Cases (Items));
|
||||
Instantiate_Pragmas (Classifications (Items));
|
||||
end if;
|
||||
end Instantiate_Subprogram_Contract;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
|
||||
|
|
@ -5227,9 +5172,10 @@ package body Sem_Ch12 is
|
|||
-- must be instantiated explicitly because they are not part of the
|
||||
-- subprogram template.
|
||||
|
||||
Instantiate_Subprogram_Contract (Original_Node (Gen_Decl));
|
||||
Build_Subprogram_Renaming;
|
||||
Instantiate_Subprogram_Contract
|
||||
(Original_Node (Gen_Decl), Renaming_List);
|
||||
|
||||
Build_Subprogram_Renaming;
|
||||
Analyze_Instance_And_Renamings;
|
||||
|
||||
-- If the generic is marked Import (Intrinsic), then so is the
|
||||
|
|
@ -10888,9 +10834,12 @@ package body Sem_Ch12 is
|
|||
Copy_Generic_Node
|
||||
(Original_Node (Gen_Body), Empty, Instantiating => True);
|
||||
|
||||
-- Build new name (possibly qualified) for body declaration
|
||||
-- Create proper (possibly qualified) defining name for the body, to
|
||||
-- correspond to the one in the spec.
|
||||
|
||||
Act_Body_Id := New_Copy (Act_Decl_Id);
|
||||
Act_Body_Id :=
|
||||
Make_Defining_Identifier (Sloc (Act_Decl_Id), Chars (Act_Decl_Id));
|
||||
Set_Comes_From_Source (Act_Body_Id, Comes_From_Source (Act_Decl_Id));
|
||||
|
||||
-- Some attributes of spec entity are not inherited by body entity
|
||||
|
||||
|
|
@ -10901,7 +10850,8 @@ package body Sem_Ch12 is
|
|||
then
|
||||
Act_Body_Name :=
|
||||
Make_Defining_Program_Unit_Name (Loc,
|
||||
Name => New_Copy_Tree (Name (Defining_Unit_Name (Act_Spec))),
|
||||
Name =>
|
||||
New_Copy_Tree (Name (Defining_Unit_Name (Act_Spec))),
|
||||
Defining_Identifier => Act_Body_Id);
|
||||
else
|
||||
Act_Body_Name := Act_Body_Id;
|
||||
|
|
@ -11109,7 +11059,7 @@ package body Sem_Ch12 is
|
|||
Gen_Id : constant Node_Id := Name (Inst_Node);
|
||||
Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node);
|
||||
Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit);
|
||||
Anon_Id : constant Entity_Id :=
|
||||
Act_Decl_Id : constant Entity_Id :=
|
||||
Defining_Unit_Name (Specification (Act_Decl));
|
||||
Pack_Id : constant Entity_Id :=
|
||||
Defining_Unit_Name (Parent (Act_Decl));
|
||||
|
|
@ -11119,6 +11069,7 @@ package body Sem_Ch12 is
|
|||
Saved_Warnings : constant Warning_Record := Save_Warnings;
|
||||
|
||||
Act_Body : Node_Id;
|
||||
Act_Body_Id : Entity_Id;
|
||||
Gen_Body : Node_Id;
|
||||
Gen_Body_Id : Node_Id;
|
||||
Pack_Body : Node_Id;
|
||||
|
|
@ -11160,11 +11111,11 @@ package body Sem_Ch12 is
|
|||
-- the spec entity appropriately.
|
||||
|
||||
if Is_Imported (Gen_Unit) then
|
||||
Set_Is_Imported (Anon_Id);
|
||||
Set_First_Rep_Item (Anon_Id, First_Rep_Item (Gen_Unit));
|
||||
Set_Interface_Name (Anon_Id, Interface_Name (Gen_Unit));
|
||||
Set_Convention (Anon_Id, Convention (Gen_Unit));
|
||||
Set_Has_Completion (Anon_Id);
|
||||
Set_Is_Imported (Act_Decl_Id);
|
||||
Set_First_Rep_Item (Act_Decl_Id, First_Rep_Item (Gen_Unit));
|
||||
Set_Interface_Name (Act_Decl_Id, Interface_Name (Gen_Unit));
|
||||
Set_Convention (Act_Decl_Id, Convention (Gen_Unit));
|
||||
Set_Has_Completion (Act_Decl_Id);
|
||||
return;
|
||||
|
||||
-- For other cases, compile the body
|
||||
|
|
@ -11194,11 +11145,11 @@ package body Sem_Ch12 is
|
|||
("missing proper body for instantiation", Gen_Body);
|
||||
end if;
|
||||
|
||||
Set_Has_Completion (Anon_Id);
|
||||
Set_Has_Completion (Act_Decl_Id);
|
||||
return;
|
||||
end if;
|
||||
|
||||
Save_Env (Gen_Unit, Anon_Id);
|
||||
Save_Env (Gen_Unit, Act_Decl_Id);
|
||||
Style_Check := False;
|
||||
|
||||
-- If the context of the instance is subject to SPARK_Mode "off" or
|
||||
|
|
@ -11221,14 +11172,17 @@ package body Sem_Ch12 is
|
|||
Copy_Generic_Node
|
||||
(Original_Node (Gen_Body), Empty, Instantiating => True);
|
||||
|
||||
-- Create proper defining name for the body, to correspond to
|
||||
-- the one in the spec.
|
||||
-- Create proper defining name for the body, to correspond to the one
|
||||
-- in the spec.
|
||||
|
||||
Set_Defining_Unit_Name (Specification (Act_Body),
|
||||
Make_Defining_Identifier
|
||||
(Sloc (Defining_Entity (Inst_Node)), Chars (Anon_Id)));
|
||||
Set_Corresponding_Spec (Act_Body, Anon_Id);
|
||||
Set_Has_Completion (Anon_Id);
|
||||
Act_Body_Id :=
|
||||
Make_Defining_Identifier (Sloc (Act_Decl_Id), Chars (Act_Decl_Id));
|
||||
|
||||
Set_Comes_From_Source (Act_Body_Id, Comes_From_Source (Act_Decl_Id));
|
||||
Set_Defining_Unit_Name (Specification (Act_Body), Act_Body_Id);
|
||||
|
||||
Set_Corresponding_Spec (Act_Body, Act_Decl_Id);
|
||||
Set_Has_Completion (Act_Decl_Id);
|
||||
Check_Generic_Actuals (Pack_Id, False);
|
||||
|
||||
-- Generate a reference to link the visible subprogram instance to
|
||||
|
|
@ -11327,16 +11281,16 @@ package body Sem_Ch12 is
|
|||
if Body_Optional then
|
||||
return;
|
||||
|
||||
elsif Ekind (Anon_Id) = E_Procedure then
|
||||
elsif Ekind (Act_Decl_Id) = E_Procedure then
|
||||
Act_Body :=
|
||||
Make_Subprogram_Body (Loc,
|
||||
Specification =>
|
||||
Make_Procedure_Specification (Loc,
|
||||
Defining_Unit_Name =>
|
||||
Make_Defining_Identifier (Loc, Chars (Anon_Id)),
|
||||
Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
|
||||
Parameter_Specifications =>
|
||||
New_Copy_List
|
||||
(Parameter_Specifications (Parent (Anon_Id)))),
|
||||
(Parameter_Specifications (Parent (Act_Decl_Id)))),
|
||||
|
||||
Declarations => Empty_List,
|
||||
Handled_Statement_Sequence =>
|
||||
|
|
@ -11352,7 +11306,7 @@ package body Sem_Ch12 is
|
|||
Make_Raise_Program_Error (Loc,
|
||||
Reason => PE_Access_Before_Elaboration);
|
||||
|
||||
Set_Etype (Ret_Expr, (Etype (Anon_Id)));
|
||||
Set_Etype (Ret_Expr, (Etype (Act_Decl_Id)));
|
||||
Set_Analyzed (Ret_Expr);
|
||||
|
||||
Act_Body :=
|
||||
|
|
@ -11360,12 +11314,12 @@ package body Sem_Ch12 is
|
|||
Specification =>
|
||||
Make_Function_Specification (Loc,
|
||||
Defining_Unit_Name =>
|
||||
Make_Defining_Identifier (Loc, Chars (Anon_Id)),
|
||||
Make_Defining_Identifier (Loc, Chars (Act_Decl_Id)),
|
||||
Parameter_Specifications =>
|
||||
New_Copy_List
|
||||
(Parameter_Specifications (Parent (Anon_Id))),
|
||||
(Parameter_Specifications (Parent (Act_Decl_Id))),
|
||||
Result_Definition =>
|
||||
New_Occurrence_Of (Etype (Anon_Id), Loc)),
|
||||
New_Occurrence_Of (Etype (Act_Decl_Id), Loc)),
|
||||
|
||||
Declarations => Empty_List,
|
||||
Handled_Statement_Sequence =>
|
||||
|
|
@ -14970,63 +14924,6 @@ package body Sem_Ch12 is
|
|||
end loop;
|
||||
end Save_Global_References_In_Aspects;
|
||||
|
||||
----------------------------------------
|
||||
-- Save_Global_References_In_Contract --
|
||||
----------------------------------------
|
||||
|
||||
procedure Save_Global_References_In_Contract
|
||||
(Templ : Node_Id;
|
||||
Gen_Id : Entity_Id)
|
||||
is
|
||||
procedure Save_Global_References_In_List (First_Prag : Node_Id);
|
||||
-- Save all global references in contract-related source pragmas found
|
||||
-- in the list starting with pragma First_Prag.
|
||||
|
||||
------------------------------------
|
||||
-- Save_Global_References_In_List --
|
||||
------------------------------------
|
||||
|
||||
procedure Save_Global_References_In_List (First_Prag : Node_Id) is
|
||||
Prag : Node_Id;
|
||||
|
||||
begin
|
||||
Prag := First_Prag;
|
||||
while Present (Prag) loop
|
||||
if Is_Generic_Contract_Pragma (Prag) then
|
||||
Save_Global_References (Prag);
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
end Save_Global_References_In_List;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Items : constant Node_Id := Contract (Defining_Entity (Templ));
|
||||
|
||||
-- Start of processing for Save_Global_References_In_Contract
|
||||
|
||||
begin
|
||||
-- The entity of the analyzed generic copy must be on the scope stack
|
||||
-- to ensure proper detection of global references.
|
||||
|
||||
Push_Scope (Gen_Id);
|
||||
|
||||
if Permits_Aspect_Specifications (Templ)
|
||||
and then Has_Aspects (Templ)
|
||||
then
|
||||
Save_Global_References_In_Aspects (Templ);
|
||||
end if;
|
||||
|
||||
if Present (Items) then
|
||||
Save_Global_References_In_List (Pre_Post_Conditions (Items));
|
||||
Save_Global_References_In_List (Contract_Test_Cases (Items));
|
||||
Save_Global_References_In_List (Classifications (Items));
|
||||
end if;
|
||||
|
||||
Pop_Scope;
|
||||
end Save_Global_References_In_Contract;
|
||||
|
||||
--------------------------------------
|
||||
-- Set_Copied_Sloc_For_Inlined_Body --
|
||||
--------------------------------------
|
||||
|
|
|
|||
|
|
@ -152,12 +152,9 @@ package Sem_Ch12 is
|
|||
-- restored in stack-like fashion. Front-end inlining also uses these
|
||||
-- structures for the management of private/full views.
|
||||
|
||||
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.
|
||||
procedure Save_Global_References_In_Aspects (N : Node_Id);
|
||||
-- Save all global references found within the expressions of all aspects
|
||||
-- that appear on node N.
|
||||
|
||||
procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id);
|
||||
-- This procedure is used when a subprogram body is inlined. This process
|
||||
|
|
|
|||
|
|
@ -23,64 +23,62 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Checks; use Checks;
|
||||
with Debug; use Debug;
|
||||
with Elists; use Elists;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Eval_Fat; use Eval_Fat;
|
||||
with Exp_Ch3; use Exp_Ch3;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Itypes; use Itypes;
|
||||
with Layout; use Layout;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Case; use Sem_Case;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Smem; use Sem_Smem;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinput; use Sinput;
|
||||
with Snames; use Snames;
|
||||
with Targparm; use Targparm;
|
||||
with Tbuild; use Tbuild;
|
||||
with Ttypes; use Ttypes;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Checks; use Checks;
|
||||
with Contracts; use Contracts;
|
||||
with Debug; use Debug;
|
||||
with Elists; use Elists;
|
||||
with Einfo; use Einfo;
|
||||
with Errout; use Errout;
|
||||
with Eval_Fat; use Eval_Fat;
|
||||
with Exp_Ch3; use Exp_Ch3;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Itypes; use Itypes;
|
||||
with Layout; use Layout;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Case; use Sem_Case;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch7; use Sem_Ch7;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Smem; use Sem_Smem;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinput; use Sinput;
|
||||
with Snames; use Snames;
|
||||
with Targparm; use Targparm;
|
||||
with Tbuild; use Tbuild;
|
||||
with Ttypes; use Ttypes;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
|
||||
package body Sem_Ch3 is
|
||||
|
||||
|
|
@ -93,16 +91,6 @@ package body Sem_Ch3 is
|
|||
-- abstract interface types implemented by a record type or a derived
|
||||
-- record type.
|
||||
|
||||
procedure Analyze_Object_Contract (Obj_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
|
||||
-- Part_Of
|
||||
|
||||
procedure Build_Derived_Type
|
||||
(N : Node_Id;
|
||||
Parent_Type : Entity_Id;
|
||||
|
|
@ -2306,7 +2294,6 @@ package body Sem_Ch3 is
|
|||
Context : Node_Id := Empty;
|
||||
Freeze_From : Entity_Id := Empty;
|
||||
Next_Decl : Node_Id;
|
||||
Pack_Decl : Node_Id := Empty;
|
||||
|
||||
Body_Seen : Boolean := False;
|
||||
-- Flag set when the first body [stub] is encountered
|
||||
|
|
@ -2477,7 +2464,6 @@ package body Sem_Ch3 is
|
|||
Context := Parent (L);
|
||||
|
||||
if Nkind (Context) = N_Package_Specification then
|
||||
Pack_Decl := Parent (Context);
|
||||
|
||||
-- When a package has private declarations, its contract must be
|
||||
-- analyzed at the end of the said declarations. This way both the
|
||||
|
|
@ -2506,14 +2492,12 @@ package body Sem_Ch3 is
|
|||
end if;
|
||||
|
||||
elsif Nkind (Context) = N_Package_Body then
|
||||
Pack_Decl := Context;
|
||||
Analyze_Package_Body_Contract (Defining_Entity (Context));
|
||||
end if;
|
||||
|
||||
-- Analyze the contracts of all subprogram declarations, subprogram
|
||||
-- bodies and variables now due to the delayed visibility needs of
|
||||
-- of their aspects and pragmas. Capture global references in generic
|
||||
-- subprograms or bodies.
|
||||
-- bodies and variables due to the delayed visibility needs of their
|
||||
-- aspects and pragmas.
|
||||
|
||||
Decl := First (L);
|
||||
while Present (Decl) loop
|
||||
|
|
@ -2533,43 +2517,21 @@ package body Sem_Ch3 is
|
|||
Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
|
||||
end if;
|
||||
|
||||
-- Capture all global references in a generic subprogram or a body
|
||||
-- [stub] now that the contract has been analyzed.
|
||||
|
||||
if Nkind_In (Decl, N_Generic_Subprogram_Declaration,
|
||||
N_Subprogram_Body,
|
||||
N_Subprogram_Body_Stub)
|
||||
and then Is_Generic_Declaration_Or_Body (Decl)
|
||||
then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Decl),
|
||||
Gen_Id => Corresponding_Spec_Of (Decl));
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
end loop;
|
||||
|
||||
-- The owner of the declarations is a package [body]
|
||||
if Nkind (Context) = N_Package_Body then
|
||||
|
||||
if Present (Pack_Decl) then
|
||||
-- Ensure that all abstract states and objects declared in the
|
||||
-- state space of a package body are utilized as constituents.
|
||||
|
||||
-- Capture all global references in a generic package or a body
|
||||
-- after all nested generic subprograms and bodies were subjected
|
||||
-- to the same processing.
|
||||
|
||||
if Is_Generic_Declaration_Or_Body (Pack_Decl) then
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (Pack_Decl),
|
||||
Gen_Id => Corresponding_Spec_Of (Pack_Decl));
|
||||
end if;
|
||||
Check_Unused_Body_States (Defining_Entity (Context));
|
||||
|
||||
-- State refinements are visible upto the end the of the package
|
||||
-- body declarations. Hide the state refinements from visibility
|
||||
-- to restore the original state conditions.
|
||||
|
||||
if Nkind (Pack_Decl) = N_Package_Body then
|
||||
Remove_Visible_Refinements (Corresponding_Spec (Pack_Decl));
|
||||
end if;
|
||||
Remove_Visible_Refinements (Corresponding_Spec (Context));
|
||||
end if;
|
||||
end if;
|
||||
end Analyze_Declarations;
|
||||
|
|
@ -3288,173 +3250,6 @@ package body Sem_Ch3 is
|
|||
end if;
|
||||
end Analyze_Number_Declaration;
|
||||
|
||||
-----------------------------
|
||||
-- Analyze_Object_Contract --
|
||||
-----------------------------
|
||||
|
||||
procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
|
||||
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
|
||||
AR_Val : Boolean := False;
|
||||
AW_Val : Boolean := False;
|
||||
ER_Val : Boolean := False;
|
||||
EW_Val : Boolean := False;
|
||||
Prag : Node_Id;
|
||||
Seen : Boolean := False;
|
||||
|
||||
begin
|
||||
-- The loop parameter in an element iterator over a formal container
|
||||
-- is declared with an object declaration but no contracts apply.
|
||||
|
||||
if Ekind (Obj_Id) = E_Loop_Parameter then
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- Constant related checks
|
||||
|
||||
if Ekind (Obj_Id) = E_Constant then
|
||||
|
||||
-- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
|
||||
-- This check is relevant only when SPARK_Mode is on as it is not a
|
||||
-- standard Ada legality rule. Internally-generated constants that
|
||||
-- map generic formals to actuals in instantiations are allowed to
|
||||
-- be volatile.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Comes_From_Source (Obj_Id)
|
||||
and then Is_Effectively_Volatile (Obj_Id)
|
||||
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
|
||||
then
|
||||
Error_Msg_N ("constant cannot be volatile", Obj_Id);
|
||||
end if;
|
||||
|
||||
-- Variable related checks
|
||||
|
||||
else pragma Assert (Ekind (Obj_Id) = E_Variable);
|
||||
|
||||
-- The following checks are relevant only when SPARK_Mode is on as
|
||||
-- they are not standard Ada legality rules. Internally generated
|
||||
-- temporaries are ignored.
|
||||
|
||||
if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
|
||||
if Is_Effectively_Volatile (Obj_Id) then
|
||||
|
||||
-- The declaration of an effectively volatile object must
|
||||
-- appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
|
||||
|
||||
if not Is_Library_Level_Entity (Obj_Id) then
|
||||
Error_Msg_N
|
||||
("volatile variable & must be declared at library level",
|
||||
Obj_Id);
|
||||
|
||||
-- An object of a discriminated type cannot be effectively
|
||||
-- volatile except for protected objects (SPARK RM 7.1.3(5)).
|
||||
|
||||
elsif Has_Discriminants (Obj_Typ)
|
||||
and then not Is_Protected_Type (Obj_Typ)
|
||||
then
|
||||
Error_Msg_N
|
||||
("discriminated object & cannot be volatile", Obj_Id);
|
||||
|
||||
-- An object of a tagged type cannot be effectively volatile
|
||||
-- (SPARK RM C.6(5)).
|
||||
|
||||
elsif Is_Tagged_Type (Obj_Typ) then
|
||||
Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
|
||||
end if;
|
||||
|
||||
-- The object is not effectively volatile
|
||||
|
||||
else
|
||||
-- A non-effectively volatile object cannot have effectively
|
||||
-- volatile components (SPARK RM 7.1.3(6)).
|
||||
|
||||
if not Is_Effectively_Volatile (Obj_Id)
|
||||
and then Has_Volatile_Component (Obj_Typ)
|
||||
then
|
||||
Error_Msg_N
|
||||
("non-volatile object & cannot have volatile components",
|
||||
Obj_Id);
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
if Is_Ghost_Entity (Obj_Id) then
|
||||
|
||||
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
|
||||
|
||||
if Is_Effectively_Volatile (Obj_Id) then
|
||||
Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
|
||||
|
||||
-- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
|
||||
|
||||
elsif Is_Imported (Obj_Id) then
|
||||
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
|
||||
|
||||
elsif Is_Exported (Obj_Id) then
|
||||
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Analyze all external properties
|
||||
|
||||
Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
|
||||
Seen := True;
|
||||
end if;
|
||||
|
||||
Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
|
||||
Seen := True;
|
||||
end if;
|
||||
|
||||
Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
|
||||
Seen := True;
|
||||
end if;
|
||||
|
||||
Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
|
||||
|
||||
if Present (Prag) then
|
||||
Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
|
||||
Seen := True;
|
||||
end if;
|
||||
|
||||
-- Verify the mutual interaction of the various external properties
|
||||
|
||||
if Seen then
|
||||
Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Check whether the lack of indicator Part_Of agrees with the placement
|
||||
-- of the object with respect to the state space.
|
||||
|
||||
Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
|
||||
|
||||
if No (Prag) then
|
||||
Check_Missing_Part_Of (Obj_Id);
|
||||
end if;
|
||||
|
||||
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
|
||||
-- exception to this is the object that represents the dispatch table of
|
||||
-- a Ghost tagged type as the symbol needs to be exported.
|
||||
|
||||
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
|
||||
if Is_Exported (Obj_Id) then
|
||||
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
|
||||
|
||||
elsif Is_Imported (Obj_Id) then
|
||||
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
|
||||
end if;
|
||||
end if;
|
||||
end Analyze_Object_Contract;
|
||||
|
||||
--------------------------------
|
||||
-- Analyze_Object_Declaration --
|
||||
--------------------------------
|
||||
|
|
|
|||
|
|
@ -23,70 +23,71 @@
|
|||
-- --
|
||||
------------------------------------------------------------------------------
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Checks; use Checks;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Expander; use Expander;
|
||||
with Exp_Ch6; use Exp_Ch6;
|
||||
with Exp_Ch7; use Exp_Ch7;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Exp_Dbug; use Exp_Dbug;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Inline; use Inline;
|
||||
with Itypes; use Itypes;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Layout; use Layout;
|
||||
with Namet; use Namet;
|
||||
with Lib; use Lib;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch4; use Sem_Ch4;
|
||||
with Sem_Ch5; use Sem_Ch5;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Sinput; use Sinput;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Snames; use Snames;
|
||||
with Stringt; use Stringt;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Checks; use Checks;
|
||||
with Contracts; use Contracts;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Expander; use Expander;
|
||||
with Exp_Ch6; use Exp_Ch6;
|
||||
with Exp_Ch7; use Exp_Ch7;
|
||||
with Exp_Ch9; use Exp_Ch9;
|
||||
with Exp_Dbug; use Exp_Dbug;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Tss; use Exp_Tss;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Fname; use Fname;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Inline; use Inline;
|
||||
with Itypes; use Itypes;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Layout; use Layout;
|
||||
with Namet; use Namet;
|
||||
with Lib; use Lib;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch4; use Sem_Ch4;
|
||||
with Sem_Ch5; use Sem_Ch5;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Dim; use Sem_Dim;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Sinput; use Sinput;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Snames; use Snames;
|
||||
with Stringt; use Stringt;
|
||||
with Style;
|
||||
with Stylesw; use Stylesw;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
with Validsw; use Validsw;
|
||||
with Stylesw; use Stylesw;
|
||||
with Tbuild; use Tbuild;
|
||||
with Uintp; use Uintp;
|
||||
with Urealp; use Urealp;
|
||||
with Validsw; use Validsw;
|
||||
|
||||
package body Sem_Ch6 is
|
||||
|
||||
|
|
@ -1377,23 +1378,11 @@ package body Sem_Ch6 is
|
|||
Analyze_Declarations (Declarations (N));
|
||||
Check_Completion;
|
||||
|
||||
-- When a generic subprogram body appears inside a package, its
|
||||
-- contract is analyzed at the end of the package body declarations.
|
||||
-- This is due to the delay with respect of the package contract upon
|
||||
-- which the body contract may depend. When the generic subprogram
|
||||
-- body is a compilation unit, this delay is not necessary.
|
||||
-- Process the contract of the subprogram body after all declarations
|
||||
-- have been analyzed. This ensures that any contract-related pragmas
|
||||
-- are available through the N_Contract node of the body.
|
||||
|
||||
if Nkind (Parent (N)) = N_Compilation_Unit then
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
|
||||
-- Capture all global references in a generic subprogram body
|
||||
-- that acts as a compilation unit now that the contract has
|
||||
-- been analyzed.
|
||||
|
||||
Save_Global_References_In_Contract
|
||||
(Templ => Original_Node (N),
|
||||
Gen_Id => Gen_Id);
|
||||
end if;
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
|
||||
Analyze (Handled_Statement_Sequence (N));
|
||||
Save_Global_References (Original_Node (N));
|
||||
|
|
@ -2220,102 +2209,6 @@ package body Sem_Ch6 is
|
|||
end if;
|
||||
end Analyze_Subprogram_Body;
|
||||
|
||||
--------------------------------------
|
||||
-- Analyze_Subprogram_Body_Contract --
|
||||
--------------------------------------
|
||||
|
||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Body_Id);
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
Prag_Nam : Name_Id;
|
||||
Ref_Depends : Node_Id := Empty;
|
||||
Ref_Global : Node_Id := Empty;
|
||||
|
||||
begin
|
||||
-- When a subprogram body declaration is illegal, its defining entity is
|
||||
-- left unanalyzed. There is nothing left to do in this case because the
|
||||
-- body lacks a contract, or even a proper Ekind.
|
||||
|
||||
if Ekind (Body_Id) = E_Void then
|
||||
return;
|
||||
end if;
|
||||
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||
|
||||
-- All subprograms carry a contract, but for some it is not significant
|
||||
-- and should not be processed.
|
||||
|
||||
if not Has_Significant_Contract (Body_Id) then
|
||||
null;
|
||||
|
||||
-- The subprogram body is a completion, analyze all delayed pragmas that
|
||||
-- apply. Note that when the body is stand alone, the pragmas are always
|
||||
-- analyzed on the spot.
|
||||
|
||||
elsif Present (Items) then
|
||||
|
||||
-- Locate and store pragmas Refined_Depends and Refined_Global since
|
||||
-- their order of analysis matters.
|
||||
|
||||
Prag := Classifications (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Refined_Depends then
|
||||
Ref_Depends := Prag;
|
||||
|
||||
elsif Prag_Nam = Name_Refined_Global then
|
||||
Ref_Global := Prag;
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze Refined_Global first as Refined_Depends may mention items
|
||||
-- classified in the global refinement.
|
||||
|
||||
if Present (Ref_Global) then
|
||||
Analyze_Refined_Global_In_Decl_Part (Ref_Global);
|
||||
end if;
|
||||
|
||||
-- Refined_Depends must be analyzed after Refined_Global in order to
|
||||
-- see the modes of all global refinements.
|
||||
|
||||
if Present (Ref_Depends) then
|
||||
Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result or
|
||||
-- define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Body_Id);
|
||||
|
||||
-- A stand alone non-volatile function body cannot have an effectively
|
||||
-- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
|
||||
-- check is relevant only when SPARK_Mode is on as it is not a standard
|
||||
-- legality rule. The check is performed here because Volatile_Function
|
||||
-- is processed after the analysis of the related subprogram body.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Body_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Body_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
end Analyze_Subprogram_Body_Contract;
|
||||
|
||||
------------------------------------
|
||||
-- Analyze_Subprogram_Body_Helper --
|
||||
------------------------------------
|
||||
|
|
@ -3102,6 +2995,24 @@ package body Sem_Ch6 is
|
|||
-- Start of processing for Analyze_Subprogram_Body_Helper
|
||||
|
||||
begin
|
||||
-- A [generic] subprogram body "freezes" the contract of the nearest
|
||||
-- enclosing package body:
|
||||
|
||||
-- package body Nearest_Enclosing_Package
|
||||
-- with Refined_State => (State => Constit)
|
||||
-- is
|
||||
-- Constit : ...;
|
||||
|
||||
-- procedure Freezes_Enclosing_Package_Body
|
||||
-- with Refined_Depends => (Input => Constit) ...
|
||||
|
||||
-- This ensures that any annotations referenced by the contract of the
|
||||
-- [generic] subprogram body are available. This form of "freezing" is
|
||||
-- decoupled from the usual Freeze_xxx mechanism because it must also
|
||||
-- work in the context of generics where normal freezing is disabled.
|
||||
|
||||
Analyze_Enclosing_Package_Body_Contract (N);
|
||||
|
||||
-- Generic subprograms are handled separately. They always have a
|
||||
-- generic specification. Determine whether current scope has a
|
||||
-- previous declaration.
|
||||
|
|
@ -3842,23 +3753,11 @@ package body Sem_Ch6 is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
-- When a subprogram body appears inside a package, its contract is
|
||||
-- analyzed at the end of the package body declarations. This is due
|
||||
-- to the delay with respect of the package contract upon which the
|
||||
-- body contract may depend. When the subprogram body is stand alone
|
||||
-- and acts as a compilation unit, this delay is not necessary.
|
||||
-- A subprogram body "freezes" its own contract. Analyze the contract
|
||||
-- after the declarations of the body have been processed as pragmas
|
||||
-- are now chained on the contract of the subprogram body.
|
||||
|
||||
if Nkind (Parent (N)) = N_Compilation_Unit then
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
end if;
|
||||
|
||||
-- Deal with preconditions, [refined] postconditions, Contract_Cases,
|
||||
-- invariants and predicates associated with body and its spec. Since
|
||||
-- there is no routine Expand_Declarations which would otherwise deal
|
||||
-- with the contract expansion, generate all necessary mechanisms to
|
||||
-- verify the contract assertions now.
|
||||
|
||||
Expand_Subprogram_Contract (N);
|
||||
Analyze_Subprogram_Body_Contract (Body_Id);
|
||||
|
||||
-- If SPARK_Mode for body is not On, disable frontend inlining for this
|
||||
-- subprogram in GNATprove mode, as its body should not be analyzed.
|
||||
|
|
@ -4096,116 +3995,6 @@ package body Sem_Ch6 is
|
|||
Ghost_Mode := Save_Ghost_Mode;
|
||||
end Analyze_Subprogram_Body_Helper;
|
||||
|
||||
---------------------------------
|
||||
-- Analyze_Subprogram_Contract --
|
||||
---------------------------------
|
||||
|
||||
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Subp_Id);
|
||||
Depends : Node_Id := Empty;
|
||||
Global : Node_Id := Empty;
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
Prag_Nam : Name_Id;
|
||||
|
||||
begin
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related subprogram body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Subp_Id, Mode);
|
||||
|
||||
-- All subprograms carry a contract, but for some it is not significant
|
||||
-- and should not be processed.
|
||||
|
||||
if not Has_Significant_Contract (Subp_Id) then
|
||||
null;
|
||||
|
||||
elsif Present (Items) then
|
||||
|
||||
-- Analyze pre- and postconditions
|
||||
|
||||
Prag := Pre_Post_Conditions (Items);
|
||||
while Present (Prag) loop
|
||||
Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze contract-cases and test-cases
|
||||
|
||||
Prag := Contract_Test_Cases (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Contract_Cases then
|
||||
Analyze_Contract_Cases_In_Decl_Part (Prag);
|
||||
else
|
||||
pragma Assert (Prag_Nam = Name_Test_Case);
|
||||
Analyze_Test_Case_In_Decl_Part (Prag);
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze classification pragmas
|
||||
|
||||
Prag := Classifications (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Depends then
|
||||
Depends := Prag;
|
||||
|
||||
elsif Prag_Nam = Name_Global then
|
||||
Global := Prag;
|
||||
|
||||
-- Note that pragma Extensions_Visible has already been analyzed
|
||||
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze Global first as Depends may mention items classified in
|
||||
-- the global categorization.
|
||||
|
||||
if Present (Global) then
|
||||
Analyze_Global_In_Decl_Part (Global);
|
||||
end if;
|
||||
|
||||
-- Depends must be analyzed after Global in order to see the modes of
|
||||
-- all global items.
|
||||
|
||||
if Present (Depends) then
|
||||
Analyze_Depends_In_Decl_Part (Depends);
|
||||
end if;
|
||||
|
||||
-- Ensure that the contract cases or postconditions mention 'Result
|
||||
-- or define a post-state.
|
||||
|
||||
Check_Result_And_Post_State (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- A non-volatile function cannot have an effectively volatile formal
|
||||
-- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
|
||||
-- only when SPARK_Mode is on as it is not a standard legality rule. The
|
||||
-- check is performed here because pragma Volatile_Function is processed
|
||||
-- after the analysis of the related subprogram declaration.
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
|
||||
and then not Is_Volatile_Function (Subp_Id)
|
||||
then
|
||||
Check_Nonvolatile_Function_Profile (Subp_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
end Analyze_Subprogram_Contract;
|
||||
|
||||
------------------------------------
|
||||
-- Analyze_Subprogram_Declaration --
|
||||
------------------------------------
|
||||
|
|
|
|||
|
|
@ -45,31 +45,6 @@ package Sem_Ch6 is
|
|||
procedure Analyze_Subprogram_Declaration (N : Node_Id);
|
||||
procedure Analyze_Subprogram_Body (N : Node_Id);
|
||||
|
||||
procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. Aspects
|
||||
-- in question are:
|
||||
-- Contract_Cases (stand alone body)
|
||||
-- Depends (stand alone body)
|
||||
-- Global (stand alone body)
|
||||
-- Postcondition (stand alone body)
|
||||
-- Precondition (stand alone body)
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Test_Case (stand alone body)
|
||||
|
||||
procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of subprogram
|
||||
-- Subp_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects in question are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
|
||||
function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id;
|
||||
-- Analyze subprogram specification in both subprogram declarations
|
||||
-- and body declarations. Returns the defining entity for the
|
||||
|
|
|
|||
|
|
@ -28,44 +28,45 @@
|
|||
-- handling of private and full declarations, and the construction of dispatch
|
||||
-- tables for tagged types.
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Dbug; use Exp_Dbug;
|
||||
with Ghost; use Ghost;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Nlists; use Nlists;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Restrict; use Restrict;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Snames; use Snames;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinput; use Sinput;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Contracts; use Contracts;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Disp; use Exp_Disp;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Dbug; use Exp_Dbug;
|
||||
with Ghost; use Ghost;
|
||||
with Lib; use Lib;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet; use Namet;
|
||||
with Nmake; use Nmake;
|
||||
with Nlists; use Nlists;
|
||||
with Opt; use Opt;
|
||||
with Output; use Output;
|
||||
with Restrict; use Restrict;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Cat; use Sem_Cat;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch10; use Sem_Ch10;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Prag; use Sem_Prag;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Snames; use Snames;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinput; use Sinput;
|
||||
with Style;
|
||||
with Uintp; use Uintp;
|
||||
with Uintp; use Uintp;
|
||||
|
||||
package body Sem_Ch7 is
|
||||
|
||||
|
|
@ -182,47 +183,6 @@ package body Sem_Ch7 is
|
|||
end if;
|
||||
end Analyze_Package_Body;
|
||||
|
||||
-----------------------------------
|
||||
-- Analyze_Package_Body_Contract --
|
||||
-----------------------------------
|
||||
|
||||
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id) is
|
||||
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
|
||||
Mode : SPARK_Mode_Type;
|
||||
Ref_State : Node_Id;
|
||||
|
||||
begin
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related package body.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Body_Id, Mode);
|
||||
|
||||
Ref_State := Get_Pragma (Body_Id, Pragma_Refined_State);
|
||||
|
||||
-- The analysis of pragma Refined_State detects whether the spec has
|
||||
-- abstract states available for refinement.
|
||||
|
||||
if Present (Ref_State) then
|
||||
Analyze_Refined_State_In_Decl_Part (Ref_State);
|
||||
|
||||
-- State refinement is required when the package declaration defines at
|
||||
-- least one abstract state. Null states are not considered. Refinement
|
||||
-- is not envorced when SPARK checks are turned off.
|
||||
|
||||
elsif SPARK_Mode /= Off
|
||||
and then Requires_State_Refinement (Spec_Id, Body_Id)
|
||||
then
|
||||
Error_Msg_N ("package & requires state refinement", Spec_Id);
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
end Analyze_Package_Body_Contract;
|
||||
|
||||
---------------------------------
|
||||
-- Analyze_Package_Body_Helper --
|
||||
---------------------------------
|
||||
|
|
@ -582,6 +542,30 @@ package body Sem_Ch7 is
|
|||
-- Start of processing for Analyze_Package_Body_Helper
|
||||
|
||||
begin
|
||||
-- A [generic] package body "freezes" the contract of the nearest
|
||||
-- enclosing package body:
|
||||
|
||||
-- package body Nearest_Enclosing_Package
|
||||
-- with Refined_State => (State => Constit)
|
||||
-- is
|
||||
-- Constit : ...;
|
||||
|
||||
-- package body Freezes_Enclosing_Package_Body
|
||||
-- with Refined_State => (State_2 => Constit_2)
|
||||
-- is
|
||||
-- Constit_2 : ...;
|
||||
|
||||
-- procedure Proc
|
||||
-- with Refined_Depends => (Input => (Constit, Constit_2)) ...
|
||||
|
||||
-- This ensures that any annotations referenced by the contract of a
|
||||
-- [generic] subprogram body declared within the current package body
|
||||
-- are available. This form of "freezing" is decoupled from the usual
|
||||
-- Freeze_xxx mechanism because it must also work in the context of
|
||||
-- generics where normal freezing is disabled.
|
||||
|
||||
Analyze_Enclosing_Package_Body_Contract (N);
|
||||
|
||||
-- Find corresponding package specification, and establish the current
|
||||
-- scope. The visible defining entity for the package is the defining
|
||||
-- occurrence in the spec. On exit from the package body, all body
|
||||
|
|
@ -944,74 +928,6 @@ package body Sem_Ch7 is
|
|||
Ghost_Mode := Save_Ghost_Mode;
|
||||
end Analyze_Package_Body_Helper;
|
||||
|
||||
------------------------------
|
||||
-- Analyze_Package_Contract --
|
||||
------------------------------
|
||||
|
||||
procedure Analyze_Package_Contract (Pack_Id : Entity_Id) is
|
||||
Items : constant Node_Id := Contract (Pack_Id);
|
||||
Init : Node_Id := Empty;
|
||||
Init_Cond : Node_Id := Empty;
|
||||
Mode : SPARK_Mode_Type;
|
||||
Prag : Node_Id;
|
||||
Prag_Nam : Name_Id;
|
||||
|
||||
begin
|
||||
-- Due to the timing of contract analysis, delayed pragmas may be
|
||||
-- subject to the wrong SPARK_Mode, usually that of the enclosing
|
||||
-- context. To remedy this, restore the original SPARK_Mode of the
|
||||
-- related package.
|
||||
|
||||
Save_SPARK_Mode_And_Set (Pack_Id, Mode);
|
||||
|
||||
if Present (Items) then
|
||||
|
||||
-- Locate and store pragmas Initial_Condition and Initializes since
|
||||
-- their order of analysis matters.
|
||||
|
||||
Prag := Classifications (Items);
|
||||
while Present (Prag) loop
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
if Prag_Nam = Name_Initial_Condition then
|
||||
Init_Cond := Prag;
|
||||
|
||||
elsif Prag_Nam = Name_Initializes then
|
||||
Init := Prag;
|
||||
end if;
|
||||
|
||||
Prag := Next_Pragma (Prag);
|
||||
end loop;
|
||||
|
||||
-- Analyze the initialization related pragmas. Initializes must come
|
||||
-- before Initial_Condition due to item dependencies.
|
||||
|
||||
if Present (Init) then
|
||||
Analyze_Initializes_In_Decl_Part (Init);
|
||||
end if;
|
||||
|
||||
if Present (Init_Cond) then
|
||||
Analyze_Initial_Condition_In_Decl_Part (Init_Cond);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Check whether the lack of indicator Part_Of agrees with the placement
|
||||
-- of the package instantiation with respect to the state space.
|
||||
|
||||
if Is_Generic_Instance (Pack_Id) then
|
||||
Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
|
||||
|
||||
if No (Prag) then
|
||||
Check_Missing_Part_Of (Pack_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Restore the SPARK_Mode of the enclosing context after all delayed
|
||||
-- pragmas have been analyzed.
|
||||
|
||||
Restore_SPARK_Mode (Mode);
|
||||
end Analyze_Package_Contract;
|
||||
|
||||
---------------------------------
|
||||
-- Analyze_Package_Declaration --
|
||||
---------------------------------
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2015, 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- --
|
||||
|
|
@ -32,20 +32,6 @@ package Sem_Ch7 is
|
|||
procedure Analyze_Package_Specification (N : Node_Id);
|
||||
procedure Analyze_Private_Type_Declaration (N : Node_Id);
|
||||
|
||||
procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of package body
|
||||
-- Body_Id as if they appeared at the end of a declarative region. The
|
||||
-- aspects that are considered are:
|
||||
-- Refined_State
|
||||
|
||||
procedure Analyze_Package_Contract (Pack_Id : Entity_Id);
|
||||
-- Analyze all delayed aspects chained on the contract of package Pack_Id
|
||||
-- as if they appeared at the end of a declarative region. The aspects
|
||||
-- that are considered are:
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of
|
||||
|
||||
procedure End_Package_Scope (P : Entity_Id);
|
||||
-- Calls Uninstall_Declarations, and then pops the scope stack
|
||||
|
||||
|
|
|
|||
|
|
@ -29,62 +29,63 @@
|
|||
-- to complete the syntax checks. Certain pragmas are handled partially or
|
||||
-- completely by the parser (see Par.Prag for further details).
|
||||
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Casing; use Casing;
|
||||
with Checks; use Checks;
|
||||
with Csets; use Csets;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Lib; use Lib;
|
||||
with Lib.Writ; use Lib.Writ;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet.Sp; use Namet.Sp;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Output; use Output;
|
||||
with Par_SCO; use Par_SCO;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Intr; use Sem_Intr;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Stringt; use Stringt;
|
||||
with Stylesw; use Stylesw;
|
||||
with Aspects; use Aspects;
|
||||
with Atree; use Atree;
|
||||
with Casing; use Casing;
|
||||
with Checks; use Checks;
|
||||
with Contracts; use Contracts;
|
||||
with Csets; use Csets;
|
||||
with Debug; use Debug;
|
||||
with Einfo; use Einfo;
|
||||
with Elists; use Elists;
|
||||
with Errout; use Errout;
|
||||
with Exp_Dist; use Exp_Dist;
|
||||
with Exp_Util; use Exp_Util;
|
||||
with Freeze; use Freeze;
|
||||
with Ghost; use Ghost;
|
||||
with Lib; use Lib;
|
||||
with Lib.Writ; use Lib.Writ;
|
||||
with Lib.Xref; use Lib.Xref;
|
||||
with Namet.Sp; use Namet.Sp;
|
||||
with Nlists; use Nlists;
|
||||
with Nmake; use Nmake;
|
||||
with Output; use Output;
|
||||
with Par_SCO; use Par_SCO;
|
||||
with Restrict; use Restrict;
|
||||
with Rident; use Rident;
|
||||
with Rtsfind; use Rtsfind;
|
||||
with Sem; use Sem;
|
||||
with Sem_Aux; use Sem_Aux;
|
||||
with Sem_Ch3; use Sem_Ch3;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Dist; use Sem_Dist;
|
||||
with Sem_Elim; use Sem_Elim;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
with Sem_Intr; use Sem_Intr;
|
||||
with Sem_Mech; use Sem_Mech;
|
||||
with Sem_Res; use Sem_Res;
|
||||
with Sem_Type; use Sem_Type;
|
||||
with Sem_Util; use Sem_Util;
|
||||
with Sem_Warn; use Sem_Warn;
|
||||
with Stand; use Stand;
|
||||
with Sinfo; use Sinfo;
|
||||
with Sinfo.CN; use Sinfo.CN;
|
||||
with Sinput; use Sinput;
|
||||
with Stringt; use Stringt;
|
||||
with Stylesw; use Stylesw;
|
||||
with Table;
|
||||
with Targparm; use Targparm;
|
||||
with Tbuild; use Tbuild;
|
||||
with Targparm; use Targparm;
|
||||
with Tbuild; use Tbuild;
|
||||
with Ttypes;
|
||||
with Uintp; use Uintp;
|
||||
with Uname; use Uname;
|
||||
with Urealp; use Urealp;
|
||||
with Validsw; use Validsw;
|
||||
with Warnsw; use Warnsw;
|
||||
with Uintp; use Uintp;
|
||||
with Uname; use Uname;
|
||||
with Urealp; use Urealp;
|
||||
with Validsw; use Validsw;
|
||||
with Warnsw; use Warnsw;
|
||||
|
||||
package body Sem_Prag is
|
||||
|
||||
|
|
@ -165,11 +166,6 @@ package body Sem_Prag is
|
|||
-- Local Subprograms and Variables --
|
||||
-------------------------------------
|
||||
|
||||
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id);
|
||||
-- Subsidiary routine to the analysis of pragmas Depends, Global and
|
||||
-- Refined_State. Append an entity to a list. If the list is empty, create
|
||||
-- a new list.
|
||||
|
||||
function Adjust_External_Name_Case (N : Node_Id) return Node_Id;
|
||||
-- This routine is used for possible casing adjustment of an explicit
|
||||
-- external name supplied as a string literal (the node N), according to
|
||||
|
|
@ -277,15 +273,6 @@ package body Sem_Prag is
|
|||
-- pragma in the source program, a breakpoint on rv catches this place in
|
||||
-- the source, allowing convenient stepping to the point of interest.
|
||||
|
||||
--------------
|
||||
-- Add_Item --
|
||||
--------------
|
||||
|
||||
procedure Add_Item (Item : Entity_Id; To_List : in out Elist_Id) is
|
||||
begin
|
||||
Append_New_Elmt (Item, To => To_List);
|
||||
end Add_Item;
|
||||
|
||||
-------------------------------
|
||||
-- Adjust_External_Name_Case --
|
||||
-------------------------------
|
||||
|
|
@ -826,7 +813,7 @@ package body Sem_Prag is
|
|||
SPARK_Msg_NE
|
||||
("duplicate use of item &", Item, Item_Id);
|
||||
else
|
||||
Add_Item (Item_Id, Seen);
|
||||
Append_New_Elmt (Item_Id, Seen);
|
||||
end if;
|
||||
|
||||
-- Detect illegal use of an input related to a null
|
||||
|
|
@ -846,7 +833,7 @@ package body Sem_Prag is
|
|||
-- of all processed inputs.
|
||||
|
||||
if Is_Input or else Self_Ref then
|
||||
Add_Item (Item_Id, All_Inputs_Seen);
|
||||
Append_New_Elmt (Item_Id, All_Inputs_Seen);
|
||||
end if;
|
||||
|
||||
-- State related checks (SPARK RM 6.1.5(3))
|
||||
|
|
@ -901,7 +888,7 @@ package body Sem_Prag is
|
|||
-- processed items.
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
Add_Item (Item_Id, States_Seen);
|
||||
Append_New_Elmt (Item_Id, States_Seen);
|
||||
end if;
|
||||
|
||||
if Ekind_In (Item_Id, E_Abstract_State,
|
||||
|
|
@ -909,7 +896,7 @@ package body Sem_Prag is
|
|||
E_Variable)
|
||||
and then Present (Encapsulating_State (Item_Id))
|
||||
then
|
||||
Add_Item (Item_Id, Constits_Seen);
|
||||
Append_New_Elmt (Item_Id, Constits_Seen);
|
||||
end if;
|
||||
|
||||
-- All other input/output items are illegal
|
||||
|
|
@ -2016,16 +2003,16 @@ package body Sem_Prag is
|
|||
-- items.
|
||||
|
||||
else
|
||||
Add_Item (Item_Id, Seen);
|
||||
Append_New_Elmt (Item_Id, Seen);
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
Add_Item (Item_Id, States_Seen);
|
||||
Append_New_Elmt (Item_Id, States_Seen);
|
||||
end if;
|
||||
|
||||
if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable)
|
||||
and then Present (Encapsulating_State (Item_Id))
|
||||
then
|
||||
Add_Item (Item_Id, Constits_Seen);
|
||||
Append_New_Elmt (Item_Id, Constits_Seen);
|
||||
end if;
|
||||
end if;
|
||||
end Analyze_Global_Item;
|
||||
|
|
@ -2396,14 +2383,14 @@ package body Sem_Prag is
|
|||
-- and variables.
|
||||
|
||||
else
|
||||
Add_Item (Item_Id, Items_Seen);
|
||||
Append_New_Elmt (Item_Id, Items_Seen);
|
||||
|
||||
if Ekind (Item_Id) = E_Abstract_State then
|
||||
Add_Item (Item_Id, States_Seen);
|
||||
Append_New_Elmt (Item_Id, States_Seen);
|
||||
end if;
|
||||
|
||||
if Present (Encapsulating_State (Item_Id)) then
|
||||
Add_Item (Item_Id, Constits_Seen);
|
||||
Append_New_Elmt (Item_Id, Constits_Seen);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
@ -2504,10 +2491,10 @@ package body Sem_Prag is
|
|||
-- Input is legal, add it to the list of processed inputs
|
||||
|
||||
else
|
||||
Add_Item (Input_Id, Inputs_Seen);
|
||||
Append_New_Elmt (Input_Id, Inputs_Seen);
|
||||
|
||||
if Ekind (Input_Id) = E_Abstract_State then
|
||||
Add_Item (Input_Id, States_Seen);
|
||||
Append_New_Elmt (Input_Id, States_Seen);
|
||||
end if;
|
||||
|
||||
if Ekind_In (Input_Id, E_Abstract_State,
|
||||
|
|
@ -2515,7 +2502,7 @@ package body Sem_Prag is
|
|||
E_Variable)
|
||||
and then Present (Encapsulating_State (Input_Id))
|
||||
then
|
||||
Add_Item (Input_Id, Constits_Seen);
|
||||
Append_New_Elmt (Input_Id, Constits_Seen);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
@ -2610,7 +2597,7 @@ package body Sem_Prag is
|
|||
if Comes_From_Source (Decl)
|
||||
and then Nkind (Decl) = N_Object_Declaration
|
||||
then
|
||||
Add_Item (Defining_Entity (Decl), States_And_Objs);
|
||||
Append_New_Elmt (Defining_Entity (Decl), States_And_Objs);
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
|
|
@ -3481,8 +3468,8 @@ package body Sem_Prag is
|
|||
|
||||
if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then
|
||||
SPARK_Msg_NE
|
||||
("indicator Part_Of must denote an abstract state of& "
|
||||
& "or public descendant (SPARK RM 7.2.6(3))",
|
||||
("indicator Part_Of must denote an abstract state or "
|
||||
& "public descendant of & (SPARK RM 7.2.6(3))",
|
||||
Indic, Parent_Unit);
|
||||
|
||||
elsif Scope (State_Id) = Parent_Unit
|
||||
|
|
@ -3494,8 +3481,8 @@ package body Sem_Prag is
|
|||
|
||||
else
|
||||
SPARK_Msg_NE
|
||||
("indicator Part_Of must denote an abstract state of& "
|
||||
& "or public descendant (SPARK RM 7.2.6(3))",
|
||||
("indicator Part_Of must denote an abstract state or "
|
||||
& "public descendant of & (SPARK RM 7.2.6(3))",
|
||||
Indic, Parent_Unit);
|
||||
end if;
|
||||
|
||||
|
|
@ -22493,7 +22480,7 @@ package body Sem_Prag is
|
|||
procedure Record_Item (Item_Id : Entity_Id) is
|
||||
begin
|
||||
if not Contains (Matched_Items, Item_Id) then
|
||||
Add_Item (Item_Id, Matched_Items);
|
||||
Append_New_Elmt (Item_Id, Matched_Items);
|
||||
end if;
|
||||
end Record_Item;
|
||||
|
||||
|
|
@ -23664,16 +23651,16 @@ package body Sem_Prag is
|
|||
and then Has_Visible_Refinement (Encapsulating_State (Item_Id))
|
||||
then
|
||||
if Global_Mode = Name_Input then
|
||||
Add_Item (Item_Id, In_Constits);
|
||||
Append_New_Elmt (Item_Id, In_Constits);
|
||||
|
||||
elsif Global_Mode = Name_In_Out then
|
||||
Add_Item (Item_Id, In_Out_Constits);
|
||||
Append_New_Elmt (Item_Id, In_Out_Constits);
|
||||
|
||||
elsif Global_Mode = Name_Output then
|
||||
Add_Item (Item_Id, Out_Constits);
|
||||
Append_New_Elmt (Item_Id, Out_Constits);
|
||||
|
||||
elsif Global_Mode = Name_Proof_In then
|
||||
Add_Item (Item_Id, Proof_In_Constits);
|
||||
Append_New_Elmt (Item_Id, Proof_In_Constits);
|
||||
end if;
|
||||
|
||||
-- When not a constituent, ensure that both occurrences of the
|
||||
|
|
@ -23821,13 +23808,13 @@ package body Sem_Prag is
|
|||
-- Add the item to the proper list
|
||||
|
||||
if Item_Mode = Name_Input then
|
||||
Add_Item (Item_Id, In_Items);
|
||||
Append_New_Elmt (Item_Id, In_Items);
|
||||
elsif Item_Mode = Name_In_Out then
|
||||
Add_Item (Item_Id, In_Out_Items);
|
||||
Append_New_Elmt (Item_Id, In_Out_Items);
|
||||
elsif Item_Mode = Name_Output then
|
||||
Add_Item (Item_Id, Out_Items);
|
||||
Append_New_Elmt (Item_Id, Out_Items);
|
||||
elsif Item_Mode = Name_Proof_In then
|
||||
Add_Item (Item_Id, Proof_In_Items);
|
||||
Append_New_Elmt (Item_Id, Proof_In_Items);
|
||||
end if;
|
||||
end Collect_Global_Item;
|
||||
|
||||
|
|
@ -24091,7 +24078,10 @@ package body Sem_Prag is
|
|||
-- Analyze_Refined_State_In_Decl_Part --
|
||||
----------------------------------------
|
||||
|
||||
procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id) is
|
||||
procedure Analyze_Refined_State_In_Decl_Part
|
||||
(N : Node_Id;
|
||||
Freeze_Id : Entity_Id := Empty)
|
||||
is
|
||||
Body_Decl : constant Node_Id := Find_Related_Package_Or_Body (N);
|
||||
Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
|
||||
Spec_Id : constant Entity_Id := Corresponding_Spec (Body_Decl);
|
||||
|
|
@ -24109,6 +24099,10 @@ package body Sem_Prag is
|
|||
-- A list that contains all constituents processed so far. The list is
|
||||
-- used to detect multiple uses of the same constituent.
|
||||
|
||||
Freeze_Posted : Boolean := False;
|
||||
-- A flag that controls the output of a freezing-related error (see use
|
||||
-- below).
|
||||
|
||||
Refined_States_Seen : Elist_Id := No_Elist;
|
||||
-- A list that contains all refined states processed so far. The list is
|
||||
-- used to detect duplicate refinements.
|
||||
|
|
@ -24116,16 +24110,9 @@ package body Sem_Prag is
|
|||
procedure Analyze_Refinement_Clause (Clause : Node_Id);
|
||||
-- Perform full analysis of a single refinement clause
|
||||
|
||||
function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id;
|
||||
-- Gather the entities of all abstract states and objects declared in
|
||||
-- the body state space of package Pack_Id.
|
||||
|
||||
procedure Report_Unrefined_States (States : Elist_Id);
|
||||
-- Emit errors for all unrefined abstract states found in list States
|
||||
|
||||
procedure Report_Unused_States (States : Elist_Id);
|
||||
-- Emit errors for all unused states found in list States
|
||||
|
||||
-------------------------------
|
||||
-- Analyze_Refinement_Clause --
|
||||
-------------------------------
|
||||
|
|
@ -24190,10 +24177,10 @@ package body Sem_Prag is
|
|||
|
||||
procedure Check_Matching_Constituent (Constit_Id : Entity_Id);
|
||||
-- Determine whether constituent Constit denoted by its entity
|
||||
-- Constit_Id appears in Hidden_States. Emit an error when the
|
||||
-- Constit_Id appears in Body_States. Emit an error when the
|
||||
-- constituent is not a valid hidden state of the related package
|
||||
-- or when it is used more than once. Otherwise remove the
|
||||
-- constituent from Hidden_States.
|
||||
-- constituent from Body_States.
|
||||
|
||||
--------------------------------
|
||||
-- Check_Matching_Constituent --
|
||||
|
|
@ -24212,7 +24199,7 @@ package body Sem_Prag is
|
|||
-- Add the constituent to the list of processed items to aid
|
||||
-- with the detection of duplicates.
|
||||
|
||||
Add_Item (Constit_Id, Constituents_Seen);
|
||||
Append_New_Elmt (Constit_Id, Constituents_Seen);
|
||||
|
||||
-- Collect the constituent in the list of refinement items
|
||||
-- and establish a relation between the refined state and
|
||||
|
|
@ -24436,12 +24423,56 @@ package body Sem_Prag is
|
|||
if Is_Entity_Name (Constit) then
|
||||
Constit_Id := Entity_Of (Constit);
|
||||
|
||||
if Ekind_In (Constit_Id, E_Abstract_State,
|
||||
E_Constant,
|
||||
E_Variable)
|
||||
-- When a constituent is declared after a subprogram body
|
||||
-- that caused "freezing" of the related contract where
|
||||
-- pragma Refined_State resides, the constituent appears
|
||||
-- undefined and carries Any_Id as its entity.
|
||||
|
||||
-- package body Pack
|
||||
-- with Refined_State => (State => Constit)
|
||||
-- is
|
||||
-- procedure Proc
|
||||
-- with Refined_Global => (Input => Constit)
|
||||
-- is
|
||||
-- ...
|
||||
-- end Proc;
|
||||
|
||||
-- Constit : ...;
|
||||
-- end Pack;
|
||||
|
||||
if Constit_Id = Any_Id then
|
||||
SPARK_Msg_NE ("& is undefined", Constit, Constit_Id);
|
||||
|
||||
-- Emit a specialized info message when the contract of
|
||||
-- the related package body was "frozen" by another body.
|
||||
-- Note that it is not possible to precisely identify why
|
||||
-- the constituent is undefined because it is not visible
|
||||
-- when pragma Refined_State is analyzed. This message is
|
||||
-- a reasonable approximation.
|
||||
|
||||
if Present (Freeze_Id) and then not Freeze_Posted then
|
||||
Freeze_Posted := True;
|
||||
|
||||
Error_Msg_Name_1 := Chars (Body_Id);
|
||||
Error_Msg_Sloc := Sloc (Freeze_Id);
|
||||
SPARK_Msg_NE
|
||||
("body & declared # freezes the contract of %",
|
||||
N, Freeze_Id);
|
||||
SPARK_Msg_N
|
||||
("\all constituents must be declared before body #",
|
||||
N);
|
||||
end if;
|
||||
|
||||
-- The constituent is a valid state or object
|
||||
|
||||
elsif Ekind_In (Constit_Id, E_Abstract_State,
|
||||
E_Constant,
|
||||
E_Variable)
|
||||
then
|
||||
Check_Matching_Constituent (Constit_Id);
|
||||
|
||||
-- Otherwise the constituent is illegal
|
||||
|
||||
else
|
||||
SPARK_Msg_NE
|
||||
("constituent & must denote object or state",
|
||||
|
|
@ -24519,7 +24550,7 @@ package body Sem_Prag is
|
|||
-- been refined.
|
||||
|
||||
if Node (State_Elmt) = State_Id then
|
||||
Add_Item (State_Id, Refined_States_Seen);
|
||||
Append_New_Elmt (State_Id, Refined_States_Seen);
|
||||
Remove_Elmt (Available_States, State_Elmt);
|
||||
return;
|
||||
end if;
|
||||
|
|
@ -24754,104 +24785,6 @@ package body Sem_Prag is
|
|||
Report_Unused_Constituents (Part_Of_Constits);
|
||||
end Analyze_Refinement_Clause;
|
||||
|
||||
-------------------------
|
||||
-- Collect_Body_States --
|
||||
-------------------------
|
||||
|
||||
function Collect_Body_States (Pack_Id : Entity_Id) return Elist_Id is
|
||||
Result : Elist_Id := No_Elist;
|
||||
-- A list containing all body states of Pack_Id
|
||||
|
||||
procedure Collect_Visible_States (Pack_Id : Entity_Id);
|
||||
-- Gather the entities of all abstract states and objects declared in
|
||||
-- the visible state space of package Pack_Id.
|
||||
|
||||
----------------------------
|
||||
-- Collect_Visible_States --
|
||||
----------------------------
|
||||
|
||||
procedure Collect_Visible_States (Pack_Id : Entity_Id) is
|
||||
Item_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Traverse the entity chain of the package and inspect all
|
||||
-- visible items.
|
||||
|
||||
Item_Id := First_Entity (Pack_Id);
|
||||
while Present (Item_Id) and then not In_Private_Part (Item_Id) loop
|
||||
|
||||
-- Do not consider internally generated items as those cannot
|
||||
-- be named and participate in refinement.
|
||||
|
||||
if not Comes_From_Source (Item_Id) then
|
||||
null;
|
||||
|
||||
elsif Ekind (Item_Id) = E_Abstract_State then
|
||||
Add_Item (Item_Id, Result);
|
||||
|
||||
-- Do not consider constants or variables that map generic
|
||||
-- formals to their actuals, as the formals cannot be named
|
||||
-- from the outside and participate in refinement.
|
||||
|
||||
elsif Ekind_In (Item_Id, E_Constant, E_Variable)
|
||||
and then No (Corresponding_Generic_Association
|
||||
(Declaration_Node (Item_Id)))
|
||||
then
|
||||
Add_Item (Item_Id, Result);
|
||||
|
||||
-- Recursively gather the visible states of a nested package
|
||||
|
||||
elsif Ekind (Item_Id) = E_Package then
|
||||
Collect_Visible_States (Item_Id);
|
||||
end if;
|
||||
|
||||
Next_Entity (Item_Id);
|
||||
end loop;
|
||||
end Collect_Visible_States;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Pack_Body : constant Node_Id :=
|
||||
Declaration_Node (Body_Entity (Pack_Id));
|
||||
Decl : Node_Id;
|
||||
Item_Id : Entity_Id;
|
||||
|
||||
-- Start of processing for Collect_Body_States
|
||||
|
||||
begin
|
||||
-- Inspect the declarations of the body looking for source objects,
|
||||
-- packages and package instantiations.
|
||||
|
||||
Decl := First (Declarations (Pack_Body));
|
||||
while Present (Decl) loop
|
||||
|
||||
-- Capture source objects as internally generated temporaries
|
||||
-- cannot be named and participate in refinement.
|
||||
|
||||
if Nkind (Decl) = N_Object_Declaration then
|
||||
Item_Id := Defining_Entity (Decl);
|
||||
|
||||
if Comes_From_Source (Item_Id) then
|
||||
Add_Item (Item_Id, Result);
|
||||
end if;
|
||||
|
||||
-- Capture the visible abstract states and objects of a source
|
||||
-- package [instantiation].
|
||||
|
||||
elsif Nkind (Decl) = N_Package_Declaration then
|
||||
Item_Id := Defining_Entity (Decl);
|
||||
|
||||
if Comes_From_Source (Item_Id) then
|
||||
Collect_Visible_States (Item_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
end loop;
|
||||
|
||||
return Result;
|
||||
end Collect_Body_States;
|
||||
|
||||
-----------------------------
|
||||
-- Report_Unrefined_States --
|
||||
-----------------------------
|
||||
|
|
@ -24871,61 +24804,6 @@ package body Sem_Prag is
|
|||
end if;
|
||||
end Report_Unrefined_States;
|
||||
|
||||
--------------------------
|
||||
-- Report_Unused_States --
|
||||
--------------------------
|
||||
|
||||
procedure Report_Unused_States (States : Elist_Id) is
|
||||
Posted : Boolean := False;
|
||||
State_Elmt : Elmt_Id;
|
||||
State_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
if Present (States) then
|
||||
State_Elmt := First_Elmt (States);
|
||||
while Present (State_Elmt) loop
|
||||
State_Id := Node (State_Elmt);
|
||||
|
||||
-- Constants are part of the hidden state of a package, but the
|
||||
-- compiler cannot determine whether they have variable input
|
||||
-- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
|
||||
-- hidden state. Do not emit an error when a constant does not
|
||||
-- participate in a state refinement, even though it acts as a
|
||||
-- hidden state.
|
||||
|
||||
if Ekind (State_Id) = E_Constant then
|
||||
null;
|
||||
|
||||
-- Generate an error message of the form:
|
||||
|
||||
-- body of package ... has unused hidden states
|
||||
-- abstract state ... defined at ...
|
||||
-- variable ... defined at ...
|
||||
|
||||
else
|
||||
if not Posted then
|
||||
Posted := True;
|
||||
SPARK_Msg_N
|
||||
("body of package & has unused hidden states", Body_Id);
|
||||
end if;
|
||||
|
||||
Error_Msg_Sloc := Sloc (State_Id);
|
||||
|
||||
if Ekind (State_Id) = E_Abstract_State then
|
||||
SPARK_Msg_NE
|
||||
("\abstract state & defined #", Body_Id, State_Id);
|
||||
|
||||
else
|
||||
pragma Assert (Ekind (State_Id) = E_Variable);
|
||||
SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Elmt (State_Elmt);
|
||||
end loop;
|
||||
end if;
|
||||
end Report_Unused_States;
|
||||
|
||||
-- Local declarations
|
||||
|
||||
Clauses : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
|
||||
|
|
@ -24945,7 +24823,7 @@ package body Sem_Prag is
|
|||
-- state space of the package body. These items must be utilized as
|
||||
-- constituents in a state refinement.
|
||||
|
||||
Body_States := Collect_Body_States (Spec_Id);
|
||||
Body_States := Collect_Body_States (Body_Id);
|
||||
|
||||
-- Multiple non-null state refinements appear as an aggregate
|
||||
|
||||
|
|
@ -24977,7 +24855,7 @@ package body Sem_Prag is
|
|||
-- Ensure that all abstract states and objects declared in the body
|
||||
-- state space of the related package are utilized as constituents.
|
||||
|
||||
Report_Unused_States (Body_States);
|
||||
Report_Unused_Body_States (Body_Id, Body_States);
|
||||
end Analyze_Refined_State_In_Decl_Part;
|
||||
|
||||
------------------------------------
|
||||
|
|
@ -25857,9 +25735,9 @@ package body Sem_Prag is
|
|||
|
||||
else
|
||||
if Is_Input then
|
||||
Add_Item (Item, Subp_Inputs);
|
||||
Append_New_Elmt (Item, Subp_Inputs);
|
||||
else
|
||||
Add_Item (Item, Subp_Outputs);
|
||||
Append_New_Elmt (Item, Subp_Outputs);
|
||||
end if;
|
||||
end if;
|
||||
end Collect_Dependency_Item;
|
||||
|
|
@ -25908,11 +25786,11 @@ package body Sem_Prag is
|
|||
procedure Collect_Global_Item (Item : Node_Id; Mode : Name_Id) is
|
||||
begin
|
||||
if Nam_In (Mode, Name_In_Out, Name_Input) then
|
||||
Add_Item (Item, Subp_Inputs);
|
||||
Append_New_Elmt (Item, Subp_Inputs);
|
||||
end if;
|
||||
|
||||
if Nam_In (Mode, Name_In_Out, Name_Output) then
|
||||
Add_Item (Item, Subp_Outputs);
|
||||
Append_New_Elmt (Item, Subp_Outputs);
|
||||
end if;
|
||||
end Collect_Global_Item;
|
||||
|
||||
|
|
@ -25988,14 +25866,14 @@ package body Sem_Prag is
|
|||
E_In_Out_Parameter,
|
||||
E_In_Parameter)
|
||||
then
|
||||
Add_Item (Formal, Subp_Inputs);
|
||||
Append_New_Elmt (Formal, Subp_Inputs);
|
||||
end if;
|
||||
|
||||
if Ekind_In (Formal, E_Generic_In_Out_Parameter,
|
||||
E_In_Out_Parameter,
|
||||
E_Out_Parameter)
|
||||
then
|
||||
Add_Item (Formal, Subp_Outputs);
|
||||
Append_New_Elmt (Formal, Subp_Outputs);
|
||||
|
||||
-- Out parameters can act as inputs when the related type is
|
||||
-- tagged, unconstrained array, unconstrained record or record
|
||||
|
|
@ -26004,7 +25882,7 @@ package body Sem_Prag is
|
|||
if Ekind (Formal) = E_Out_Parameter
|
||||
and then Is_Unconstrained_Or_Tagged_Item (Formal)
|
||||
then
|
||||
Add_Item (Formal, Subp_Inputs);
|
||||
Append_New_Elmt (Formal, Subp_Inputs);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
|
|||
|
|
@ -209,8 +209,12 @@ package Sem_Prag is
|
|||
-- uses Analyze_Global_In_Decl_Part as a starting point, then performs
|
||||
-- various consistency checks between Global and Refined_Global.
|
||||
|
||||
procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
|
||||
-- Perform full analysis of delayed pragma Refined_State
|
||||
procedure Analyze_Refined_State_In_Decl_Part
|
||||
(N : Node_Id;
|
||||
Freeze_Id : Entity_Id := Empty);
|
||||
-- Perform full analysis of delayed pragma Refined_State. Freeze_Id denotes
|
||||
-- the entity of [generic] package body or [generic] subprogram body which
|
||||
-- caused "freezing" of the related contract where the pragma resides.
|
||||
|
||||
procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id);
|
||||
-- Perform preanalysis of pragma Test_Case
|
||||
|
|
|
|||
|
|
@ -52,7 +52,6 @@ with Sem_Aux; use Sem_Aux;
|
|||
with Sem_Attr; use Sem_Attr;
|
||||
with Sem_Ch6; use Sem_Ch6;
|
||||
with Sem_Ch8; use Sem_Ch8;
|
||||
with Sem_Ch12; use Sem_Ch12;
|
||||
with Sem_Ch13; use Sem_Ch13;
|
||||
with Sem_Disp; use Sem_Disp;
|
||||
with Sem_Eval; use Sem_Eval;
|
||||
|
|
@ -250,209 +249,6 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Add_Block_Identifier;
|
||||
|
||||
-----------------------
|
||||
-- Add_Contract_Item --
|
||||
-----------------------
|
||||
|
||||
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is
|
||||
Items : Node_Id := Contract (Id);
|
||||
|
||||
procedure Add_Classification;
|
||||
-- Prepend Prag to the list of classifications
|
||||
|
||||
procedure Add_Contract_Test_Case;
|
||||
-- Prepend Prag to the list of contract and test cases
|
||||
|
||||
procedure Add_Pre_Post_Condition;
|
||||
-- Prepend Prag to the list of pre- and postconditions
|
||||
|
||||
------------------------
|
||||
-- Add_Classification --
|
||||
------------------------
|
||||
|
||||
procedure Add_Classification is
|
||||
begin
|
||||
Set_Next_Pragma (Prag, Classifications (Items));
|
||||
Set_Classifications (Items, Prag);
|
||||
end Add_Classification;
|
||||
|
||||
----------------------------
|
||||
-- Add_Contract_Test_Case --
|
||||
----------------------------
|
||||
|
||||
procedure Add_Contract_Test_Case is
|
||||
begin
|
||||
Set_Next_Pragma (Prag, Contract_Test_Cases (Items));
|
||||
Set_Contract_Test_Cases (Items, Prag);
|
||||
end Add_Contract_Test_Case;
|
||||
|
||||
----------------------------
|
||||
-- Add_Pre_Post_Condition --
|
||||
----------------------------
|
||||
|
||||
procedure Add_Pre_Post_Condition is
|
||||
begin
|
||||
Set_Next_Pragma (Prag, Pre_Post_Conditions (Items));
|
||||
Set_Pre_Post_Conditions (Items, Prag);
|
||||
end Add_Pre_Post_Condition;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Prag_Nam : Name_Id;
|
||||
|
||||
-- Start of processing for Add_Contract_Item
|
||||
|
||||
begin
|
||||
-- A contract must contain only pragmas
|
||||
|
||||
pragma Assert (Nkind (Prag) = N_Pragma);
|
||||
Prag_Nam := Pragma_Name (Prag);
|
||||
|
||||
-- Create a new contract when adding the first item
|
||||
|
||||
if No (Items) then
|
||||
Items := Make_Contract (Sloc (Id));
|
||||
Set_Contract (Id, Items);
|
||||
end if;
|
||||
|
||||
-- Contract items related to constants. Applicable pragmas are:
|
||||
-- Part_Of
|
||||
|
||||
if Ekind (Id) = E_Constant then
|
||||
if Prag_Nam = Name_Part_Of then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to [generic] packages or instantiations. The
|
||||
-- applicable pragmas are:
|
||||
-- Abstract_States
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of (instantiation only)
|
||||
|
||||
elsif Ekind_In (Id, E_Generic_Package, E_Package) then
|
||||
if Nam_In (Prag_Nam, Name_Abstract_State,
|
||||
Name_Initial_Condition,
|
||||
Name_Initializes)
|
||||
then
|
||||
Add_Classification;
|
||||
|
||||
-- Indicator Part_Of must be associated with a package instantiation
|
||||
|
||||
elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to package bodies. The applicable pragmas are:
|
||||
-- Refined_States
|
||||
|
||||
elsif Ekind (Id) = E_Package_Body then
|
||||
if Prag_Nam = Name_Refined_State then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to subprogram or entry declarations. The
|
||||
-- applicable pragmas are:
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Extensions_Visible
|
||||
-- Global
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Test_Case
|
||||
-- Volatile_Function
|
||||
|
||||
elsif Ekind_In (Id, E_Entry, E_Entry_Family)
|
||||
or else Is_Generic_Subprogram (Id)
|
||||
or else Is_Subprogram (Id)
|
||||
then
|
||||
if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then
|
||||
Add_Pre_Post_Condition;
|
||||
|
||||
elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then
|
||||
Add_Contract_Test_Case;
|
||||
|
||||
elsif Nam_In (Prag_Nam, Name_Depends,
|
||||
Name_Extensions_Visible,
|
||||
Name_Global)
|
||||
then
|
||||
Add_Classification;
|
||||
|
||||
elsif Prag_Nam = Name_Volatile_Function
|
||||
and then Ekind_In (Id, E_Function, E_Generic_Function)
|
||||
then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to subprogram bodies. Applicable pragmas are:
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
|
||||
elsif Ekind (Id) = E_Subprogram_Body then
|
||||
if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then
|
||||
Add_Classification;
|
||||
|
||||
elsif Nam_In (Prag_Nam, Name_Postcondition,
|
||||
Name_Precondition,
|
||||
Name_Refined_Post)
|
||||
then
|
||||
Add_Pre_Post_Condition;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
|
||||
-- Contract items related to variables. Applicable pragmas are:
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
-- Constant_After_Elaboration
|
||||
-- Effective_Reads
|
||||
-- Effective_Writes
|
||||
-- Part_Of
|
||||
|
||||
elsif Ekind (Id) = E_Variable then
|
||||
if Nam_In (Prag_Nam, Name_Async_Readers,
|
||||
Name_Async_Writers,
|
||||
Name_Constant_After_Elaboration,
|
||||
Name_Effective_Reads,
|
||||
Name_Effective_Writes,
|
||||
Name_Part_Of)
|
||||
then
|
||||
Add_Classification;
|
||||
|
||||
-- The pragma is not a proper contract item
|
||||
|
||||
else
|
||||
raise Program_Error;
|
||||
end if;
|
||||
end if;
|
||||
end Add_Contract_Item;
|
||||
|
||||
----------------------------
|
||||
-- Add_Global_Declaration --
|
||||
----------------------------
|
||||
|
|
@ -3692,6 +3488,231 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Check_Unprotected_Access;
|
||||
|
||||
------------------------------
|
||||
-- Check_Unused_Body_States --
|
||||
------------------------------
|
||||
|
||||
procedure Check_Unused_Body_States (Body_Id : Entity_Id) is
|
||||
Legal_Constits : Boolean := True;
|
||||
-- This flag designates whether all constituents of pragma Refined_State
|
||||
-- are legal. The flag is used to suppress the generation of potentially
|
||||
-- misleading error messages due to a malformed pragma.
|
||||
|
||||
procedure Process_Refinement_Clause
|
||||
(Clause : Node_Id;
|
||||
States : Elist_Id);
|
||||
-- Inspect all constituents of refinement clause Clause and remove any
|
||||
-- matches from body state list States.
|
||||
|
||||
-------------------------------
|
||||
-- Process_Refinement_Clause --
|
||||
-------------------------------
|
||||
|
||||
procedure Process_Refinement_Clause
|
||||
(Clause : Node_Id;
|
||||
States : Elist_Id)
|
||||
is
|
||||
procedure Process_Constituent (Constit : Node_Id);
|
||||
-- Remove constituent Constit from body state list States
|
||||
|
||||
-------------------------
|
||||
-- Process_Constituent --
|
||||
-------------------------
|
||||
|
||||
procedure Process_Constituent (Constit : Node_Id) is
|
||||
Constit_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
if Error_Posted (Constit) then
|
||||
Legal_Constits := False;
|
||||
end if;
|
||||
|
||||
-- Guard against illegal constituents. Only abstract states and
|
||||
-- objects can appear on the right hand side of a refinement.
|
||||
|
||||
if Is_Entity_Name (Constit) then
|
||||
Constit_Id := Entity_Of (Constit);
|
||||
|
||||
if Present (Constit_Id)
|
||||
and then Ekind_In (Constit_Id, E_Abstract_State,
|
||||
E_Constant,
|
||||
E_Variable)
|
||||
then
|
||||
Remove (States, Constit_Id);
|
||||
end if;
|
||||
end if;
|
||||
end Process_Constituent;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Constit : Node_Id;
|
||||
|
||||
-- Start of processing for Process_Refinement_Clause
|
||||
|
||||
begin
|
||||
if Nkind (Clause) = N_Component_Association then
|
||||
Constit := Expression (Clause);
|
||||
|
||||
-- Multiple constituents appear as an aggregate
|
||||
|
||||
if Nkind (Constit) = N_Aggregate then
|
||||
Constit := First (Expressions (Constit));
|
||||
while Present (Constit) loop
|
||||
Process_Constituent (Constit);
|
||||
Next (Constit);
|
||||
end loop;
|
||||
|
||||
-- Various forms of a single constituent
|
||||
|
||||
else
|
||||
Process_Constituent (Constit);
|
||||
end if;
|
||||
end if;
|
||||
end Process_Refinement_Clause;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Prag : constant Node_Id :=
|
||||
Get_Pragma (Body_Id, Pragma_Refined_State);
|
||||
Spec_Id : constant Entity_Id := Spec_Entity (Body_Id);
|
||||
Clause : Node_Id;
|
||||
States : Elist_Id;
|
||||
|
||||
-- Start of processing for Check_Unused_Body_States
|
||||
|
||||
begin
|
||||
-- Inspect the clauses of pragma Refined_State and determine whether all
|
||||
-- visible states declared within the body of the package participate in
|
||||
-- the refinement.
|
||||
|
||||
if Present (Prag) then
|
||||
Clause := Expression (Get_Argument (Prag, Spec_Id));
|
||||
States := Collect_Body_States (Body_Id);
|
||||
|
||||
-- Multiple non-null state refinements appear as an aggregate
|
||||
|
||||
if Nkind (Clause) = N_Aggregate then
|
||||
Clause := First (Component_Associations (Clause));
|
||||
while Present (Clause) loop
|
||||
Process_Refinement_Clause (Clause, States);
|
||||
Next (Clause);
|
||||
end loop;
|
||||
|
||||
-- Various forms of a single state refinement
|
||||
|
||||
else
|
||||
Process_Refinement_Clause (Clause, States);
|
||||
end if;
|
||||
|
||||
-- Ensure that all abstract states and objects declared in the body
|
||||
-- state space of the related package are utilized as constituents.
|
||||
|
||||
if Legal_Constits then
|
||||
Report_Unused_Body_States (Body_Id, States);
|
||||
end if;
|
||||
end if;
|
||||
end Check_Unused_Body_States;
|
||||
|
||||
-------------------------
|
||||
-- Collect_Body_States --
|
||||
-------------------------
|
||||
|
||||
function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id is
|
||||
procedure Collect_Visible_States
|
||||
(Pack_Id : Entity_Id;
|
||||
States : in out Elist_Id);
|
||||
-- Gather the entities of all abstract states and objects declared in
|
||||
-- the visible state space of package Pack_Id.
|
||||
|
||||
----------------------------
|
||||
-- Collect_Visible_States --
|
||||
----------------------------
|
||||
|
||||
procedure Collect_Visible_States
|
||||
(Pack_Id : Entity_Id;
|
||||
States : in out Elist_Id)
|
||||
is
|
||||
Item_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
-- Traverse the entity chain of the package and inspect all visible
|
||||
-- items.
|
||||
|
||||
Item_Id := First_Entity (Pack_Id);
|
||||
while Present (Item_Id) and then not In_Private_Part (Item_Id) loop
|
||||
|
||||
-- Do not consider internally generated items as those cannot be
|
||||
-- named and participate in refinement.
|
||||
|
||||
if not Comes_From_Source (Item_Id) then
|
||||
null;
|
||||
|
||||
elsif Ekind (Item_Id) = E_Abstract_State then
|
||||
Append_New_Elmt (Item_Id, States);
|
||||
|
||||
-- Do not consider objects that map generic formals to their
|
||||
-- actuals, as the formals cannot be named from the outside and
|
||||
-- participate in refinement.
|
||||
|
||||
elsif Ekind_In (Item_Id, E_Constant, E_Variable)
|
||||
and then No (Corresponding_Generic_Association
|
||||
(Declaration_Node (Item_Id)))
|
||||
then
|
||||
Append_New_Elmt (Item_Id, States);
|
||||
|
||||
-- Recursively gather the visible states of a nested package
|
||||
|
||||
elsif Ekind (Item_Id) = E_Package then
|
||||
Collect_Visible_States (Item_Id, States);
|
||||
end if;
|
||||
|
||||
Next_Entity (Item_Id);
|
||||
end loop;
|
||||
end Collect_Visible_States;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
|
||||
Decl : Node_Id;
|
||||
Item_Id : Entity_Id;
|
||||
States : Elist_Id := No_Elist;
|
||||
|
||||
-- Start of processing for Collect_Body_States
|
||||
|
||||
begin
|
||||
-- Inspect the declarations of the body looking for source objects,
|
||||
-- packages and package instantiations.
|
||||
|
||||
Decl := First (Declarations (Body_Decl));
|
||||
while Present (Decl) loop
|
||||
|
||||
-- Capture source objects as internally generated temporaries cannot
|
||||
-- be named and participate in refinement.
|
||||
|
||||
if Nkind (Decl) = N_Object_Declaration then
|
||||
Item_Id := Defining_Entity (Decl);
|
||||
|
||||
if Comes_From_Source (Item_Id) then
|
||||
Append_New_Elmt (Item_Id, States);
|
||||
end if;
|
||||
|
||||
-- Capture the visible abstract states and objects of a source
|
||||
-- package [instantiation].
|
||||
|
||||
elsif Nkind (Decl) = N_Package_Declaration then
|
||||
Item_Id := Defining_Entity (Decl);
|
||||
|
||||
if Comes_From_Source (Item_Id) then
|
||||
Collect_Visible_States (Item_Id, States);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
end loop;
|
||||
|
||||
return States;
|
||||
end Collect_Body_States;
|
||||
|
||||
------------------------
|
||||
-- Collect_Interfaces --
|
||||
------------------------
|
||||
|
|
@ -4766,147 +4787,6 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Corresponding_Spec_Of;
|
||||
|
||||
-----------------------------
|
||||
-- Create_Generic_Contract --
|
||||
-----------------------------
|
||||
|
||||
procedure Create_Generic_Contract (Unit : Node_Id) is
|
||||
Templ : constant Node_Id := Original_Node (Unit);
|
||||
Templ_Id : constant Entity_Id := Defining_Entity (Templ);
|
||||
|
||||
procedure Add_Generic_Contract_Pragma (Prag : Node_Id);
|
||||
-- Add a single contract-related source pragma Prag to the contract of
|
||||
-- generic template Templ_Id.
|
||||
|
||||
---------------------------------
|
||||
-- Add_Generic_Contract_Pragma --
|
||||
---------------------------------
|
||||
|
||||
procedure Add_Generic_Contract_Pragma (Prag : Node_Id) is
|
||||
Prag_Templ : Node_Id;
|
||||
|
||||
begin
|
||||
-- Mark the pragma to prevent the premature capture of global
|
||||
-- references when capturing global references of the context
|
||||
-- (see Save_References_In_Pragma).
|
||||
|
||||
Set_Is_Generic_Contract_Pragma (Prag);
|
||||
|
||||
-- Pragmas that apply to a generic subprogram declaration are not
|
||||
-- part of the semantic structure of the generic template:
|
||||
|
||||
-- generic
|
||||
-- procedure Example (Formal : Integer);
|
||||
-- pragma Precondition (Formal > 0);
|
||||
|
||||
-- Create a generic template for such pragmas and link the template
|
||||
-- of the pragma with the generic template.
|
||||
|
||||
if Nkind (Templ) = N_Generic_Subprogram_Declaration then
|
||||
Rewrite
|
||||
(Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False));
|
||||
Prag_Templ := Original_Node (Prag);
|
||||
|
||||
Set_Is_Generic_Contract_Pragma (Prag_Templ);
|
||||
Add_Contract_Item (Prag_Templ, Templ_Id);
|
||||
|
||||
-- Otherwise link the pragma with the generic template
|
||||
|
||||
else
|
||||
Add_Contract_Item (Prag, Templ_Id);
|
||||
end if;
|
||||
end Add_Generic_Contract_Pragma;
|
||||
|
||||
-- Local variables
|
||||
|
||||
Context : constant Node_Id := Parent (Unit);
|
||||
Decl : Node_Id := Empty;
|
||||
|
||||
-- Start of processing for Create_Generic_Contract
|
||||
|
||||
begin
|
||||
-- A generic package declaration carries contract-related source pragmas
|
||||
-- in its visible declarations.
|
||||
|
||||
if Nkind (Templ) = N_Generic_Package_Declaration then
|
||||
Set_Ekind (Templ_Id, E_Generic_Package);
|
||||
|
||||
if Present (Visible_Declarations (Specification (Templ))) then
|
||||
Decl := First (Visible_Declarations (Specification (Templ)));
|
||||
end if;
|
||||
|
||||
-- A generic package body carries contract-related source pragmas in its
|
||||
-- declarations.
|
||||
|
||||
elsif Nkind (Templ) = N_Package_Body then
|
||||
Set_Ekind (Templ_Id, E_Package_Body);
|
||||
|
||||
if Present (Declarations (Templ)) then
|
||||
Decl := First (Declarations (Templ));
|
||||
end if;
|
||||
|
||||
-- Generic subprogram declaration
|
||||
|
||||
elsif Nkind (Templ) = N_Generic_Subprogram_Declaration then
|
||||
if Nkind (Specification (Templ)) = N_Function_Specification then
|
||||
Set_Ekind (Templ_Id, E_Generic_Function);
|
||||
else
|
||||
Set_Ekind (Templ_Id, E_Generic_Procedure);
|
||||
end if;
|
||||
|
||||
-- When the generic subprogram acts as a compilation unit, inspect
|
||||
-- the Pragmas_After list for contract-related source pragmas.
|
||||
|
||||
if Nkind (Context) = N_Compilation_Unit then
|
||||
if Present (Aux_Decls_Node (Context))
|
||||
and then Present (Pragmas_After (Aux_Decls_Node (Context)))
|
||||
then
|
||||
Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
|
||||
end if;
|
||||
|
||||
-- Otherwise inspect the successive declarations for contract-related
|
||||
-- source pragmas.
|
||||
|
||||
else
|
||||
Decl := Next (Unit);
|
||||
end if;
|
||||
|
||||
-- A generic subprogram body carries contract-related source pragmas in
|
||||
-- its declarations.
|
||||
|
||||
elsif Nkind (Templ) = N_Subprogram_Body then
|
||||
Set_Ekind (Templ_Id, E_Subprogram_Body);
|
||||
|
||||
if Present (Declarations (Templ)) then
|
||||
Decl := First (Declarations (Templ));
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Inspect the relevant declarations looking for contract-related source
|
||||
-- pragmas and add them to the contract of the generic unit.
|
||||
|
||||
while Present (Decl) loop
|
||||
if Comes_From_Source (Decl) then
|
||||
if Nkind (Decl) = N_Pragma then
|
||||
|
||||
-- The source pragma is a contract annotation
|
||||
|
||||
if Is_Contract_Annotation (Decl) then
|
||||
Add_Generic_Contract_Pragma (Decl);
|
||||
end if;
|
||||
|
||||
-- The region where a contract-related source pragma may appear
|
||||
-- ends with the first source non-pragma declaration or statement.
|
||||
|
||||
else
|
||||
exit;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next (Decl);
|
||||
end loop;
|
||||
end Create_Generic_Contract;
|
||||
|
||||
--------------------
|
||||
-- Current_Entity --
|
||||
--------------------
|
||||
|
|
@ -10249,53 +10129,6 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Inherit_Rep_Item_Chain;
|
||||
|
||||
---------------------------------
|
||||
-- Inherit_Subprogram_Contract --
|
||||
---------------------------------
|
||||
|
||||
procedure Inherit_Subprogram_Contract
|
||||
(Subp : Entity_Id;
|
||||
From_Subp : Entity_Id)
|
||||
is
|
||||
procedure Inherit_Pragma (Prag_Id : Pragma_Id);
|
||||
-- Propagate a pragma denoted by Prag_Id from From_Subp's contract to
|
||||
-- Subp's contract.
|
||||
|
||||
--------------------
|
||||
-- Inherit_Pragma --
|
||||
--------------------
|
||||
|
||||
procedure Inherit_Pragma (Prag_Id : Pragma_Id) is
|
||||
Prag : constant Node_Id := Get_Pragma (From_Subp, Prag_Id);
|
||||
New_Prag : Node_Id;
|
||||
|
||||
begin
|
||||
-- A pragma cannot be part of more than one First_Pragma/Next_Pragma
|
||||
-- chains, therefore the node must be replicated. The new pragma is
|
||||
-- flagged is inherited for distrinction purposes.
|
||||
|
||||
if Present (Prag) then
|
||||
New_Prag := New_Copy_Tree (Prag);
|
||||
Set_Is_Inherited (New_Prag);
|
||||
|
||||
Add_Contract_Item (New_Prag, Subp);
|
||||
end if;
|
||||
end Inherit_Pragma;
|
||||
|
||||
-- Start of processing for Inherit_Subprogram_Contract
|
||||
|
||||
begin
|
||||
-- Inheritance is carried out only when both entities are subprograms
|
||||
-- with contracts.
|
||||
|
||||
if Is_Subprogram_Or_Generic_Subprogram (Subp)
|
||||
and then Is_Subprogram_Or_Generic_Subprogram (From_Subp)
|
||||
and then Present (Contract (From_Subp))
|
||||
then
|
||||
Inherit_Pragma (Pragma_Extensions_Visible);
|
||||
end if;
|
||||
end Inherit_Subprogram_Contract;
|
||||
|
||||
---------------------------------
|
||||
-- Insert_Explicit_Dereference --
|
||||
---------------------------------
|
||||
|
|
@ -17171,6 +17004,63 @@ package body Sem_Util is
|
|||
(Boolean_Literals (not Range_Checks_Suppressed (E)), Loc);
|
||||
end Rep_To_Pos_Flag;
|
||||
|
||||
-------------------------------
|
||||
-- Report_Unused_Body_States --
|
||||
-------------------------------
|
||||
|
||||
procedure Report_Unused_Body_States
|
||||
(Body_Id : Entity_Id;
|
||||
States : Elist_Id)
|
||||
is
|
||||
Posted : Boolean := False;
|
||||
State_Elmt : Elmt_Id;
|
||||
State_Id : Entity_Id;
|
||||
|
||||
begin
|
||||
if Present (States) then
|
||||
State_Elmt := First_Elmt (States);
|
||||
while Present (State_Elmt) loop
|
||||
State_Id := Node (State_Elmt);
|
||||
|
||||
-- Constants are part of the hidden state of a package, but the
|
||||
-- compiler cannot determine whether they have variable input
|
||||
-- (SPARK RM 7.1.1(2)) and cannot classify them properly as a
|
||||
-- hidden state. Do not emit an error when a constant does not
|
||||
-- participate in a state refinement, even though it acts as a
|
||||
-- hidden state.
|
||||
|
||||
if Ekind (State_Id) = E_Constant then
|
||||
null;
|
||||
|
||||
-- Generate an error message of the form:
|
||||
|
||||
-- body of package ... has unused hidden states
|
||||
-- abstract state ... defined at ...
|
||||
-- variable ... defined at ...
|
||||
|
||||
else
|
||||
if not Posted then
|
||||
Posted := True;
|
||||
SPARK_Msg_N
|
||||
("body of package & has unused hidden states", Body_Id);
|
||||
end if;
|
||||
|
||||
Error_Msg_Sloc := Sloc (State_Id);
|
||||
|
||||
if Ekind (State_Id) = E_Abstract_State then
|
||||
SPARK_Msg_NE
|
||||
("\abstract state & defined #", Body_Id, State_Id);
|
||||
|
||||
else
|
||||
SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
Next_Elmt (State_Elmt);
|
||||
end loop;
|
||||
end if;
|
||||
end Report_Unused_Body_States;
|
||||
|
||||
--------------------
|
||||
-- Require_Entity --
|
||||
--------------------
|
||||
|
|
|
|||
|
|
@ -49,32 +49,6 @@ package Sem_Util is
|
|||
-- it the identifier of the block. Id denotes the generated entity. If the
|
||||
-- block already has an identifier, Id returns the entity of its label.
|
||||
|
||||
procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id);
|
||||
-- Add pragma Prag to the contract of a constant, entry, package [body],
|
||||
-- subprogram [body] or variable denoted by Id. The following are valid
|
||||
-- pragmas:
|
||||
-- Abstract_State
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
-- Constant_After_Elaboration
|
||||
-- Contract_Cases
|
||||
-- Depends
|
||||
-- Effective_Reads
|
||||
-- Effective_Writes
|
||||
-- Extensions_Visible
|
||||
-- Global
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
-- Part_Of
|
||||
-- Postcondition
|
||||
-- Precondition
|
||||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_Post
|
||||
-- Refined_States
|
||||
-- Test_Case
|
||||
-- Volatile_Function
|
||||
|
||||
procedure Add_Global_Declaration (N : Node_Id);
|
||||
-- These procedures adds a declaration N at the library level, to be
|
||||
-- elaborated before any other code in the unit. It is used for example
|
||||
|
|
@ -276,6 +250,14 @@ package Sem_Util is
|
|||
-- error message on node N. Used in object declarations, type conversions
|
||||
-- and qualified expressions.
|
||||
|
||||
procedure Check_Function_With_Address_Parameter (Subp_Id : Entity_Id);
|
||||
-- A subprogram that has an Address parameter and is declared in a Pure
|
||||
-- package is not considered Pure, because the parameter may be used as a
|
||||
-- pointer and the referenced data may change even if the address value
|
||||
-- itself does not.
|
||||
-- If the programmer gave an explicit Pure_Function pragma, then we respect
|
||||
-- the pragma and leave the subprogram Pure.
|
||||
|
||||
procedure Check_Function_Writable_Actuals (N : Node_Id);
|
||||
-- (Ada 2012): If the construct N has two or more direct constituents that
|
||||
-- are names or expressions whose evaluation may occur in an arbitrary
|
||||
|
|
@ -322,19 +304,20 @@ package Sem_Util is
|
|||
-- N is one of the statement forms that is a potentially blocking
|
||||
-- operation. If it appears within a protected action, emit warning.
|
||||
|
||||
procedure Check_Function_With_Address_Parameter (Subp_Id : Entity_Id);
|
||||
-- A subprogram that has an Address parameter and is declared in a Pure
|
||||
-- package is not considered Pure, because the parameter may be used as a
|
||||
-- pointer and the referenced data may change even if the address value
|
||||
-- itself does not.
|
||||
-- If the programmer gave an explicit Pure_Function pragma, then we respect
|
||||
-- the pragma and leave the subprogram Pure.
|
||||
|
||||
procedure Check_Result_And_Post_State (Subp_Id : Entity_Id);
|
||||
-- Determine whether the contract of subprogram Subp_Id mentions attribute
|
||||
-- 'Result and it contains an expression that evaluates differently in pre-
|
||||
-- and post-state.
|
||||
|
||||
procedure Check_Unused_Body_States (Body_Id : Entity_Id);
|
||||
-- Verify that all abstract states and object declared in the state space
|
||||
-- of a package body denoted by entity Body_Id are used as constituents.
|
||||
-- Emit an error if this is not the case.
|
||||
|
||||
function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id;
|
||||
-- Gather the entities of all abstract states and objects declared in the
|
||||
-- body state space of package body Body_Id.
|
||||
|
||||
procedure Check_Unprotected_Access
|
||||
(Context : Node_Id;
|
||||
Expr : Node_Id);
|
||||
|
|
@ -434,11 +417,6 @@ package Sem_Util is
|
|||
-- Return the corresponding spec of Decl when it denotes a package or a
|
||||
-- subprogram [stub], or the defining entity of Decl.
|
||||
|
||||
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.
|
||||
|
||||
function Current_Entity (N : Node_Id) return Entity_Id;
|
||||
pragma Inline (Current_Entity);
|
||||
-- Find the currently visible definition for a given identifier, that is to
|
||||
|
|
@ -1159,14 +1137,6 @@ package Sem_Util is
|
|||
-- Inherit the rep item chain of type From_Typ without clobbering any
|
||||
-- existing rep items on Typ's chain. Typ is the destination type.
|
||||
|
||||
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 Insert_Explicit_Dereference (N : Node_Id);
|
||||
-- In a context that requires a composite or subprogram type and where a
|
||||
-- prefix is an access type, rewrite the access type node N (which is the
|
||||
|
|
@ -1877,6 +1847,13 @@ package Sem_Util is
|
|||
-- more there is at least one case in the generated code (the code for
|
||||
-- array assignment in a loop) that depends on this suppression.
|
||||
|
||||
procedure Report_Unused_Body_States
|
||||
(Body_Id : Entity_Id;
|
||||
States : Elist_Id);
|
||||
-- Emit errors for each abstract state or object found in list States that
|
||||
-- is declared in package body Body_Id, but is not used as constituent in a
|
||||
-- state refinement.
|
||||
|
||||
procedure Require_Entity (N : Node_Id);
|
||||
-- N is a node which should have an entity value if it is an entity name.
|
||||
-- If not, then check if there were previous errors. If so, just fill
|
||||
|
|
|
|||
|
|
@ -1860,6 +1860,14 @@ package body Sinfo is
|
|||
return Flag11 (N);
|
||||
end Is_Expanded_Build_In_Place_Call;
|
||||
|
||||
function Is_Expanded_Contract
|
||||
(N : Node_Id) return Boolean is
|
||||
begin
|
||||
pragma Assert (False
|
||||
or else NT (N).Nkind = N_Contract);
|
||||
return Flag1 (N);
|
||||
end Is_Expanded_Contract;
|
||||
|
||||
function Is_Finalization_Wrapper
|
||||
(N : Node_Id) return Boolean is
|
||||
begin
|
||||
|
|
@ -5073,6 +5081,14 @@ package body Sinfo is
|
|||
Set_Flag11 (N, Val);
|
||||
end Set_Is_Expanded_Build_In_Place_Call;
|
||||
|
||||
procedure Set_Is_Expanded_Contract
|
||||
(N : Node_Id; Val : Boolean := True) is
|
||||
begin
|
||||
pragma Assert (False
|
||||
or else NT (N).Nkind = N_Contract);
|
||||
Set_Flag1 (N, Val);
|
||||
end Set_Is_Expanded_Contract;
|
||||
|
||||
procedure Set_Is_Finalization_Wrapper
|
||||
(N : Node_Id; Val : Boolean := True) is
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -1542,6 +1542,10 @@ package Sinfo is
|
|||
-- is called in a dispatching context. Used to prevent a formal/actual
|
||||
-- mismatch when the call is rewritten as a dispatching call.
|
||||
|
||||
-- Is_Expanded_Contract (Flag1-Sem)
|
||||
-- Present in N_Contract nodes. Set if the contract has already undergone
|
||||
-- expansion activities.
|
||||
|
||||
-- Is_Asynchronous_Call_Block (Flag7-Sem)
|
||||
-- A flag set in a Block_Statement node to indicate that it is the
|
||||
-- expansion of an asynchronous entry call. Such a block needs cleanup
|
||||
|
|
@ -7564,6 +7568,7 @@ package Sinfo is
|
|||
-- Pre_Post_Conditions (Node1-Sem) (set to Empty if none)
|
||||
-- Contract_Test_Cases (Node2-Sem) (set to Empty if none)
|
||||
-- Classifications (Node3-Sem) (set to Empty if none)
|
||||
-- Is_Expanded_Contract (Flag1-Sem)
|
||||
|
||||
-- Pre_Post_Conditions contains a collection of pragmas that correspond
|
||||
-- to pre- and postconditions associated with an entry or a subprogram
|
||||
|
|
@ -7592,9 +7597,11 @@ package Sinfo is
|
|||
-- Abstract_States
|
||||
-- Async_Readers
|
||||
-- Async_Writers
|
||||
-- Constant_After_Elaboration
|
||||
-- Depends
|
||||
-- Effective_Reads
|
||||
-- Effective_Writes
|
||||
-- Extensions_Visible
|
||||
-- Global
|
||||
-- Initial_Condition
|
||||
-- Initializes
|
||||
|
|
@ -7602,6 +7609,7 @@ package Sinfo is
|
|||
-- Refined_Depends
|
||||
-- Refined_Global
|
||||
-- Refined_States
|
||||
-- Volatile_Function
|
||||
-- The ordering is in LIFO fashion.
|
||||
|
||||
-------------------
|
||||
|
|
@ -9322,6 +9330,9 @@ package Sinfo is
|
|||
function Is_Expanded_Build_In_Place_Call
|
||||
(N : Node_Id) return Boolean; -- Flag11
|
||||
|
||||
function Is_Expanded_Contract
|
||||
(N : Node_Id) return Boolean; -- Flag1
|
||||
|
||||
function Is_Finalization_Wrapper
|
||||
(N : Node_Id) return Boolean; -- Flag9
|
||||
|
||||
|
|
@ -10348,6 +10359,9 @@ package Sinfo is
|
|||
procedure Set_Is_Expanded_Build_In_Place_Call
|
||||
(N : Node_Id; Val : Boolean := True); -- Flag11
|
||||
|
||||
procedure Set_Is_Expanded_Contract
|
||||
(N : Node_Id; Val : Boolean := True); -- Flag1
|
||||
|
||||
procedure Set_Is_Finalization_Wrapper
|
||||
(N : Node_Id; Val : Boolean := True); -- Flag9
|
||||
|
||||
|
|
@ -12748,6 +12762,7 @@ package Sinfo is
|
|||
pragma Inline (Is_Elsif);
|
||||
pragma Inline (Is_Entry_Barrier_Function);
|
||||
pragma Inline (Is_Expanded_Build_In_Place_Call);
|
||||
pragma Inline (Is_Expanded_Contract);
|
||||
pragma Inline (Is_Finalization_Wrapper);
|
||||
pragma Inline (Is_Folded_In_Parser);
|
||||
pragma Inline (Is_Generic_Contract_Pragma);
|
||||
|
|
@ -13085,6 +13100,7 @@ package Sinfo is
|
|||
pragma Inline (Set_Is_Elsif);
|
||||
pragma Inline (Set_Is_Entry_Barrier_Function);
|
||||
pragma Inline (Set_Is_Expanded_Build_In_Place_Call);
|
||||
pragma Inline (Set_Is_Expanded_Contract);
|
||||
pragma Inline (Set_Is_Finalization_Wrapper);
|
||||
pragma Inline (Set_Is_Folded_In_Parser);
|
||||
pragma Inline (Set_Is_Generic_Contract_Pragma);
|
||||
|
|
|
|||
|
|
@ -127,7 +127,7 @@ package body Switch.B is
|
|||
-- A little check, "gnat" at the start of a switch is not allowed except
|
||||
-- for the compiler
|
||||
|
||||
if Switch_Chars'Last >= Ptr + 3
|
||||
if Max >= Ptr + 3
|
||||
and then Switch_Chars (Ptr .. Ptr + 3) = "gnat"
|
||||
then
|
||||
Osint.Fail ("invalid switch: """ & Switch_Chars & """"
|
||||
|
|
@ -229,8 +229,28 @@ package body Switch.B is
|
|||
-- Processing for E switch
|
||||
|
||||
when 'E' =>
|
||||
Ptr := Ptr + 1;
|
||||
|
||||
-- -E is equivalent to -Ea (see below)
|
||||
|
||||
Exception_Tracebacks := True;
|
||||
Ptr := Ptr + 1;
|
||||
|
||||
if Ptr <= Max then
|
||||
case Switch_Chars (Ptr) is
|
||||
|
||||
-- -Ea sets Exception_Tracebacks
|
||||
|
||||
when 'a' => null;
|
||||
|
||||
-- -Es sets both Exception_Tracebacks and
|
||||
-- Exception_Tracebacks_Symbolic.
|
||||
|
||||
when 's' => Exception_Tracebacks_Symbolic := True;
|
||||
when others => Bad_Switch (Switch_Chars);
|
||||
end case;
|
||||
|
||||
Ptr := Ptr + 1;
|
||||
end if;
|
||||
|
||||
-- Processing for F switch
|
||||
|
||||
|
|
@ -542,13 +562,11 @@ package body Switch.B is
|
|||
declare
|
||||
Src_Path_Name : constant String_Ptr :=
|
||||
Get_RTS_Search_Dir
|
||||
(Switch_Chars
|
||||
(Ptr + 1 .. Switch_Chars'Last),
|
||||
(Switch_Chars (Ptr + 1 .. Max),
|
||||
Include);
|
||||
Lib_Path_Name : constant String_Ptr :=
|
||||
Get_RTS_Search_Dir
|
||||
(Switch_Chars
|
||||
(Ptr + 1 .. Switch_Chars'Last),
|
||||
(Switch_Chars (Ptr + 1 .. Max),
|
||||
Objects);
|
||||
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 2001-2007, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 2001-2015, 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- --
|
||||
|
|
@ -32,7 +32,7 @@
|
|||
package Switch.B is
|
||||
|
||||
procedure Scan_Binder_Switches (Switch_Chars : String);
|
||||
-- Procedures to scan out binder switches stored in the given string.
|
||||
-- Procedure to scan out binder switches stored in the given string.
|
||||
-- The first character is known to be a valid switch character, and there
|
||||
-- are no blanks or other switch terminator characters in the string, so
|
||||
-- the entire string should consist of valid switch characters, except that
|
||||
|
|
|
|||
Loading…
Reference in New Issue