diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-05-21 12:48:37 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2014-05-21 12:48:37 +0200 |
| commit | 2735b82d096137ab53517510fd3669e60a663915 (patch) | |
| tree | 2b61dc53cf097856ce13cbea844e143b7a52001a /gcc/ada/sem_prag.adb | |
| parent | 149604e46a31c3f1a22194e61ba3a0f01903de03 (diff) | |
| download | gcc-2735b82d096137ab53517510fd3669e60a663915.zip gcc-2735b82d096137ab53517510fd3669e60a663915.tar.gz gcc-2735b82d096137ab53517510fd3669e60a663915.tar.bz2 | |
[multiple changes]
2014-05-21 Robert Dewar <dewar@adacore.com>
* einfo.ads: Minor reformatting.
* ceinfo.adb: Deal with slight format change of einfo.ads.
2014-05-21 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Analyze_Part_Of): Further work on the proper
implementation of the SPARK 2014 rule concerning private child
units (LRM 7.2.6).
2014-05-21 Vincent Celier <celier@adacore.com>
* makeusg.adb: Add switch -d to usage.
2014-05-21 Ed Schonberg <schonberg@adacore.com>
* sem_util.adb (Find_Actual): If an actual that is the prefix
of an enclosing prefixed call has been rewritten, use Nkind
and Sloc to identify the corresponding formal, when handling
deferred references.
2014-05-21 Robert Dewar <dewar@adacore.com>
* debug.adb: Document -gnatd.z switch.
* sem_eval.adb (Why_Non_Static): Test -gnatd.z switch.
From-SVN: r210689
Diffstat (limited to 'gcc/ada/sem_prag.adb')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 41 |
1 files changed, 30 insertions, 11 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 05e29f7..c8ef01a 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -3444,9 +3444,10 @@ package body Sem_Prag is Indic : Node_Id; Legal : out Boolean) is - Pack_Id : Entity_Id; - Placement : State_Space_Kind; - State_Id : Entity_Id; + Pack_Id : Entity_Id; + Placement : State_Space_Kind; + Parent_Unit : Entity_Id; + State_Id : Entity_Id; begin -- Assume that the pragma/option is illegal @@ -3509,22 +3510,40 @@ package body Sem_Prag is if Is_Child_Unit (Pack_Id) and then Is_Private_Descendant (Pack_Id) then + -- A variable or state abstraction which is part of the + -- visible state of a private child unit (or a public + -- descendant thereof) shall have its Part_Of indicator + -- specified; the Part_Of indicator shall denote a state + -- abstraction declared by either the parent unit of the + -- private unit or by a public descendant of that parent unit. + + -- Find parent unit of nearest private ancestor. + + Parent_Unit := Pack_Id; + while Present (Parent_Unit) loop + exit when Private_Present + (Parent (Unit_Declaration_Node (Parent_Unit))); + Parent_Unit := Scope (Parent_Unit); + end loop; + + Parent_Unit := Scope (Parent_Unit); + if not Is_Child_Or_Sibling (Pack_Id, Scope (State_Id)) then Error_Msg_N ("indicator Part_Of must denote an abstract state of " & "parent unit or descendant (SPARK RM 7.2.6(3))", Indic); - -- If the unit is a public child of a private unit it cannot - -- refine the state of a private parent, only that of a - -- public ancestor or descendant thereof. - - elsif not Private_Present - (Parent (Unit_Declaration_Node (Pack_Id))) - and then Is_Private_Descendant (Scope (State_Id)) + elsif Scope (State_Id) = Parent_Unit + or else (Is_Ancestor_Package (Parent_Unit, Scope (State_Id)) + and then + not Is_Private_Descendant (Scope (State_Id))) then + null; + + else Error_Msg_N ("indicator Part_Of must denote the abstract state of " - & "a public ancestor", State); + & "parent of private ancestor", State); end if; -- Indicator Part_Of is not needed when the related package is not |