[multiple changes]
2013-10-17 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Is_Matching_Input): Account for the case where a state with a null refinement appears as the last input of a refinement clause. 2013-10-17 Robert Dewar <dewar@adacore.com> * sem_aux.ads, sem_aux.adb: Minor reformatting. From-SVN: r203766
This commit is contained in:
parent
8b58a06044
commit
72d1b27a2a
4 changed files with 128 additions and 104 deletions
|
@ -1,3 +1,13 @@
|
|||
2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_prag.adb (Is_Matching_Input): Account
|
||||
for the case where a state with a null refinement appears as
|
||||
the last input of a refinement clause.
|
||||
|
||||
2013-10-17 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem_aux.ads, sem_aux.adb: Minor reformatting.
|
||||
|
||||
2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* aspects.adb, aspects.ads, sem_prag.ads: Remove all entries
|
||||
|
|
|
@ -813,105 +813,6 @@ package body Sem_Aux is
|
|||
end if;
|
||||
end Is_Generic_Formal;
|
||||
|
||||
---------------------
|
||||
-- Is_Limited_View --
|
||||
---------------------
|
||||
|
||||
function Is_Limited_View (Ent : Entity_Id) return Boolean is
|
||||
Btype : constant Entity_Id := Available_View (Base_Type (Ent));
|
||||
|
||||
begin
|
||||
if Is_Limited_Record (Btype) then
|
||||
return True;
|
||||
|
||||
elsif Ekind (Btype) = E_Limited_Private_Type
|
||||
and then Nkind (Parent (Btype)) = N_Formal_Type_Declaration
|
||||
then
|
||||
return not In_Package_Body (Scope ((Btype)));
|
||||
|
||||
elsif Is_Private_Type (Btype) then
|
||||
|
||||
-- AI05-0063: A type derived from a limited private formal type is
|
||||
-- not immutably limited in a generic body.
|
||||
|
||||
if Is_Derived_Type (Btype)
|
||||
and then Is_Generic_Type (Etype (Btype))
|
||||
then
|
||||
if not Is_Limited_Type (Etype (Btype)) then
|
||||
return False;
|
||||
|
||||
-- A descendant of a limited formal type is not immutably limited
|
||||
-- in the generic body, or in the body of a generic child.
|
||||
|
||||
elsif Ekind (Scope (Etype (Btype))) = E_Generic_Package then
|
||||
return not In_Package_Body (Scope (Btype));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
|
||||
else
|
||||
declare
|
||||
Utyp : constant Entity_Id := Underlying_Type (Btype);
|
||||
begin
|
||||
if No (Utyp) then
|
||||
return False;
|
||||
else
|
||||
return Is_Limited_View (Utyp);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
elsif Is_Concurrent_Type (Btype) then
|
||||
return True;
|
||||
|
||||
elsif Is_Record_Type (Btype) then
|
||||
|
||||
-- Note that we return True for all limited interfaces, even though
|
||||
-- (unsynchronized) limited interfaces can have descendants that are
|
||||
-- nonlimited, because this is a predicate on the type itself, and
|
||||
-- things like functions with limited interface results need to be
|
||||
-- handled as build in place even though they might return objects
|
||||
-- of a type that is not inherently limited.
|
||||
|
||||
if Is_Class_Wide_Type (Btype) then
|
||||
return Is_Limited_View (Root_Type (Btype));
|
||||
|
||||
else
|
||||
declare
|
||||
C : Entity_Id;
|
||||
|
||||
begin
|
||||
C := First_Component (Btype);
|
||||
while Present (C) loop
|
||||
|
||||
-- Don't consider components with interface types (which can
|
||||
-- only occur in the case of a _parent component anyway).
|
||||
-- They don't have any components, plus it would cause this
|
||||
-- function to return true for nonlimited types derived from
|
||||
-- limited interfaces.
|
||||
|
||||
if not Is_Interface (Etype (C))
|
||||
and then Is_Limited_View (Etype (C))
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
C := Next_Component (C);
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return False;
|
||||
end if;
|
||||
|
||||
elsif Is_Array_Type (Btype) then
|
||||
return Is_Limited_View (Component_Type (Btype));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Is_Limited_View;
|
||||
|
||||
-------------------------------
|
||||
-- Is_Immutably_Limited_Type --
|
||||
-------------------------------
|
||||
|
@ -1081,6 +982,105 @@ package body Sem_Aux is
|
|||
end if;
|
||||
end Is_Limited_Type;
|
||||
|
||||
---------------------
|
||||
-- Is_Limited_View --
|
||||
---------------------
|
||||
|
||||
function Is_Limited_View (Ent : Entity_Id) return Boolean is
|
||||
Btype : constant Entity_Id := Available_View (Base_Type (Ent));
|
||||
|
||||
begin
|
||||
if Is_Limited_Record (Btype) then
|
||||
return True;
|
||||
|
||||
elsif Ekind (Btype) = E_Limited_Private_Type
|
||||
and then Nkind (Parent (Btype)) = N_Formal_Type_Declaration
|
||||
then
|
||||
return not In_Package_Body (Scope ((Btype)));
|
||||
|
||||
elsif Is_Private_Type (Btype) then
|
||||
|
||||
-- AI05-0063: A type derived from a limited private formal type is
|
||||
-- not immutably limited in a generic body.
|
||||
|
||||
if Is_Derived_Type (Btype)
|
||||
and then Is_Generic_Type (Etype (Btype))
|
||||
then
|
||||
if not Is_Limited_Type (Etype (Btype)) then
|
||||
return False;
|
||||
|
||||
-- A descendant of a limited formal type is not immutably limited
|
||||
-- in the generic body, or in the body of a generic child.
|
||||
|
||||
elsif Ekind (Scope (Etype (Btype))) = E_Generic_Package then
|
||||
return not In_Package_Body (Scope (Btype));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
|
||||
else
|
||||
declare
|
||||
Utyp : constant Entity_Id := Underlying_Type (Btype);
|
||||
begin
|
||||
if No (Utyp) then
|
||||
return False;
|
||||
else
|
||||
return Is_Limited_View (Utyp);
|
||||
end if;
|
||||
end;
|
||||
end if;
|
||||
|
||||
elsif Is_Concurrent_Type (Btype) then
|
||||
return True;
|
||||
|
||||
elsif Is_Record_Type (Btype) then
|
||||
|
||||
-- Note that we return True for all limited interfaces, even though
|
||||
-- (unsynchronized) limited interfaces can have descendants that are
|
||||
-- nonlimited, because this is a predicate on the type itself, and
|
||||
-- things like functions with limited interface results need to be
|
||||
-- handled as build in place even though they might return objects
|
||||
-- of a type that is not inherently limited.
|
||||
|
||||
if Is_Class_Wide_Type (Btype) then
|
||||
return Is_Limited_View (Root_Type (Btype));
|
||||
|
||||
else
|
||||
declare
|
||||
C : Entity_Id;
|
||||
|
||||
begin
|
||||
C := First_Component (Btype);
|
||||
while Present (C) loop
|
||||
|
||||
-- Don't consider components with interface types (which can
|
||||
-- only occur in the case of a _parent component anyway).
|
||||
-- They don't have any components, plus it would cause this
|
||||
-- function to return true for nonlimited types derived from
|
||||
-- limited interfaces.
|
||||
|
||||
if not Is_Interface (Etype (C))
|
||||
and then Is_Limited_View (Etype (C))
|
||||
then
|
||||
return True;
|
||||
end if;
|
||||
|
||||
C := Next_Component (C);
|
||||
end loop;
|
||||
end;
|
||||
|
||||
return False;
|
||||
end if;
|
||||
|
||||
elsif Is_Array_Type (Btype) then
|
||||
return Is_Limited_View (Component_Type (Btype));
|
||||
|
||||
else
|
||||
return False;
|
||||
end if;
|
||||
end Is_Limited_View;
|
||||
|
||||
----------------------
|
||||
-- Nearest_Ancestor --
|
||||
----------------------
|
||||
|
|
|
@ -283,7 +283,7 @@ package Sem_Aux is
|
|||
function Is_Immutably_Limited_Type (Ent : Entity_Id) return Boolean;
|
||||
-- Implements definition in Ada 2012 RM-7.5 (8.1/3). This differs from the
|
||||
-- following predicate in that an untagged record with immutably limited
|
||||
-- components is NOT by itself immutably limited. This matters, eg. when
|
||||
-- components is NOT by itself immutably limited. This matters, e.g. when
|
||||
-- checking the legality of an access to the current instance.
|
||||
|
||||
function Is_Limited_View (Ent : Entity_Id) return Boolean;
|
||||
|
@ -301,7 +301,7 @@ package Sem_Aux is
|
|||
-- private type, limited interface type, task type, protected type,
|
||||
-- composite containing a limited component, or a subtype of any of
|
||||
-- these types). This older routine overlaps with the previous one, this
|
||||
-- should be cleaned up?
|
||||
-- should be cleaned up???
|
||||
|
||||
function Nearest_Ancestor (Typ : Entity_Id) return Entity_Id;
|
||||
-- Given a subtype Typ, this function finds out the nearest ancestor from
|
||||
|
|
|
@ -20004,17 +20004,17 @@ package body Sem_Prag is
|
|||
-- A state with a null refinement matches either a
|
||||
-- null input list or nothing at all (no input):
|
||||
|
||||
-- Refined_State (State => null)
|
||||
-- Refined_State => (State => null)
|
||||
|
||||
-- No input
|
||||
|
||||
-- Depends => (<output> => (State, Input))
|
||||
-- Refined_Depends => (<output> => Input -- OK
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
-- Null input list
|
||||
|
||||
-- Depends => (<output> => State)
|
||||
-- Refined_Depends => (<output> => null) -- OK
|
||||
-- Refined_Depends => (<output> => null) -- OK
|
||||
|
||||
if Has_Null_Refinement (Dep_Id) then
|
||||
Has_Null_State := True;
|
||||
|
@ -20073,6 +20073,20 @@ package body Sem_Prag is
|
|||
|
||||
Ref_Input := Next_Ref_Input;
|
||||
end loop;
|
||||
|
||||
-- When a state with a null refinement appears as the last
|
||||
-- input, it matches nothing:
|
||||
|
||||
-- Refined_State => (State => null)
|
||||
-- Depends => (<output> => (Input, State))
|
||||
-- Refined_Depends => (<output> => Input) -- OK
|
||||
|
||||
if Ekind (Dep_Id) = E_Abstract_State
|
||||
and then Has_Null_Refinement (Dep_Id)
|
||||
and then No (Ref_Input)
|
||||
then
|
||||
Has_Null_State := True;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- A state with visible refinement was matched against one or
|
||||
|
|
Loading…
Add table
Reference in a new issue