Skip to content

R
riscv-gcc-1
Commit 2757c5bf by Arnaud Charlet
Options

[multiple changes] 

2014-01-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Has_Option): Reimplemented.
	* sem_prag.adb (Analyze_Refinement_Clause): Add global
	variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
	External_Constit_Seen and State. Add local variables Body_Ref,
	Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
	avoid a cumbersome while pool. Verify the legality of an external
	state and relevant properties.
	(Check_External_Property): New routine.
	(Check_Matching_State): Remove parameter profile
	and update comment on usage.
	(Collect_Constituent): Store the
	relevant external property of a constituent.
	* sem_util.adb (Async_Readers_Enabled): Update the call to
	Has_Enabled_Property.
	(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
	(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
	Update comment on usage. Reimplement the logic to recognize the various
	formats of properties.

2014-01-27  Ed Schonberg  <schonberg@adacore.com>

	* par-ch5.adb: Minor reformatting.

2014-01-27  Tristan Gingold  <gingold@adacore.com>

	* s-tposen.ads: Harmonize style and comments.

2014-01-27  Vincent Celier  <celier@adacore.com>

	* projects.texi: Document that shared library projects, by
	default, cannot import projects that are not shared library
	projects.

2014-01-27  Robert Dewar  <dewar@adacore.com>

	* sem_ch8.adb (Find_Selected_Component): Use Replace instead
	of Rewrite.

2014-01-27  Ed Schonberg  <schonberg@adacore.com>

	* a-suenco.adb, a-suenst.adb (Decode): Raise encoding error if
	any other exception is raised.
	(Convert): If both Input_Scheme and Output_Scheme are UTF_8 it is
	still necessary to perform a conversion in order to remove overlong
	encodings.

From-SVN: r207142
parent 00ba7be8
Showing with 422 additions and 193 deletions
gcc/ada/ChangeLog
2014-01-27 Hristian Kirtchev <kirtchev@adacore.com>
* einfo.adb (Has_Option): Reimplemented.
* sem_prag.adb (Analyze_Refinement_Clause): Add global
variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
External_Constit_Seen and State. Add local variables Body_Ref,
Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
avoid a cumbersome while pool. Verify the legality of an external
state and relevant properties.
(Check_External_Property): New routine.
(Check_Matching_State): Remove parameter profile
and update comment on usage.
(Collect_Constituent): Store the
relevant external property of a constituent.
* sem_util.adb (Async_Readers_Enabled): Update the call to
Has_Enabled_Property.
(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
Update comment on usage. Reimplement the logic to recognize the various
formats of properties.
2014-01-27 Ed Schonberg <schonberg@adacore.com>
* par-ch5.adb: Minor reformatting.
2014-01-27 Tristan Gingold <gingold@adacore.com>
* s-tposen.ads: Harmonize style and comments.
2014-01-27 Vincent Celier <celier@adacore.com>
* projects.texi: Document that shared library projects, by
default, cannot import projects that are not shared library
projects.
2014-01-27 Robert Dewar <dewar@adacore.com>
* sem_ch8.adb (Find_Selected_Component): Use Replace instead
of Rewrite.
2014-01-27 Ed Schonberg <schonberg@adacore.com>
* a-suenco.adb, a-suenst.adb (Decode): Raise encoding error if
any other exception is raised.
(Convert): If both Input_Scheme and Output_Scheme are UTF_8 it is
still necessary to perform a conversion in order to remove overlong
encodings.
2014-01-27 Robert Dewar <dewar@adacore.com> 2014-01-27 Robert Dewar <dewar@adacore.com>
* exp_smem.adb: Minor reformatting. * exp_smem.adb: Minor reformatting.
......
gcc/ada/a-suenco.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2010-2012, Free Software Foundation, Inc. -- -- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
-- -- -- --
-- GNAT is free software; you can redistribute it and/or modify it under -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -41,9 +41,12 @@ package body Ada.Strings.UTF_Encoding.Conversions is ...@@ -41,9 +41,12 @@ package body Ada.Strings.UTF_Encoding.Conversions is
Output_BOM : Boolean := False) return UTF_String Output_BOM : Boolean := False) return UTF_String
is is
begin begin
-- Nothing to do if identical schemes -- Nothing to do if identical schemes, but for UTF_8 we need to
-- exclude overlong encodings, so need to do the full conversion.
if Input_Scheme = Output_Scheme then if Input_Scheme = Output_Scheme
and then Input_Scheme /= UTF_8
then
return Item; return Item;
-- For remaining cases, one or other of the operands is UTF-16BE/LE -- For remaining cases, one or other of the operands is UTF-16BE/LE
......
gcc/ada/a-suenst.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- B o d y --
-- -- -- --
-- Copyright (C) 2010-2012, Free Software Foundation, Inc. -- -- Copyright (C) 2010-2013, Free Software Foundation, Inc. --
-- -- -- --
-- GNAT is free software; you can redistribute it and/or modify it under -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -158,6 +158,12 @@ package body Ada.Strings.UTF_Encoding.Strings is ...@@ -158,6 +158,12 @@ package body Ada.Strings.UTF_Encoding.Strings is
end loop; end loop;
return Result (1 .. Len); return Result (1 .. Len);
exception
-- 'Val may have been out of range
when others =>
Raise_Encoding_Error (Iptr - 1);
end Decode; end Decode;
-- Decode UTF-16 input to String -- Decode UTF-16 input to String
......
gcc/ada/einfo.adb
...@@ -589,10 +589,10 @@ package body Einfo is ...@@ -589,10 +589,10 @@ package body Einfo is
----------------------- -----------------------
function Has_Option function Has_Option
(State : Entity_Id; (State_Id : Entity_Id;
Opt_Nam : Name_Id) return Boolean; Option_Nam : Name_Id) return Boolean;
-- Determine whether abstract state State has a particular option denoted -- Determine whether abstract state State_Id has particular option denoted
-- by the name Opt_Nam. -- by the name Option_Nam.
--------------- ---------------
-- Float_Rep -- -- Float_Rep --
...@@ -609,32 +609,55 @@ package body Einfo is ...@@ -609,32 +609,55 @@ package body Einfo is
---------------- ----------------
function Has_Option function Has_Option
(State : Entity_Id; (State_Id : Entity_Id;
Opt_Nam : Name_Id) return Boolean Option_Nam : Name_Id) return Boolean
is is
Par : constant Node_Id := Parent (State); Decl : constant Node_Id := Parent (State_Id);
Opt : Node_Id; Opt : Node_Id;
Opt_Nam : Node_Id;
begin begin
pragma Assert (Ekind (State) = E_Abstract_State); pragma Assert (Ekind (State_Id) = E_Abstract_State);
-- States with options appear as extension aggregates in the tree -- The declaration of abstract states with options appear as an
-- extension aggregate. If this is not the case, the option is not
-- available.
if Nkind (Par) = N_Extension_Aggregate then if Nkind (Decl) /= N_Extension_Aggregate then
if Opt_Nam = Name_Part_Of then return False;
return Present (Component_Associations (Par)); end if;
else -- Simple options
Opt := First (Expressions (Par));
while Present (Opt) loop
if Chars (Opt) = Opt_Nam then
return True;
end if;
Next (Opt); Opt := First (Expressions (Decl));
end loop; while Present (Opt) loop
-- Currently the only simple option allowed is External
if Nkind (Opt) = N_Identifier
and then Chars (Opt) = Name_External
and then Chars (Opt) = Option_Nam
then
return True;
end if; end if;
end if;
Next (Opt);
end loop;
-- Complex options with various specifiers
Opt := First (Component_Associations (Decl));
while Present (Opt) loop
Opt_Nam := First (Choices (Opt));
if Nkind (Opt_Nam) = N_Identifier
and then Chars (Opt_Nam) = Option_Nam
then
return True;
end if;
Next (Opt);
end loop;
return False; return False;
end Has_Option; end Has_Option;
......
gcc/ada/par-ch5.adb
...@@ -1739,14 +1739,13 @@ package body Ch5 is ...@@ -1739,14 +1739,13 @@ package body Ch5 is
elsif Prev_Token = Tok_In elsif Prev_Token = Tok_In
and then Present (Subtype_Indication (Node1)) and then Present (Subtype_Indication (Node1))
then then
-- Simplest recovery is to transform it into an element iterator. -- Simplest recovery is to transform it into an element iterator.
-- Error message on 'in" has already been emitted when parsing the -- Error message on 'in" has already been emitted when parsing the
-- optional constraint. -- optional constraint.
Set_Of_Present (Node1); Set_Of_Present (Node1);
Error_Msg_N Error_Msg_N
("subtype indication is only legal on on element iterator", ("subtype indication is only legal on an element iterator",
Subtype_Indication (Node1)); Subtype_Indication (Node1));
else else
......
gcc/ada/projects.texi
...@@ -1616,6 +1616,10 @@ implementation part of the library implies minimal post-compilation actions on ...@@ -1616,6 +1616,10 @@ implementation part of the library implies minimal post-compilation actions on
the complete system and potentially no action at all for the rest of the the complete system and potentially no action at all for the rest of the
system in the case of dynamic SALs. system in the case of dynamic SALs.
There is a restriction on shared library projects: by default, they are only
allowed to import other shared library projects. They are not allowed to
import non library projects or static library projects.
The GNAT Project Manager takes complete care of the library build, rebuild and The GNAT Project Manager takes complete care of the library build, rebuild and
installation tasks, including recompilation of the source files for which installation tasks, including recompilation of the source files for which
objects do not exist or are not up to date, assembly of the library archive, and objects do not exist or are not up to date, assembly of the library archive, and
......
gcc/ada/s-tposen.ads
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- -- -- --
-- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS -- -- GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS --
-- -- -- --
-- SYSTEM.TASKING.PROTECTED_OBJECTS.SINGLE_ENTRY -- -- SYSTEM.TASKING.PROTECTED_OBJECTS.SINGLE_ENTRY --
-- -- -- --
-- S p e c -- -- S p e c --
-- -- -- --
-- Copyright (C) 1992-2012, Free Software Foundation, Inc. -- -- Copyright (C) 1992-2013, Free Software Foundation, Inc. --
-- -- -- --
-- GNARL is free software; you can redistribute it and/or modify it under -- -- 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- -- -- 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- -- -- 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- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
...@@ -31,7 +31,7 @@ ...@@ -31,7 +31,7 @@
-- This package provides an optimized version of Protected_Objects.Operations -- This package provides an optimized version of Protected_Objects.Operations
-- and Protected_Objects.Entries making the following assumptions: -- and Protected_Objects.Entries making the following assumptions:
--
-- PO have only one entry -- PO have only one entry
-- There is only one caller at a time (No_Entry_Queue) -- There is only one caller at a time (No_Entry_Queue)
-- There is no dynamic priority support (No_Dynamic_Priorities) -- There is no dynamic priority support (No_Dynamic_Priorities)
...@@ -39,17 +39,17 @@ ...@@ -39,17 +39,17 @@
-- (No_Abort_Statements, Max_Asynchronous_Select_Nesting => 0) -- (No_Abort_Statements, Max_Asynchronous_Select_Nesting => 0)
-- PO are at library level -- PO are at library level
-- None of the tasks will terminate (no need for finalization) -- None of the tasks will terminate (no need for finalization)
--
-- This interface is intended to be used in the ravenscar profile, the -- This interface is intended to be used in the Ravenscar profile, the
-- compiler is responsible for ensuring that the conditions mentioned above -- compiler is responsible for ensuring that the conditions mentioned above
-- are respected, except for the No_Entry_Queue restriction that is checked -- are respected, except for the No_Entry_Queue restriction that is checked
-- dynamically in this package, since the check cannot be performed at compile -- dynamically in this package, since the check cannot be performed at compile
-- time, and is relatively cheap (see body). -- time, and is relatively cheap (see body).
--
-- This package is part of the high level tasking interface used by the -- This package is part of the high level tasking interface used by the
-- compiler to expand Ada 95 tasking constructs into simpler run time calls -- compiler to expand Ada 95 tasking constructs into simpler run time calls
-- (aka GNARLI, GNU Ada Run-time Library Interface) -- (aka GNARLI, GNU Ada Run-time Library Interface)
--
-- Note: the compiler generates direct calls to this interface, via Rtsfind. -- Note: the compiler generates direct calls to this interface, via Rtsfind.
-- Any changes to this interface may require corresponding compiler changes -- Any changes to this interface may require corresponding compiler changes
-- in exp_ch9.adb and possibly exp_ch7.adb -- in exp_ch9.adb and possibly exp_ch7.adb
...@@ -191,34 +191,34 @@ package System.Tasking.Protected_Objects.Single_Entry is ...@@ -191,34 +191,34 @@ package System.Tasking.Protected_Objects.Single_Entry is
-- to keep track of the runtime state of a protected object. -- to keep track of the runtime state of a protected object.
procedure Lock_Entry (Object : Protection_Entry_Access); procedure Lock_Entry (Object : Protection_Entry_Access);
-- Lock a protected object for write access. Upon return, the caller -- Lock a protected object for write access. Upon return, the caller owns
-- owns the lock to this object, and no other call to Lock or -- the lock to this object, and no other call to Lock or Lock_Read_Only
-- Lock_Read_Only with the same argument will return until the -- with the same argument will return until the corresponding call to
-- corresponding call to Unlock has been made by the caller. -- Unlock has been made by the caller.
procedure Lock_Read_Only_Entry procedure Lock_Read_Only_Entry
(Object : Protection_Entry_Access); (Object : Protection_Entry_Access);
-- Lock a protected object for read access. Upon return, the caller -- Lock a protected object for read access. Upon return, the caller owns
-- owns the lock for read access, and no other calls to Lock -- the lock for read access, and no other calls to Lock with the same
-- with the same argument will return until the corresponding call -- argument will return until the corresponding call to Unlock has been
-- to Unlock has been made by the caller. Other calls to Lock_Read_Only -- made by the caller. Other calls to Lock_Read_Only may (but need not)
-- may (but need not) return before the call to Unlock, and the -- return before the call to Unlock, and the corresponding callers will
-- corresponding callers will also own the lock for read access. -- also own the lock for read access.
procedure Unlock_Entry (Object : Protection_Entry_Access); procedure Unlock_Entry (Object : Protection_Entry_Access);
-- Relinquish ownership of the lock for the object represented by -- Relinquish ownership of the lock for the object represented by the
-- the Object parameter. If this ownership was for write access, or -- Object parameter. If this ownership was for write access, or if it was
-- if it was for read access where there are no other read access -- for read access where there are no other read access locks outstanding,
-- locks outstanding, one (or more, in the case of Lock_Read_Only) -- one (or more, in the case of Lock_Read_Only) of the tasks waiting on
-- of the tasks waiting on this lock (if any) will be given the -- this lock (if any) will be given the lock and allowed to return from
-- lock and allowed to return from the Lock or Lock_Read_Only call. -- the Lock or Lock_Read_Only call.
procedure Service_Entry (Object : Protection_Entry_Access); procedure Service_Entry (Object : Protection_Entry_Access);
-- Service the entry queue of the specified object, executing the -- Service the entry queue of the specified object, executing the
-- corresponding body of any queued entry call that is waiting on True -- corresponding body of any queued entry call that is waiting on True
-- barrier. This is used when the state of a protected object may have -- barrier. This is used when the state of a protected object may have
-- changed, in particular after the execution of the statement sequence of -- changed, in particular after the execution of the statement sequence
-- a protected procedure. -- of a protected procedure.
-- --
-- This must be called with abort deferred and with the corresponding -- This must be called with abort deferred and with the corresponding
-- object locked. Object is unlocked on return. -- object locked. Object is unlocked on return.
...@@ -227,9 +227,10 @@ package System.Tasking.Protected_Objects.Single_Entry is ...@@ -227,9 +227,10 @@ package System.Tasking.Protected_Objects.Single_Entry is
(Object : Protection_Entry_Access; (Object : Protection_Entry_Access;
Uninterpreted_Data : System.Address; Uninterpreted_Data : System.Address;
Mode : Call_Modes); Mode : Call_Modes);
-- Make a protected entry call to the specified object. -- Make a protected entry call to the specified object
-- Pend a protected entry call on the protected object represented --
-- by Object. A pended call is not queued; it may be executed immediately -- Pend a protected entry call on the protected object represented by
-- Object. A pended call is not queued; it may be executed immediately
-- or queued, depending on the state of the entry barrier. -- or queued, depending on the state of the entry barrier.
-- --
-- Uninterpreted_Data -- Uninterpreted_Data
...@@ -258,19 +259,18 @@ package System.Tasking.Protected_Objects.Single_Entry is ...@@ -258,19 +259,18 @@ package System.Tasking.Protected_Objects.Single_Entry is
procedure Exceptional_Complete_Single_Entry_Body procedure Exceptional_Complete_Single_Entry_Body
(Object : Protection_Entry_Access; (Object : Protection_Entry_Access;
Ex : Ada.Exceptions.Exception_Id); Ex : Ada.Exceptions.Exception_Id);
-- Perform all of the functions of Complete_Entry_Body. In addition, -- Perform all of the functions of Complete_Entry_Body. In addition, report
-- report in Ex the exception whose propagation terminated the entry -- in Ex the exception whose propagation terminated the entry body to the
-- body to the runtime system. -- runtime system.
function Protected_Count_Entry (Object : Protection_Entry) function Protected_Count_Entry (Object : Protection_Entry) return Natural;
return Natural;
-- Return the number of entry calls on Object (0 or 1) -- Return the number of entry calls on Object (0 or 1)
function Protected_Single_Entry_Caller (Object : Protection_Entry) function Protected_Single_Entry_Caller
return Task_Id; (Object : Protection_Entry) return Task_Id;
-- Return value of E'Caller, where E is the protected entry currently -- Return value of E'Caller, where E is the protected entry currently being
-- being handled. This will only work if called from within an -- handled. This will only work if called from within an entry body, as
-- entry body, as required by the LRM (C.7.1(14)). -- required by the LRM (C.7.1(14)).
private private
type Protection_Entry is record type Protection_Entry is record
......
gcc/ada/sem_ch8.adb
...@@ -6296,8 +6296,9 @@ package body Sem_Ch8 is ...@@ -6296,8 +6296,9 @@ package body Sem_Ch8 is
-- If no interpretation as an expanded name is possible, it -- If no interpretation as an expanded name is possible, it
-- must be a selected component of a record returned by a -- must be a selected component of a record returned by a
-- function call. Reformat prefix as a function call, the rest -- function call. Reformat prefix as a function call, the rest
-- is done by type resolution. If the prefix is procedure or -- is done by type resolution.
-- entry, as is P.X; this is an error.
-- Error if the prefix is procedure or entry, as is P.X
if Ekind (P_Name) /= E_Function if Ekind (P_Name) /= E_Function
and then and then
...@@ -6309,7 +6310,6 @@ package body Sem_Ch8 is ...@@ -6309,7 +6310,6 @@ package body Sem_Ch8 is
-- chain, the candidate package may be anywhere on it. -- chain, the candidate package may be anywhere on it.
if Present (Homonym (Current_Entity (P_Name))) then if Present (Homonym (Current_Entity (P_Name))) then
P_Name := Current_Entity (P_Name); P_Name := Current_Entity (P_Name);
while Present (P_Name) loop while Present (P_Name) loop
...@@ -6327,6 +6327,7 @@ package body Sem_Ch8 is ...@@ -6327,6 +6327,7 @@ package body Sem_Ch8 is
Set_Entity (Prefix (N), P_Name); Set_Entity (Prefix (N), P_Name);
Find_Expanded_Name (N); Find_Expanded_Name (N);
return; return;
else else
P_Name := Entity (Prefix (N)); P_Name := Entity (Prefix (N));
end if; end if;
...@@ -6338,11 +6339,27 @@ package body Sem_Ch8 is ...@@ -6338,11 +6339,27 @@ package body Sem_Ch8 is
Set_Entity (N, Any_Id); Set_Entity (N, Any_Id);
Set_Etype (N, Any_Type); Set_Etype (N, Any_Type);
-- Here we have a function call, so do the reformatting
else else
Nam := New_Copy (P); Nam := New_Copy (P);
Save_Interps (P, Nam); Save_Interps (P, Nam);
Rewrite (P,
-- We use Replace here because this is one of those cases
-- where the parser has missclassified the node, and we
-- fix things up and then do the semantic analysis on the
-- fixed up node. Normally we do this using one of the
-- Sinfo.CN routines, but this is too tricky for that.
-- Note that using Rewrite would be wrong, because we
-- would have a tree where the original node is unanalyzed,
-- and this violates the required interface for ASIS.
Replace (P,
Make_Function_Call (Sloc (P), Name => Nam)); Make_Function_Call (Sloc (P), Name => Nam));
-- Now analyze the reformatted node
Analyze_Call (P); Analyze_Call (P);
Analyze_Selected_Component (N); Analyze_Selected_Component (N);
end if; end if;
......
gcc/ada/sem_prag.adb
...@@ -22214,24 +22214,44 @@ package body Sem_Prag is ...@@ -22214,24 +22214,44 @@ package body Sem_Prag is
------------------------------- -------------------------------
procedure Analyze_Refinement_Clause (Clause : Node_Id) is procedure Analyze_Refinement_Clause (Clause : Node_Id) is
State_Id : Entity_Id := Empty; AR_Constit : Entity_Id := Empty;
-- The entity of the state being refined in the current clause AW_Constit : Entity_Id := Empty;
ER_Constit : Entity_Id := Empty;
EW_Constit : Entity_Id := Empty;
-- The entities of external constituents that contain one of the
-- following enabled properties: Async_Readers, Async_Writers,
-- Effective_Reads and Effective_Writes.
External_Constit_Seen : Boolean := False;
-- Flag used to mark when at least one external constituent is part
-- of the state refinement.
Non_Null_Seen : Boolean := False; Non_Null_Seen : Boolean := False;
Null_Seen : Boolean := False; Null_Seen : Boolean := False;
-- Flags used to detect multiple uses of null in a single clause or a -- Flags used to detect multiple uses of null in a single clause or a
-- mixture of null and non-null constituents. -- mixture of null and non-null constituents.
State : Node_Id;
State_Id : Entity_Id;
-- The state being refined in the current clause
procedure Analyze_Constituent (Constit : Node_Id); procedure Analyze_Constituent (Constit : Node_Id);
-- Perform full analysis of a single constituent -- Perform full analysis of a single constituent
procedure Check_Matching_State procedure Check_External_Property
(State : Node_Id; (Prop_Nam : Name_Id;
State_Id : Entity_Id); Enabled : Boolean;
-- Determine whether state State denoted by its name State_Id appears Constit : Entity_Id);
-- in Abstr_States. Emit an error when attempting to re-refine the -- Determine whether a property denoted by name Prop_Nam is present
-- state or when the state is not defined in the package declaration. -- in both the refined state and constituent Constit. Flag Enabled
-- Otherwise remove the state from Abstr_States. -- should be set when the property applies to the refined state. If
-- this is not the case, emit an error message.
procedure Check_Matching_State;
-- Determine whether the state being refined appears in Abstr_States.
-- Emit an error when attempting to re-refine the state or when the
-- state is not defined in the package declaration. Otherwise remove
-- the state from Abstr_States.
------------------------- -------------------------
-- Analyze_Constituent -- -- Analyze_Constituent --
...@@ -22276,6 +22296,29 @@ package body Sem_Prag is ...@@ -22276,6 +22296,29 @@ package body Sem_Prag is
-- body declarations end (see routine Analyze_Declarations). -- body declarations end (see routine Analyze_Declarations).
Set_Has_Visible_Refinement (State_Id); Set_Has_Visible_Refinement (State_Id);
-- When the constituent is external, save its relevant
-- property for further checks.
if Async_Readers_Enabled (Constit_Id) then
AR_Constit := Constit_Id;
External_Constit_Seen := True;
end if;
if Async_Writers_Enabled (Constit_Id) then
AW_Constit := Constit_Id;
External_Constit_Seen := True;
end if;
if Effective_Reads_Enabled (Constit_Id) then
ER_Constit := Constit_Id;
External_Constit_Seen := True;
end if;
if Effective_Writes_Enabled (Constit_Id) then
EW_Constit := Constit_Id;
External_Constit_Seen := True;
end if;
end Collect_Constituent; end Collect_Constituent;
-- Local variables -- Local variables
...@@ -22426,14 +22469,44 @@ package body Sem_Prag is ...@@ -22426,14 +22469,44 @@ package body Sem_Prag is
end if; end if;
end Analyze_Constituent; end Analyze_Constituent;
-----------------------------
-- Check_External_Property --
-----------------------------
procedure Check_External_Property
(Prop_Nam : Name_Id;
Enabled : Boolean;
Constit : Entity_Id)
is
begin
Error_Msg_Name_1 := Prop_Nam;
-- The property is enabled in the related Abstract_State pragma
-- that defines the state.
if Enabled then
if No (Constit) then
Error_Msg_NE
("external state & requires at least one constituent with "
& "property % (SPARK RM 7.2.8(3))", State, State_Id);
end if;
-- The property is missing in the declaration of the state, but a
-- constituent is introducing it in the state refinement.
elsif Present (Constit) then
Error_Msg_Name_2 := Chars (Constit);
Error_Msg_NE
("external state & lacks property % set by constituent % "
& "(SPARK RM 7.2.8(3))", State, State_Id);
end if;
end Check_External_Property;
-------------------------- --------------------------
-- Check_Matching_State -- -- Check_Matching_State --
-------------------------- --------------------------
procedure Check_Matching_State procedure Check_Matching_State is
(State : Node_Id;
State_Id : Entity_Id)
is
State_Elmt : Elmt_Id; State_Elmt : Elmt_Id;
begin begin
...@@ -22478,8 +22551,10 @@ package body Sem_Prag is ...@@ -22478,8 +22551,10 @@ package body Sem_Prag is
-- Local declarations -- Local declarations
Constit : Node_Id; Body_Ref : Node_Id;
State : Node_Id; Body_Ref_Elmt : Elmt_Id;
Constit : Node_Id;
Extra_State : Node_Id;
-- Start of processing for Analyze_Refinement_Clause -- Start of processing for Analyze_Refinement_Clause
...@@ -22487,67 +22562,60 @@ package body Sem_Prag is ...@@ -22487,67 +22562,60 @@ package body Sem_Prag is
-- Analyze the state name of a refinement clause -- Analyze the state name of a refinement clause
State := First (Choices (Clause)); State := First (Choices (Clause));
while Present (State) loop
if Present (State_Id) then
Error_Msg_N
("refinement clause cannot cover multiple states", State);
else Analyze (State);
Analyze (State); Resolve_State (State);
Resolve_State (State);
-- Ensure that the state name denotes a valid abstract state -- Ensure that the state name denotes a valid abstract state that is
-- that is defined in the spec of the related package. -- defined in the spec of the related package.
if Is_Entity_Name (State) then if Is_Entity_Name (State) then
State_Id := Entity_Of (State); State_Id := Entity_Of (State);
-- Catch any attempts to re-refine a state or refine a -- Catch any attempts to re-refine a state or refine a state that
-- state that is not defined in the package declaration. -- is not defined in the package declaration.
if Ekind (State_Id) = E_Abstract_State then if Ekind (State_Id) = E_Abstract_State then
Check_Matching_State (State, State_Id); Check_Matching_State;
else else
Error_Msg_NE Error_Msg_NE
("& must denote an abstract state", State, State_Id); ("& must denote an abstract state", State, State_Id);
end if; end if;
-- A global item cannot denote a state abstraction whose -- A global item cannot denote a state abstraction whose
-- refinement is visible, in other words a state abstraction -- refinement is visible, in other words a state abstraction
-- cannot be named within its enclosing package's body other -- cannot be named within its enclosing package's body other than
-- than in its refinement. -- in its refinement.
if Has_Body_References (State_Id) then if Has_Body_References (State_Id) then
declare Body_Ref_Elmt := First_Elmt (Body_References (State_Id));
Ref : Node_Id; while Present (Body_Ref_Elmt) loop
Ref_Elmt : Elmt_Id; Body_Ref := Node (Body_Ref_Elmt);
begin Error_Msg_N
Ref_Elmt := First_Elmt (Body_References (State_Id)); ("global reference to & not allowed (SPARK RM 6.1.4(8))",
while Present (Ref_Elmt) loop Body_Ref);
Ref := Node (Ref_Elmt); Error_Msg_Sloc := Sloc (State);
Error_Msg_N ("\refinement of & is visible#", Body_Ref);
Error_Msg_N Next_Elmt (Body_Ref_Elmt);
("global reference to & not allowed (SPARK RM " end loop;
& "6.1.4(8))", Ref); end if;
Error_Msg_Sloc := Sloc (State);
Error_Msg_N ("\refinement of & is visible#", Ref);
Next_Elmt (Ref_Elmt); -- The state name is illegal
end loop;
end;
end if;
-- The state name is illegal else
Error_Msg_N ("malformed state name in refinement clause", State);
end if;
else -- A refinement clause may only refine one state at a time
Error_Msg_N
("malformed state name in refinement clause", State);
end if;
end if;
Next (State); Extra_State := Next (State);
end loop;
if Present (Extra_State) then
Error_Msg_N
("refinement clause cannot cover multiple states", Extra_State);
end if;
-- Analyze all constituents of the refinement. Multiple constituents -- Analyze all constituents of the refinement. Multiple constituents
-- appear as an aggregate. -- appear as an aggregate.
...@@ -22575,6 +22643,60 @@ package body Sem_Prag is ...@@ -22575,6 +22643,60 @@ package body Sem_Prag is
else else
Analyze_Constituent (Constit); Analyze_Constituent (Constit);
end if; end if;
-- A refined external state is subject to special rules with respect
-- to its properties and constituents.
if Is_External_State (State_Id) then
-- The set of properties that all external constituents yield must
-- match that of the refined state. There are two cases to detect:
-- the refined state lacks a property or has an extra property.
if External_Constit_Seen then
Check_External_Property
(Prop_Nam => Name_Async_Readers,
Enabled => Async_Readers_Enabled (State_Id),
Constit => AR_Constit);
Check_External_Property
(Prop_Nam => Name_Async_Writers,
Enabled => Async_Writers_Enabled (State_Id),
Constit => AW_Constit);
Check_External_Property
(Prop_Nam => Name_Effective_Reads,
Enabled => Effective_Reads_Enabled (State_Id),
Constit => ER_Constit);
Check_External_Property
(Prop_Nam => Name_Effective_Writes,
Enabled => Effective_Writes_Enabled (State_Id),
Constit => EW_Constit);
-- An external state may be refined to null (SPARK RM 7.2.8(2))
elsif Null_Seen then
null;
-- The external state has constituents, but none of them are
-- external.
else
Error_Msg_NE
("external state & requires at least one external "
& "constituent or null refinement (SPARK RM 7.2.8(2))",
State, State_Id);
end if;
-- When a refined state is not external, it should not have external
-- constituents.
elsif External_Constit_Seen then
Error_Msg_NE
("non-external state & cannot contain external constituents in "
& "refinement (SPARK RM 7.2.8(1))", State, State_Id);
end if;
end Analyze_Refinement_Clause; end Analyze_Refinement_Clause;
--------------------------- ---------------------------
......
gcc/ada/sem_util.adb
...@@ -114,11 +114,11 @@ package body Sem_Util is ...@@ -114,11 +114,11 @@ package body Sem_Util is
-- have a default. -- have a default.
function Has_Enabled_Property function Has_Enabled_Property
(Extern : Node_Id; (State_Id : Node_Id;
Prop_Nam : Name_Id) return Boolean; Prop_Nam : Name_Id) return Boolean;
-- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled. -- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-- Given pragma External, determine whether it contains a property denoted -- Determine whether an abstract state denoted by its entity State_Id has
-- by its name Prop_Nam and if it does, whether its expression is True. -- enabled property Prop_Name.
function Has_Null_Extension (T : Entity_Id) return Boolean; function Has_Null_Extension (T : Entity_Id) return Boolean;
-- T is a derived tagged type. Check whether the type extension is null. -- T is a derived tagged type. Check whether the type extension is null.
...@@ -560,10 +560,7 @@ package body Sem_Util is ...@@ -560,10 +560,7 @@ package body Sem_Util is
function Async_Readers_Enabled (Id : Entity_Id) return Boolean is function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
begin begin
if Ekind (Id) = E_Abstract_State then if Ekind (Id) = E_Abstract_State then
return return Has_Enabled_Property (Id, Name_Async_Readers);
Has_Enabled_Property
(Extern => Get_Pragma (Id, Pragma_External),
Prop_Nam => Name_Async_Readers);
else pragma Assert (Ekind (Id) = E_Variable); else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Async_Readers)); return Present (Get_Pragma (Id, Pragma_Async_Readers));
...@@ -577,10 +574,7 @@ package body Sem_Util is ...@@ -577,10 +574,7 @@ package body Sem_Util is
function Async_Writers_Enabled (Id : Entity_Id) return Boolean is function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
begin begin
if Ekind (Id) = E_Abstract_State then if Ekind (Id) = E_Abstract_State then
return return Has_Enabled_Property (Id, Name_Async_Writers);
Has_Enabled_Property
(Extern => Get_Pragma (Id, Pragma_External),
Prop_Nam => Name_Async_Writers);
else pragma Assert (Ekind (Id) = E_Variable); else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Async_Writers)); return Present (Get_Pragma (Id, Pragma_Async_Writers));
...@@ -4818,10 +4812,7 @@ package body Sem_Util is ...@@ -4818,10 +4812,7 @@ package body Sem_Util is
function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
begin begin
if Ekind (Id) = E_Abstract_State then if Ekind (Id) = E_Abstract_State then
return return Has_Enabled_Property (Id, Name_Effective_Reads);
Has_Enabled_Property
(Extern => Get_Pragma (Id, Pragma_External),
Prop_Nam => Name_Effective_Reads);
else pragma Assert (Ekind (Id) = E_Variable); else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Effective_Reads)); return Present (Get_Pragma (Id, Pragma_Effective_Reads));
...@@ -4835,10 +4826,7 @@ package body Sem_Util is ...@@ -4835,10 +4826,7 @@ package body Sem_Util is
function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
begin begin
if Ekind (Id) = E_Abstract_State then if Ekind (Id) = E_Abstract_State then
return return Has_Enabled_Property (Id, Name_Effective_Writes);
Has_Enabled_Property
(Extern => Get_Pragma (Id, Pragma_External),
Prop_Nam => Name_Effective_Writes);
else pragma Assert (Ekind (Id) = E_Variable); else pragma Assert (Ekind (Id) = E_Variable);
return Present (Get_Pragma (Id, Pragma_Effective_Writes)); return Present (Get_Pragma (Id, Pragma_Effective_Writes));
...@@ -7182,69 +7170,86 @@ package body Sem_Util is ...@@ -7182,69 +7170,86 @@ package body Sem_Util is
-------------------------- --------------------------
function Has_Enabled_Property function Has_Enabled_Property
(Extern : Node_Id; (State_Id : Node_Id;
Prop_Nam : Name_Id) return Boolean Prop_Nam : Name_Id) return Boolean
is is
Prop : Node_Id; Decl : constant Node_Id := Parent (State_Id);
Props : Node_Id := Empty; Opt : Node_Id;
Opt_Nam : Node_Id;
Prop : Node_Id;
Props : Node_Id;
begin begin
-- The related abstract state or variable do not have an Extern pragma, -- The declaration of an external abstract state appears as an extension
-- the property in question cannot be set. -- aggregate. If this is not the case, properties can never be set.
if No (Extern) then if Nkind (Decl) /= N_Extension_Aggregate then
return False; return False;
elsif Nkind (Extern) = N_Component_Association then
Props := Expression (Extern);
end if; end if;
-- External state with properties -- When External appears as a simple option, it automatically enables
-- all properties.
if Present (Props) then Opt := First (Expressions (Decl));
while Present (Opt) loop
if Nkind (Opt) = N_Identifier
and then Chars (Opt) = Name_External
then
return True;
end if;
-- Multiple properties appear as an aggregate Next (Opt);
end loop;
if Nkind (Props) = N_Aggregate then -- When External specifies particular properties, inspect those and
-- find the desired one (if any).
-- Simple property form Opt := First (Component_Associations (Decl));
while Present (Opt) loop
Opt_Nam := First (Choices (Opt));
Prop := First (Expressions (Props)); if Nkind (Opt_Nam) = N_Identifier
while Present (Prop) loop and then Chars (Opt_Nam) = Name_External
if Chars (Prop) = Prop_Nam then then
return True; Props := Expression (Opt);
end if;
Next (Prop); -- Multiple properties appear as an aggregate
end loop;
-- Property with expression form if Nkind (Props) = N_Aggregate then
Prop := First (Component_Associations (Props)); -- Simple property form
while Present (Prop) loop
if Chars (Prop) = Prop_Nam then
return Is_True (Expr_Value (Expression (Prop)));
end if;
Next (Prop); Prop := First (Expressions (Props));
end loop; while Present (Prop) loop
if Chars (Prop) = Prop_Nam then
return True;
end if;
Next (Prop);
end loop;
-- Pragma Extern contains properties, but not the one we want -- Property with expression form
return False; Prop := First (Component_Associations (Props));
while Present (Prop) loop
if Chars (Prop) = Prop_Nam then
return Is_True (Expr_Value (Expression (Prop)));
end if;
Next (Prop);
end loop;
-- Single property -- Single property
else else
return Chars (Prop) = Prop_Nam; return Chars (Prop) = Prop_Nam;
end if;
end if; end if;
-- An external state defined without any properties defaults all Next (Opt);
-- properties to True; end loop;
else return False;
return True;
end if;
end Has_Enabled_Property; end Has_Enabled_Property;
-------------------- --------------------
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment