[Ada] Check for illegal global refs to abstract state when refinement visible

[Arnaud Charlet <charlet at adacore dot com>]

This implements the rule in SPARK RM (6.1.5(4)): A global item shall
not denote a state abstraction whose refinement is visible (a state
abstraction cannot be named within its enclosing package's body other
than in its refinement).

The following is compiled with -gnatd.V

     1. package Depends_Illegal
     2.    with Abstract_State => A
     3. is
     4.    pragma Elaborate_Body (Depends_Illegal);
     5. end Depends_Illegal;

     1. package body Depends_Illegal
     2.    with Refined_State => (A => (X, Y))
     3. is
     4.    X, Y : Natural := 0;
     5.    function F1 (Par1 : Natural) return Natural
     6.       with Global  => A,
                              |
        >>> global reference to "A" not allowed (SPARK RM 6.1.5(4))
        >>> refinement of "A" is visible at line 2

     7.            Depends => (F1'Result => A,
                                            |
        >>> global reference to "A" not allowed (SPARK RM 6.1.5(4))
        >>> refinement of "A" is visible at line 2

     8.                        null      => Par1)
     9.    is
    10.    begin
    11.       return X;
    12.    end F1;
    13. end Depends_Illegal;

Tested on x86_64-pc-linux-gnu, committed on trunk

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* einfo.ads, einfo.adb (Has_Body_References): New flag.
	(Body_References): New field.
	* sem_prag.adb (Record_Possible_Body_Reference): New procedure
	(Analyze_Input_Output): Call Record_Possible_Body_Reference
	(Analyze_Global_Item): Call Record_Possible_Body_Reference
	(Analyze_Refinement_Clause): Output messages if illegal global refs.

Attachment: difs
Description: Text document