+2015-11-18 Nicolas Roche <roche@adacore.com>
+
+ * sysdep.c (__gnat_localtime_tzoff): On Windows platform
+ GetTimeZoneInformation function is thread-safe. Thus there
+ is no need to lock the runtime in the implementation of
+ __gnat_localtime_tzoff on that platform.
+
+2015-11-18 Eric Botcazou <ebotcazou@adacore.com>
+
+ * s-arit64.adb (To_Neg_Int): Add a special case for 2**63 input.
+
+2015-11-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * contracts.adb (Analyze_Contracts): New routine.
+ (Analyze_Enclosing_Package_Body_Contract): Removed.
+ (Analyze_Entry_Or_Subprogram_Contract): Add formal parameter
+ Freeze_Id. Propagate the entity of the freezing body to vaious
+ analysis routines.
+ (Analyze_Initial_Declaration_Contract): Removed.
+ (Analyze_Object_Contract): Add formal parameter
+ Freeze_Id. Propagate the entity of the freezing body to vaious
+ analysis routines.
+ (Analyze_Previous_Contracts): New routine.
+ * contracts.ads (Analyze_Enclosing_Package_Body_Contract): Removed.
+ (Analyze_Contracts): New routine.
+ (Analyze_Entry_Or_Subprogram_Contract): Add formal
+ parameter Freeze_Id and update the comment on usage.
+ (Analyze_Initial_Declaration_Contract): Removed.
+ (Analyze_Object_Contract): Add formal parameter Freeze_Id and
+ update the comment on usage.
+ (Analyze_Previous_Contracts): New routine.
+ * sem_ch3.adb (Analyze_Declarations): Use Analyze_Contracts to
+ analyze all contracts of eligible constructs.
+ * sem_ch6.adb (Analyze_Generic_Subprogram_Body):
+ A body no longer freezes the contract of its initial
+ declaration. This effect is achieved through different means.
+ (Analyze_Subprogram_Body_Helper): A body now freezes the contracts
+ of all eligible constructs that precede it. A body no longer
+ freezes the contract of its initial declaration. This effect is
+ achieved through different means.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): A body now freezes
+ the contracts of all eligible constructs that precede it. A body
+ no longer freezes the contract of its initial declaration. This
+ effect is achieved through different means.
+ * sem_ch9.adb (Analyze_Entry_Body): A body now freezes
+ the contracts of all eligible constructs that precede
+ it. A body no longer freezes the contract of its initial
+ declaration. This effect is achieved through different means.
+ (Analyze_Protected_Body): A body now freezes the contracts
+ of all eligible constructs that precede it. A body no longer
+ freezes the contract of its initial declaration. This effect
+ is achieved through different means.
+ (Analyze_Task_Body): A
+ body now freezes the contracts of all eligible constructs that
+ precede it. A body no longer freezes the contract of its initial
+ declaration. This effect is achieved through different means.
+ * sem_prag.adb (Add_Item_To_Name_Buffer): Single protected/task
+ objects now output their respective current instance of xxx
+ type messages. (Analyze_Contract_Cases_In_Decl_Part): Add
+ formal parameter Freeze_Id. Emit a clarification message
+ when an undefined entity may the byproduct of contract
+ freezing.
+ (Analyze_Part_Of_In_Decl_Part): Add formal
+ parameter Freeze_Id. Emit a clarification message when an
+ undefined entity may the byproduct of contract freezing.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Add formal
+ parameter Freeze_Id. Emit a clarification message when an
+ undefined entity may the byproduct of contract freezing.
+ (Analyze_Refined_State_In_Decl_Part): Do not report unused body
+ states as constituents of single protected/task types may not
+ bave been identified yet.
+ (Collect_Subprogram_Inputs_Outputs):
+ Reimplemented. (Contract_Freeze_Error): New routine.
+ (Process_Overloadable): Use predicate Is_Single_Task_Object.
+ * sem_prag.ads (Analyze_Contract_Cases_In_Decl_Part):
+ Add formal parameter Freeze_Id and update the comment
+ on usage.
+ (Analyze_Part_Of_In_Decl_Part): Add formal
+ parameter Freeze_Id and update the comment on usage.
+ (Analyze_Pre_Post_Condition_In_Decl_Part): Add formal parameter
+ Freeze_Id and update the comment on usage.
+ * sem_util.adb (Check_Unused_Body_States): Remove global
+ variable Legal_Constits. The routine now reports unused
+ body states regardless of whether constituents are
+ legal or not.
+ (Collect_Body_States): A constituent of a
+ single protected/task type is not a visible state of a
+ package body.
+ (Collect_Visible_States): A constituent
+ of a single protected/task type is not a visible
+ state of a package body.
+ (Has_Undefined_Reference): New routine.
+ (Is_Single_Concurrent_Object): Reimplemented.
+ (Is_Single_Protected_Object): New routine.
+ (Is_Single_Task_Object): New routine.
+ (Is_Visible_Object): New routine.
+ (Report_Unused_Body_States): Moved to Check_Unused_Body_States.
+ * sem_util.ads (Check_Unused_Body_States): Update the comment on usage.
+ (Has_Undefined_Reference): New routine.
+ (Is_Single_Protected_Object): New routine.
+ (Is_Single_Task_Object): New routine.
+ (Report_Unused_Body_States): Moved to Check_Unused_Body_States.
+
+2015-11-18 Pierre-Marie de Rodat <derodat@adacore.com>
+
+ * Makefile.rtl, impunit.adb: Add g-strhas.ads.
+ * g-strhas.ads: New file.
+ * s-strhas.ads: Add a comment to redirect users to g-strhas.ads.
+
+2015-11-18 Bob Duff <duff@adacore.com>
+
+ * sem_elab.adb (Check_Internal_Call_Continue): Fix the case
+ where the call in question is to a renaming of a subprogram that
+ can be safely called without ABE.
+ * checks.adb: Minor edits.
+
2015-11-18 Hristian Kirtchev <kirtchev@adacore.com>
* atree.adb (Elist11): New routine.
g-sptabo$(objext) \
g-sptain$(objext) \
g-sptavs$(objext) \
+ g-strhas$(objext) \
g-string$(objext) \
g-strspl$(objext) \
g-table$(objext) \
-- This block is inserted (using Insert_Actions), and then the node
-- is replaced with a reference to Rnn.
- -- A special case arises if our parent is a conversion node. In this
- -- case no point in generating a conversion to Result_Type, we will
- -- let the parent handle this. Note that this special case is not
- -- just about optimization. Consider
+ -- If our parent is a conversion node then there is no point in
+ -- generating a conversion to Result_Type, we will let the parent
+ -- handle this. Note that this special case is not just about
+ -- optimization. Consider
-- A,B,C : Integer;
-- ...
package body Contracts is
+ procedure Analyze_Contracts
+ (L : List_Id;
+ Freeze_Nod : Node_Id;
+ Freeze_Id : Entity_Id);
+ -- Subsidiary to the one parameter version of Analyze_Contracts and routine
+ -- Analyze_Previous_Constracts. Analyze the contracts of all constructs in
+ -- the list L. If Freeze_Nod is set, then the analysis stops when the node
+ -- is reached. Freeze_Id is the entity of some related context which caused
+ -- freezing upto node Freeze_Nod.
+
procedure Expand_Subprogram_Contract (Body_Id : Entity_Id);
-- Expand the contracts of a subprogram body and its correspoding spec (if
-- any). This routine processes all [refined] pre- and postconditions as
end if;
end Add_Contract_Item;
- ---------------------------------------------
- -- Analyze_Enclosing_Package_Body_Contract --
- ---------------------------------------------
+ -----------------------
+ -- Analyze_Contracts --
+ -----------------------
+
+ procedure Analyze_Contracts (L : List_Id) is
+ begin
+ Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
+ end Analyze_Contracts;
- procedure Analyze_Enclosing_Package_Body_Contract (Body_Decl : Node_Id) is
- Par : Node_Id;
+ procedure Analyze_Contracts
+ (L : List_Id;
+ Freeze_Nod : Node_Id;
+ Freeze_Id : Entity_Id)
+ is
+ Decl : Node_Id;
begin
- -- Climb the parent chain looking for an enclosing body. Do not use the
- -- scope stack, as a body uses the entity of its corresponding spec.
+ Decl := First (L);
+ while Present (Decl) loop
- Par := Parent (Body_Decl);
- while Present (Par) loop
- if Nkind (Par) = N_Package_Body then
- Analyze_Package_Body_Contract
- (Body_Id => Defining_Entity (Par),
- Freeze_Id => Defining_Entity (Body_Decl));
+ -- The caller requests that the traversal stops at a particular node
+ -- that causes contract "freezing".
- return;
+ if Present (Freeze_Nod) and then Decl = Freeze_Nod then
+ exit;
end if;
- Par := Parent (Par);
+ -- Entry or subprogram declarations
+
+ if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+ N_Entry_Declaration,
+ N_Generic_Subprogram_Declaration,
+ N_Subprogram_Declaration)
+ then
+ Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id => Defining_Entity (Decl),
+ Freeze_Id => Freeze_Id);
+
+ -- Entry or subprogram bodies
+
+ elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
+ Analyze_Entry_Or_Subprogram_Body_Contract (Defining_Entity (Decl));
+
+ -- Objects
+
+ elsif Nkind (Decl) = N_Object_Declaration then
+ Analyze_Object_Contract
+ (Obj_Id => Defining_Entity (Decl),
+ Freeze_Id => Freeze_Id);
+
+ -- Protected untis
+
+ elsif Nkind_In (Decl, N_Protected_Type_Declaration,
+ N_Single_Protected_Declaration)
+ then
+ Analyze_Protected_Contract (Defining_Entity (Decl));
+
+ -- Subprogram body stubs
+
+ elsif Nkind (Decl) = N_Subprogram_Body_Stub then
+ Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
+
+ -- Task units
+
+ elsif Nkind_In (Decl, N_Single_Task_Declaration,
+ N_Task_Type_Declaration)
+ then
+ Analyze_Task_Contract (Defining_Entity (Decl));
+ end if;
+
+ Next (Decl);
end loop;
- end Analyze_Enclosing_Package_Body_Contract;
+ end Analyze_Contracts;
-----------------------------------------------
-- Analyze_Entry_Or_Subprogram_Body_Contract --
-- Analyze_Entry_Or_Subprogram_Contract --
------------------------------------------
- procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id) is
+ procedure Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
Items : constant Node_Id := Contract (Subp_Id);
Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
else
Prag := Pre_Post_Conditions (Items);
while Present (Prag) loop
- Analyze_Pre_Post_Condition_In_Decl_Part (Prag);
+ Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Freeze_Id);
Prag := Next_Pragma (Prag);
end loop;
end if;
-- Otherwise analyze the contract cases
else
- Analyze_Contract_Cases_In_Decl_Part (Prag);
+ Analyze_Contract_Cases_In_Decl_Part (Prag, Freeze_Id);
end if;
else
pragma Assert (Prag_Nam = Name_Test_Case);
end if;
end Analyze_Entry_Or_Subprogram_Contract;
- ------------------------------------------
- -- Analyze_Initial_Declaration_Contract --
- ------------------------------------------
-
- procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id) is
- Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl);
-
- begin
- -- Note that stubs are excluded because the compiler always analyzes the
- -- proper body when a stub is encountered.
-
- if Nkind (Body_Decl) = N_Entry_Body then
- Analyze_Entry_Or_Subprogram_Contract (Spec_Id);
-
- elsif Nkind (Body_Decl) = N_Package_Body then
- Analyze_Package_Contract (Spec_Id);
-
- elsif Nkind (Body_Decl) = N_Protected_Body then
- Analyze_Protected_Contract (Spec_Id);
-
- elsif Nkind (Body_Decl) = N_Subprogram_Body then
- if Present (Corresponding_Spec (Body_Decl)) then
- Analyze_Entry_Or_Subprogram_Contract (Spec_Id);
- end if;
-
- elsif Nkind (Body_Decl) = N_Task_Body then
- Analyze_Task_Contract (Spec_Id);
-
- else
- raise Program_Error;
- end if;
- end Analyze_Initial_Declaration_Contract;
-
-----------------------------
-- Analyze_Object_Contract --
-----------------------------
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
+ procedure Analyze_Object_Contract
+ (Obj_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
AR_Val : Boolean := False;
AW_Val : Boolean := False;
-- Analyze indicator Part_Of
if Present (Prag) then
- Analyze_Part_Of_In_Decl_Part (Prag);
+ Analyze_Part_Of_In_Decl_Part (Prag, Freeze_Id);
-- The variable is a constituent of a single protected/task type
-- and behaves as a component of the type. Verify that references
end Analyze_Package_Contract;
--------------------------------
+ -- Analyze_Previous_Contracts --
+ --------------------------------
+
+ procedure Analyze_Previous_Contracts (Body_Decl : Node_Id) is
+ Body_Id : constant Entity_Id := Defining_Entity (Body_Decl);
+ Par : Node_Id;
+
+ begin
+ -- A body that is in the process of being inlined appears from source,
+ -- but carries name _parent. Such a body does not cause "freezing" of
+ -- contracts.
+
+ if Chars (Body_Id) = Name_uParent then
+ return;
+ end if;
+
+ -- Climb the parent chain looking for an enclosing package body. Do not
+ -- use the scope stack, as a body uses the entity of its corresponding
+ -- spec.
+
+ Par := Parent (Body_Decl);
+ while Present (Par) loop
+ if Nkind (Par) = N_Package_Body then
+ Analyze_Package_Body_Contract
+ (Body_Id => Defining_Entity (Par),
+ Freeze_Id => Defining_Entity (Body_Decl));
+
+ exit;
+ end if;
+
+ Par := Parent (Par);
+ end loop;
+
+ -- Analyze the contracts of all eligible construct upto the body which
+ -- caused the "freezing".
+
+ if Is_List_Member (Body_Decl) then
+ Analyze_Contracts
+ (L => List_Containing (Body_Decl),
+ Freeze_Nod => Body_Decl,
+ Freeze_Id => Body_Id);
+ end if;
+ end Analyze_Previous_Contracts;
+
+ --------------------------------
-- Analyze_Protected_Contract --
--------------------------------
-- 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_Contracts (L : List_Id);
+ -- Analyze the contracts of all eligible constructs found in list L
procedure Analyze_Entry_Or_Subprogram_Body_Contract (Body_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of entry or
-- Refined_Post
-- Test_Case (stand alone subprogram body)
- procedure Analyze_Entry_Or_Subprogram_Contract (Subp_Id : Entity_Id);
+ procedure Analyze_Entry_Or_Subprogram_Contract
+ (Subp_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty);
-- Analyze all delayed pragmas chained on the contract of entry or
-- subprogram Subp_Id as if they appeared at the end of a declarative
-- region. The pragmas in question are:
-- Postcondition
-- Precondition
-- Test_Case
+ --
+ -- Freeze_Id is the entity of a [generic] package body or a [generic]
+ -- subprogram body which "freezes" the contract of Subp_Id.
- procedure Analyze_Initial_Declaration_Contract (Body_Decl : Node_Id);
- -- Analyze the contract of the initial declaration of entry body, package
- -- body, protected body, subprogram body or task body Body_Decl.
-
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
+ procedure Analyze_Object_Contract
+ (Obj_Id : Entity_Id;
+ Freeze_Id : Entity_Id := Empty);
-- Analyze all delayed pragmas chained on the contract of object Obj_Id as
-- if they appeared at the end of the declarative region. The pragmas to be
-- considered are:
-- Effective_Writes
-- Global (single concurrent object)
-- Part_Of
+ --
+ -- Freeze_Id is the entity of a [generic] package body or a [generic]
+ -- subprogram body which "freezes" the contract of Obj_Id.
procedure Analyze_Package_Body_Contract
(Body_Id : Entity_Id;
-- Initializes
-- Part_Of
+ procedure Analyze_Previous_Contracts (Body_Decl : Node_Id);
+ -- Analyze the contracts of all source constructs found in the declarative
+ -- list which contains entry, package, protected, subprogram, or task body
+ -- denoted by Body_Decl. The analysis stops once Body_Decl is reached.
+
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
-- Analyze all delayed pragmas chained on the contract of protected unit
-- Prot_Id if they appeared at the end of a declarative region. Currently
--- /dev/null
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- G N A T . S T R I N G _ H A S H --
+-- --
+-- 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. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+-- This package provides a generic hashing function over strings, suitable for
+-- use with a string keyed hash table. In particular, it is the basis for the
+-- string hash functions in Ada.Containers.
+--
+-- The algorithm used here is not appropriate for applications that require
+-- cryptographically strong hashes, or for application which wish to use very
+-- wide hash values as pseudo unique identifiers. In such cases please refer
+-- to GNAT.SHA1 and GNAT.MD5.
+
+with System.String_Hash;
+
+package GNAT.String_Hash renames System.String_Hash;
("g-sptabo", F), -- GNAT.Spitbol.Table_Boolean
("g-sptain", F), -- GNAT.Spitbol.Table_Integer
("g-sptavs", F), -- GNAT.Spitbol.Table_Vstring
+ ("g-strhas", F), -- GNAT.String_Hash
("g-string", F), -- GNAT.Strings
("g-strspl", F), -- GNAT.String_Split
("g-sse ", F), -- GNAT.SSE
-- --
-- B o d y --
-- --
--- 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- --
----------------
function To_Neg_Int (A : Uns64) return Int64 is
- R : constant Int64 := -To_Int (A);
+ R : constant Int64 := (if A = 2**63 then Int64'First else -To_Int (A));
+ -- Note that we can't just use the expression of the Else, because it
+ -- overflows for A = 2**63.
begin
if R <= 0 then
return R;
-- --
-- S p e c --
-- --
--- Copyright (C) 2009, Free Software Foundation, Inc. --
+-- Copyright (C) 2009-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- --
-- cryptographically strong hashes, or for application which wish to use very
-- wide hash values as pseudo unique identifiers. In such cases please refer
-- to GNAT.SHA1 and GNAT.MD5.
+--
+-- Note: this package is in the System hierarchy so that it can be directly
+-- be used by other predefined packages. User access to this package is via
+-- a renaming of this package in GNAT.String_Hash (file g-strhas.ads).
package System.String_Hash is
pragma Pure;
Analyze_Package_Body_Contract (Defining_Entity (Context));
end if;
- -- Analyze the contracts of eligible constructs (see below) due to
- -- the delayed visibility needs of their aspects and pragmas.
+ -- Analyze the contracts of various constructs now due to the delayed
+ -- visibility needs of their aspects and pragmas.
- Decl := First (L);
- while Present (Decl) loop
-
- -- Entry or subprogram declarations
-
- if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
- N_Entry_Declaration,
- N_Generic_Subprogram_Declaration,
- N_Subprogram_Declaration)
- then
- Analyze_Entry_Or_Subprogram_Contract (Defining_Entity (Decl));
-
- -- Entry or subprogram bodies
-
- elsif Nkind_In (Decl, N_Entry_Body, N_Subprogram_Body) then
- Analyze_Entry_Or_Subprogram_Body_Contract
- (Defining_Entity (Decl));
-
- -- Objects
-
- elsif Nkind (Decl) = N_Object_Declaration then
- Analyze_Object_Contract (Defining_Entity (Decl));
-
- -- Protected untis
-
- elsif Nkind_In (Decl, N_Protected_Type_Declaration,
- N_Single_Protected_Declaration)
- then
- Analyze_Protected_Contract (Defining_Entity (Decl));
-
- -- Subprogram body stubs
-
- elsif Nkind (Decl) = N_Subprogram_Body_Stub then
- Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
-
- -- Task units
-
- elsif Nkind_In (Decl, N_Single_Task_Declaration,
- N_Task_Type_Declaration)
- then
- Analyze_Task_Contract (Defining_Entity (Decl));
- end if;
-
- Next (Decl);
- end loop;
+ Analyze_Contracts (L);
if Nkind (Context) = N_Package_Body then
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- -- A generic subprogram body "freezes" the contract of its initial
- -- declaration. This analysis depends on attribute Corresponding_Spec
- -- being set. Only bodies coming from source should cause this type
- -- of "freezing".
-
- if Comes_From_Source (N) then
- Analyze_Initial_Declaration_Contract (N);
- end if;
-
Analyze_Declarations (Declarations (N));
Check_Completion;
begin
-- A [generic] subprogram body "freezes" the contract of the nearest
- -- enclosing package body:
+ -- enclosing package body and all other contracts encountered in the
+ -- same declarative part upto and excluding the subprogram body:
-- package body Nearest_Enclosing_Package
-- with Refined_State => (State => Constit)
-- Original_Node.
if Comes_From_Source (Original_Node (N)) then
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
end if;
-- Generic subprograms are handled separately. They always have a
Analyze_Aspect_Specifications_On_Body_Or_Stub (N);
end if;
- -- A subprogram body "freezes" the contract of its initial declaration.
- -- This analysis depends on attribute Corresponding_Spec being set. Only
- -- bodies coming from source should cause this type of "freezing".
-
- if Comes_From_Source (N) then
- Analyze_Initial_Declaration_Contract (N);
- end if;
-
Analyze_Declarations (Declarations (N));
-- Verify that the SPARK_Mode of the body agrees with that of its spec
begin
-- A [generic] package body "freezes" the contract of the nearest
- -- enclosing package body:
+ -- enclosing package body and all other contracts encountered in the
+ -- same declarative part upto and excluding the package body:
-- package body Nearest_Enclosing_Package
-- with Refined_State => (State => Constit)
-- Only bodies coming from source should cause this type of "freezing"
if Comes_From_Source (N) then
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
end if;
-- Find corresponding package specification, and establish the current
-- This analysis depends on attribute Corresponding_Spec being set. Only
-- bodies coming from source shuld cause this type of "freezing".
- if Comes_From_Source (N) then
- Analyze_Initial_Declaration_Contract (N);
- end if;
-
if Present (Declarations (N)) then
Analyze_Declarations (Declarations (N));
Inspect_Deferred_Constant_Completion (Declarations (N));
Entry_Name : Entity_Id;
begin
- -- An entry body "freezes" the contract of the nearest enclosing
- -- package body. This ensures that any annotations referenced by the
- -- contract of an entry or subprogram body declared within the current
- -- protected body are available.
+ -- An entry body "freezes" the contract of the nearest enclosing package
+ -- body and all other contracts encountered in the same declarative part
+ -- upto and excluding the entry body. This ensures that any annotations
+ -- referenced by the contract of an entry or subprogram body declared
+ -- within the current protected body are available.
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
(Sloc (N), Entry_Name, P_Type, N, Decls);
end if;
- -- An entry body "freezes" the contract of its initial declaration. This
- -- analysis depends on attribute Corresponding_Body being set.
-
- Analyze_Initial_Declaration_Contract (N);
-
if Present (Decls) then
Analyze_Declarations (Decls);
Inspect_Deferred_Constant_Completion (Decls);
begin
-- A protected body "freezes" the contract of the nearest enclosing
- -- package body. This ensures that any annotations referenced by the
- -- contract of an entry or subprogram body declared within the current
- -- protected body are available.
+ -- package body and all other contracts encountered in the same
+ -- declarative part upto and excluding the protected body. This ensures
+ -- that any annotations referenced by the contract of an entry or
+ -- subprogram body declared within the current protected body are
+ -- available.
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
Set_Ekind (Body_Id, E_Protected_Body);
Expand_Protected_Body_Declarations (N, Spec_Id);
Last_E := Last_Entity (Spec_Id);
- -- A protected body "freezes" the contract of its initial declaration.
- -- This analysis depends on attribute Corresponding_Spec being set.
-
- Analyze_Initial_Declaration_Contract (N);
-
Analyze_Declarations (Declarations (N));
-- For visibility purposes, all entities in the body are private. Set
begin
-- A task body "freezes" the contract of the nearest enclosing package
- -- body. This ensures that annotations referenced by the contract of an
- -- entry or subprogram body declared within the current protected body
- -- are available.
+ -- body and all other contracts encountered in the same declarative part
+ -- upto and excluding the task body. This ensures that annotations
+ -- referenced by the contract of an entry or subprogram body declared
+ -- within the current protected body are available.
- Analyze_Enclosing_Package_Body_Contract (N);
+ Analyze_Previous_Contracts (N);
Tasking_Used := True;
Set_Scope (Body_Id, Current_Scope);
Install_Declarations (Spec_Id);
Last_E := Last_Entity (Spec_Id);
- -- A task body "freezes" the contract of its initial declaration. This
- -- analysis depends on attribute Corresponding_Spec being set.
-
- Analyze_Initial_Declaration_Contract (N);
-
Analyze_Declarations (Decls);
Inspect_Deferred_Constant_Completion (Decls);
Outer_Scope : Entity_Id;
Orig_Ent : Entity_Id)
is
- Loc : constant Source_Ptr := Sloc (N);
- Inst_Case : constant Boolean := Is_Generic_Unit (E);
-
- Sbody : Node_Id;
- Ebody : Entity_Id;
-
function Find_Elab_Reference (N : Node_Id) return Traverse_Result;
-- Function applied to each node as we traverse the body. Checks for
-- call or entity reference that needs checking, and if so checks it.
end if;
end Find_Elab_Reference;
+ Inst_Case : constant Boolean := Is_Generic_Unit (E);
+ Loc : constant Source_Ptr := Sloc (N);
+
+ Ebody : Entity_Id;
+ Sbody : Node_Id;
+
-- Start of processing for Check_Internal_Call_Continue
begin
-- Not that special case, warning and dynamic check is required
-- If we have nothing in the call stack, then this is at the outer
- -- level, and the ABE is bound to occur, unless it's a 'Access.
+ -- level, and the ABE is bound to occur, unless it's a 'Access, or
+ -- it's a renaming.
if Elab_Call.Last = 0 then
Error_Msg_Warn := SPARK_Mode /= On;
- if Inst_Case then
- Error_Msg_NE
- ("cannot instantiate& before body seen<<", N, Orig_Ent);
- elsif Nkind (N) /= N_Attribute_Reference then
- Error_Msg_NE
- ("cannot call& before body seen<<", N, Orig_Ent);
- else
- Error_Msg_NE
- ("Access attribute of & before body seen<<", N, Orig_Ent);
- Error_Msg_N ("\possible Program_Error on later references<", N);
- end if;
+ declare
+ Insert_Check : Boolean := True;
+ -- This flag is set to True if an elaboration check should be
+ -- inserted.
- if Nkind (N) /= N_Attribute_Reference then
- Error_Msg_N ("\Program_Error [<<", N);
- Insert_Elab_Check (N);
- end if;
+ begin
+ if Inst_Case then
+ Error_Msg_NE
+ ("cannot instantiate& before body seen<<", N, Orig_Ent);
+
+ elsif Nkind (N) = N_Attribute_Reference then
+ Error_Msg_NE
+ ("Access attribute of & before body seen<<", N, Orig_Ent);
+ Error_Msg_N ("\possible Program_Error on later references<", N);
+ Insert_Check := False;
+
+ elsif Nkind (Unit_Declaration_Node (Orig_Ent)) /=
+ N_Subprogram_Renaming_Declaration
+ then
+ Error_Msg_NE
+ ("cannot call& before body seen<<", N, Orig_Ent);
+
+ else
+ Insert_Check := False;
+ end if;
+
+ if Insert_Check then
+ Error_Msg_N ("\Program_Error [<<", N);
+ Insert_Elab_Check (N);
+ end if;
+ end;
-- Call is not at outer level
-- corresponding constituent from list Constits (if any) appear in the same
-- context denoted by Context. If this is the case, emit an error.
+ procedure Contract_Freeze_Error
+ (Contract_Id : Entity_Id;
+ Freeze_Id : Entity_Id);
+ -- Subsidiary to the analysis of pragmas Contract_Cases, Part_Of, Post, and
+ -- Pre. Emit a freezing-related error message where Freeze_Id is the entity
+ -- of a body which caused contract "freezing" and Contract_Id denotes the
+ -- entity of the affected contstruct.
+
procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id);
-- Subsidiary to all Find_Related_xxx routines. Emit an error on pragma
-- Prag that duplicates previous pragma Prev.
-- Analyze_Contract_Cases_In_Decl_Part --
-----------------------------------------
- procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Contract_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
+ Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
+
Others_Seen : Boolean := False;
+ -- This flag is set when an "others" choice is encountered. It is used
+ -- to detect multiple illegal occurences of "others".
procedure Analyze_Contract_Case (CCase : Node_Id);
-- Verify the legality of a single contract case
procedure Analyze_Contract_Case (CCase : Node_Id) is
Case_Guard : Node_Id;
Conseq : Node_Id;
+ Errors : Nat;
Extra_Guard : Node_Id;
begin
-- Preanalyze the case guard and consequence
if Nkind (Case_Guard) /= N_Others_Choice then
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
+
+ -- Emit a clarification message when the case guard contains
+ -- at leat one undefined reference, possibly due to contract
+ -- "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Case_Guard)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
end if;
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
+ -- Emit a clarification message when the consequence contains
+ -- at leat one undefined reference, possibly due to contract
+ -- "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Conseq)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
+
-- The contract case is malformed
else
-- Local variables
- Subp_Decl : constant Node_Id := Find_Related_Declaration_Or_Body (N);
- Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
- CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
+ CCases : constant Node_Id := Expression (Get_Argument (N, Spec_Id));
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
elsif Ekind (Item_Id) = E_Loop_Parameter then
Add_Str_To_Name_Buffer ("loop parameter");
- elsif Ekind (Item_Id) = E_Protected_Type then
+ elsif Ekind (Item_Id) = E_Protected_Type
+ or else Is_Single_Protected_Object (Item_Id)
+ then
Add_Str_To_Name_Buffer ("current instance of protected type");
- elsif Ekind (Item_Id) = E_Task_Type then
+ elsif Ekind (Item_Id) = E_Task_Type
+ or else Is_Single_Task_Object (Item_Id)
+ then
Add_Str_To_Name_Buffer ("current instance of task type");
elsif Ekind (Item_Id) = E_Variable then
-- Analyze_Part_Of_In_Decl_Part --
----------------------------------
- procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Part_Of_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
+ Encap : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
+ Errors : constant Nat := Serious_Errors_Detected;
Var_Decl : constant Node_Id := Find_Related_Context (N);
Var_Id : constant Entity_Id := Defining_Entity (Var_Decl);
Encap_Id : Entity_Id;
Analyze_Part_Of
(Indic => N,
Item_Id => Var_Id,
- Encap => Get_Pragma_Arg (First (Pragma_Argument_Associations (N))),
+ Encap => Encap,
Encap_Id => Encap_Id,
Legal => Legal);
Append_Elmt (Var_Id, Part_Of_Constituents (Encap_Id));
Set_Encapsulating_State (Var_Id, Encap_Id);
end if;
+
+ -- Emit a clarification message when the encapsulator is undefined,
+ -- possibly due to contract "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Encap)
+ then
+ Contract_Freeze_Error (Var_Id, Freeze_Id);
+ end if;
end Analyze_Part_Of_In_Decl_Part;
--------------------
-- Obj : Anon_Task_Typ;
-- pragma SPARK_Mode ...;
- if Is_Single_Concurrent_Object (Spec_Id)
- and then Ekind (Spec_Typ) = E_Task_Type
- then
+ if Is_Single_Task_Object (Spec_Id) then
Set_SPARK_Pragma (Spec_Typ, N);
Set_SPARK_Pragma_Inherited (Spec_Typ, False);
Set_SPARK_Aux_Pragma (Spec_Typ, N);
-- Analyze_Pre_Post_Condition_In_Decl_Part --
---------------------------------------------
- procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id) is
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty)
+ is
procedure Process_Class_Wide_Condition
(Expr : Node_Id;
Spec_Id : Entity_Id;
Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+ Errors : Nat;
Restore_Scope : Boolean := False;
-- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
end if;
end if;
+ Errors := Serious_Errors_Detected;
Preanalyze_Assert_Expression (Expr, Standard_Boolean);
+ -- Emit a clarification message when the expression contains at leat one
+ -- undefined reference, possibly due to contract "freezing".
+
+ if Errors /= Serious_Errors_Detected
+ and then Present (Freeze_Id)
+ and then Has_Undefined_Reference (Expr)
+ then
+ Contract_Freeze_Error (Spec_Id, Freeze_Id);
+ end if;
+
-- For a class-wide condition, a reference to a controlling formal must
-- be interpreted as having the class-wide type (or an access to such)
-- so that the inherited condition can be properly applied to any
Report_Unrefined_States (Available_States);
- -- Ensure that all abstract states and objects declared in the body
- -- state space of the related package are utilized as constituents.
-
- Report_Unused_Body_States (Body_Id, Body_States);
-
Set_Is_Analyzed_Pragma (N);
end Analyze_Refined_State_In_Decl_Part;
-- Local variables
- Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id);
- Spec_Id : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
Clause : Node_Id;
Clauses : Node_Id;
Depends : Node_Id;
Formal : Entity_Id;
Global : Node_Id;
+ Spec_Id : Entity_Id;
+ Subp_Decl : Node_Id;
Typ : Entity_Id;
-- Start of processing for Collect_Subprogram_Inputs_Outputs
begin
Global_Seen := False;
- -- Process all [generic] formal parameters
+ -- Process all formal parameters of entries, [generic] subprograms and
+ -- their bodies.
- Formal := First_Entity (Spec_Id);
- while Present (Formal) loop
- if Ekind_In (Formal, E_Generic_In_Parameter,
- E_In_Out_Parameter,
- E_In_Parameter)
- then
- 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
- Append_New_Elmt (Formal, Subp_Outputs);
+ if Ekind_In (Subp_Id, E_Entry,
+ E_Entry_Family,
+ E_Function,
+ E_Generic_Function,
+ E_Generic_Procedure,
+ E_Procedure,
+ E_Subprogram_Body)
+ then
+ Subp_Decl := Unit_Declaration_Node (Subp_Id);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
- -- Out parameters can act as inputs when the related type is
- -- tagged, unconstrained array, unconstrained record or record
- -- with unconstrained components.
+ -- Process all [generic] formal parameters
- if Ekind (Formal) = E_Out_Parameter
- and then Is_Unconstrained_Or_Tagged_Item (Formal)
+ Formal := First_Entity (Spec_Id);
+ while Present (Formal) loop
+ if Ekind_In (Formal, E_Generic_In_Parameter,
+ E_In_Out_Parameter,
+ E_In_Parameter)
then
Append_New_Elmt (Formal, Subp_Inputs);
end if;
- end if;
- Next_Entity (Formal);
- end loop;
+ if Ekind_In (Formal, E_Generic_In_Out_Parameter,
+ E_In_Out_Parameter,
+ E_Out_Parameter)
+ then
+ Append_New_Elmt (Formal, Subp_Outputs);
+
+ -- Out parameters can act as inputs when the related type is
+ -- tagged, unconstrained array, unconstrained record or record
+ -- with unconstrained components.
+
+ if Ekind (Formal) = E_Out_Parameter
+ and then Is_Unconstrained_Or_Tagged_Item (Formal)
+ then
+ Append_New_Elmt (Formal, Subp_Inputs);
+ end if;
+ end if;
+
+ Next_Entity (Formal);
+ end loop;
+
+ -- Otherwise the input denotes a task type, a task body, or the
+ -- anonymous object created for a single task type.
+
+ elsif Ekind_In (Subp_Id, E_Task_Type, E_Task_Body)
+ or else Is_Single_Task_Object (Subp_Id)
+ then
+ Subp_Decl := Declaration_Node (Subp_Id);
+ Spec_Id := Unique_Defining_Entity (Subp_Decl);
+ end if;
-- When processing an entry, subprogram or task body, look for pragmas
-- Refined_Depends and Refined_Global as they specify the inputs and
end if;
end if;
+ -- The current instance of a protected type acts as a formal parameter
+ -- of mode IN for functions and IN OUT for entries and procedures
+ -- (SPARK RM 6.1.4).
+
if Ekind (Scope (Spec_Id)) = E_Protected_Type then
Typ := Scope (Spec_Id);
- -- A single protected type declaration does not have a current
- -- instance because the type is technically an object.
+ -- Use the anonymous object when the type is single protected
if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
- null;
-
- -- Otherwise the current instance of the protected type acts as a
- -- formal parameter of mode IN for functions and IN OUT for entries
- -- and procedures (SPARK RM 6.1.4).
+ Typ := Anonymous_Object (Typ);
+ end if;
- else
- Append_New_Elmt (Typ, Subp_Inputs);
+ Append_New_Elmt (Typ, Subp_Inputs);
- if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then
- Append_New_Elmt (Typ, Subp_Outputs);
- end if;
+ if Ekind_In (Spec_Id, E_Entry, E_Entry_Family, E_Procedure) then
+ Append_New_Elmt (Typ, Subp_Outputs);
end if;
+ -- The current instance of a task type acts as a formal parameter of
+ -- mode IN OUT (SPARK RM 6.1.4).
+
elsif Ekind (Spec_Id) = E_Task_Type then
Typ := Spec_Id;
- -- A single task type declaration does not have a current instance
- -- because the type is technically an object.
+ -- Use the anonymous object when the type is single task
if Is_Single_Concurrent_Type_Declaration (Declaration_Node (Typ)) then
- null;
+ Typ := Anonymous_Object (Typ);
+ end if;
- -- Otherwise the current instance of the task type acts as a formal
- -- parameter of mode IN OUT (SPARK RM 6.1.4).
+ Append_New_Elmt (Typ, Subp_Inputs);
+ Append_New_Elmt (Typ, Subp_Outputs);
- else
- Append_New_Elmt (Typ, Subp_Inputs);
- Append_New_Elmt (Typ, Subp_Outputs);
- end if;
+ elsif Is_Single_Task_Object (Spec_Id) then
+ Append_New_Elmt (Spec_Id, Subp_Inputs);
+ Append_New_Elmt (Spec_Id, Subp_Outputs);
end if;
end Collect_Subprogram_Inputs_Outputs;
+ ---------------------------
+ -- Contract_Freeze_Error --
+ ---------------------------
+
+ procedure Contract_Freeze_Error
+ (Contract_Id : Entity_Id;
+ Freeze_Id : Entity_Id)
+ is
+ begin
+ Error_Msg_Name_1 := Chars (Contract_Id);
+ Error_Msg_Sloc := Sloc (Freeze_Id);
+
+ SPARK_Msg_NE
+ ("body & declared # freezes the contract of%", Contract_Id, Freeze_Id);
+ SPARK_Msg_N
+ ("\all contractual items must be declared before body #", Contract_Id);
+ end Contract_Freeze_Error;
+
---------------------------------
-- Delay_Config_Pragma_Analyze --
---------------------------------
procedure Analyze_Pragma (N : Node_Id);
-- Analyze procedure for pragma reference node N
- procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of delayed pragma Contract_Cases
+ procedure Analyze_Contract_Cases_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Contract_Cases. Freeze_Id is the
+ -- entity of [generic] package body or [generic] subprogram body which
+ -- caused "freezing" of the related contract where the pragma resides.
procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Depends. This routine is also
procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
-- Perform full analysis of delayed pragma Initializes
- procedure Analyze_Part_Of_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of delayed pragma Part_Of
+ procedure Analyze_Part_Of_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of delayed pragma Part_Of. Freeze_Id is the entity
+ -- of [generic] package body or [generic] subprogram body which caused the
+ -- "freezing" of the related contract where the pragma resides.
- procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id);
- -- Perform full analysis of pragmas Precondition and Postcondition
+ procedure Analyze_Pre_Post_Condition_In_Decl_Part
+ (N : Node_Id;
+ Freeze_Id : Entity_Id := Empty);
+ -- Perform full analysis of pragmas Precondition and Postcondition.
+ -- 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_Refined_Depends_In_Decl_Part (N : Node_Id);
-- Preform full analysis of delayed pragma Refined_Depends. This routine
------------------------------
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.
+ procedure Report_Unused_Body_States (States : Elist_Id);
+ -- Emit errors for each abstract state or object found in list States
+
-------------------------------
-- Process_Refinement_Clause --
-------------------------------
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.
end if;
end Process_Refinement_Clause;
+ -------------------------------
+ -- Report_Unused_Body_States --
+ -------------------------------
+
+ procedure Report_Unused_Body_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
+ 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;
+
-- Local variables
- Prag : constant Node_Id :=
- Get_Pragma (Body_Id, Pragma_Refined_State);
+ 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;
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.
+ -- visible states declared within the package body participate in the
+ -- refinement.
if Present (Prag) then
Clause := Expression (Get_Argument (Prag, Spec_Id));
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.
+ -- Ensure that all abstract states and objects declared in the
+ -- package body state space are utilized as constituents.
- if Legal_Constits then
- Report_Unused_Body_States (Body_Id, States);
- end if;
+ Report_Unused_Body_States (States);
end if;
end Check_Unused_Body_States;
-------------------------
function Collect_Body_States (Body_Id : Entity_Id) return Elist_Id is
+ function Is_Visible_Object (Obj_Id : Entity_Id) return Boolean;
+ -- Determine whether object Obj_Id is a suitable visible state of a
+ -- package body.
+
procedure Collect_Visible_States
(Pack_Id : Entity_Id;
States : in out Elist_Id);
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)))
+ and then Is_Visible_Object (Item_Id)
then
Append_New_Elmt (Item_Id, States);
end loop;
end Collect_Visible_States;
+ -----------------------
+ -- Is_Visible_Object --
+ -----------------------
+
+ function Is_Visible_Object (Obj_Id : Entity_Id) return Boolean is
+ begin
+ -- Objects that map generic formals to their actuals are not visible
+ -- from outside the generic instantiation.
+
+ if Present (Corresponding_Generic_Association
+ (Declaration_Node (Obj_Id)))
+ then
+ return False;
+
+ -- Constituents of a single protected/task type act as components of
+ -- the type and are not visible from outside the type.
+
+ elsif Ekind (Obj_Id) = E_Variable
+ and then Present (Encapsulating_State (Obj_Id))
+ and then Is_Single_Concurrent_Object (Encapsulating_State (Obj_Id))
+ then
+ return False;
+
+ else
+ return True;
+ end if;
+ end Is_Visible_Object;
+
-- Local variables
Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id);
begin
-- Inspect the declarations of the body looking for source objects,
- -- packages and package instantiations.
+ -- packages and package instantiations. Note that even though this
+ -- processing is very similar to Collect_Visible_States, a package
+ -- body does not have a First/Next_Entity list.
Decl := First (Declarations (Body_Decl));
while Present (Decl) loop
if Nkind (Decl) = N_Object_Declaration then
Item_Id := Defining_Entity (Decl);
- if Comes_From_Source (Item_Id) then
+ if Comes_From_Source (Item_Id)
+ and then Is_Visible_Object (Item_Id)
+ then
Append_New_Elmt (Item_Id, States);
end if;
function Fix_Msg (Id : Entity_Id; Msg : String) return String is
Is_Task : constant Boolean :=
Ekind_In (Id, E_Task_Body, E_Task_Type)
- or else (Is_Single_Concurrent_Object (Id)
- and then Ekind (Etype (Id)) = E_Task_Type);
+ or else Is_Single_Task_Object (Id);
Msg_Last : constant Natural := Msg'Last;
Msg_Index : Natural;
Res : String (Msg'Range) := (others => ' ');
end if;
end Has_Tagged_Component;
+ -----------------------------
+ -- Has_Undefined_Reference --
+ -----------------------------
+
+ function Has_Undefined_Reference (Expr : Node_Id) return Boolean is
+ Has_Undef_Ref : Boolean := False;
+ -- Flag set when expression Expr contains at least one undefined
+ -- reference.
+
+ function Is_Undefined_Reference (N : Node_Id) return Traverse_Result;
+ -- Determine whether N denotes a reference and if it does, whether it is
+ -- undefined.
+
+ ----------------------------
+ -- Is_Undefined_Reference --
+ ----------------------------
+
+ function Is_Undefined_Reference (N : Node_Id) return Traverse_Result is
+ begin
+ if Is_Entity_Name (N)
+ and then Present (Entity (N))
+ and then Entity (N) = Any_Id
+ then
+ Has_Undef_Ref := True;
+ return Abandon;
+ end if;
+
+ return OK;
+ end Is_Undefined_Reference;
+
+ procedure Find_Undefined_References is
+ new Traverse_Proc (Is_Undefined_Reference);
+
+ -- Start of processing for Has_Undefined_Reference
+
+ begin
+ Find_Undefined_References (Expr);
+
+ return Has_Undef_Ref;
+ end Has_Undefined_Reference;
+
----------------------------
-- Has_Volatile_Component --
----------------------------
function Is_Single_Concurrent_Object (Id : Entity_Id) return Boolean is
begin
return
- Ekind (Id) = E_Variable
- and then Is_Single_Concurrent_Type (Etype (Id));
+ Is_Single_Protected_Object (Id) or else Is_Single_Task_Object (Id);
end Is_Single_Concurrent_Object;
-------------------------------
and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_7);
end Is_Single_Precision_Floating_Point_Type;
+ --------------------------------
+ -- Is_Single_Protected_Object --
+ --------------------------------
+
+ function Is_Single_Protected_Object (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind (Id) = E_Variable
+ and then Ekind (Etype (Id)) = E_Protected_Type
+ and then Is_Single_Concurrent_Type (Etype (Id));
+ end Is_Single_Protected_Object;
+
+ ---------------------------
+ -- Is_Single_Task_Object --
+ ---------------------------
+
+ function Is_Single_Task_Object (Id : Entity_Id) return Boolean is
+ begin
+ return
+ Ekind (Id) = E_Variable
+ and then Ekind (Etype (Id)) = E_Task_Type
+ and then Is_Single_Concurrent_Type (Etype (Id));
+ end Is_Single_Task_Object;
+
-------------------------------------
-- Is_SPARK_05_Initialization_Expr --
-------------------------------------
(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 --
--------------------
-- for the current unit. The declarations are added in the current scope,
-- so the caller should push a new scope as required before the call.
+ function Add_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
+ -- Returns the name of E adding Suffix
+
function Address_Integer_Convert_OK (T1, T2 : Entity_Id) return Boolean;
-- Given two types, returns True if we are in Allow_Integer_Address mode
-- and one of the types is (a descendent of) System.Address (and this type
-- 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.
+ -- Verify that all abstract states and objects declared in the state space
+ -- of package body Body_Id are used as constituents. Emit an error if this
+ -- is not the case.
procedure Check_Unprotected_Access
(Context : Node_Id;
-- and the context is external to the protected operation, to warn against
-- a possible unlocked access to data.
+ 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 Collect_Interfaces
(T : Entity_Id;
Ifaces_List : out Elist_Id;
function Has_Suffix (E : Entity_Id; Suffix : Character) return Boolean;
-- Returns true if the last character of E is Suffix. Used in Assertions.
- function Add_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
- -- Returns the name of E adding Suffix
-
- function Remove_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
- -- Returns the name of E without Suffix
-
function Has_Tagged_Component (Typ : Entity_Id) return Boolean;
-- Returns True if Typ is a composite type (array or record) which is
-- either itself a tagged type, or has a component (recursively) which is
-- component is present. This function is used to check if "=" has to be
-- expanded into a bunch component comparisons.
+ function Has_Undefined_Reference (Expr : Node_Id) return Boolean;
+ -- Given arbitrary expression Expr, determine whether it contains at
+ -- least one name whose entity is Any_Id.
+
function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
- -- Given an arbitrary type, determine whether it contains at least one
+ -- Given arbitrary type Typ, determine whether it contains at least one
-- volatile component.
function Implementation_Kind (Subp : Entity_Id) return Name_Id;
-- . machine_emax = 2**7
-- . machine_emin = 3 - machine_emax
+ function Is_Single_Protected_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes the anonymous object
+ -- created for a single protected type.
+
+ function Is_Single_Task_Object (Id : Entity_Id) return Boolean;
+ -- Determine whether arbitrary entity Id denotes the anonymous object
+ -- created for a single task type.
+
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an initialization
-- expression in SPARK 2005, suitable for initializing an object in an
-- the removal performed by this routine does not affect the visibility of
-- existing homonyms.
+ function Remove_Suffix (E : Entity_Id; Suffix : Character) return Name_Id;
+ -- Returns the name of E without Suffix
+
function Rep_To_Pos_Flag (E : Entity_Id; Loc : Source_Ptr) return Node_Id;
-- This is used to construct the second argument in a call to Rep_To_Pos
-- which is Standard_True if range checks are enabled (E is an entity to
-- 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
#if defined (__MINGW32__)
-#ifdef CERT
-
-/* For the Cert run times on native Windows we use dummy functions
- for locking and unlocking tasks since we do not support multiple
- threads on this configuration (Cert run time on native Windows). */
-
-void dummy (void) {}
-
-void (*Lock_Task) () = &dummy;
-void (*Unlock_Task) () = &dummy;
-
-#else
-
-#define Lock_Task system__soft_links__lock_task
-extern void (*Lock_Task) (void);
-
-#define Unlock_Task system__soft_links__unlock_task
-extern void (*Unlock_Task) (void);
-
-#endif
-
/* Reentrant localtime for Windows. */
extern void
DWORD tzi_status;
- (*Lock_Task) ();
-
tzi_status = GetTimeZoneInformation (&tzi);
/* Cases where we simply want to extract the offset of the current time
}
}
}
-
- (*Unlock_Task) ();
}
#elif defined (__Lynx__)
projects / platform / upstream / linaro-gcc.git / commitdiff