[Ada] Only functions can have Ghost convention

[Arnaud Charlet <charlet at adacore dot com>]

This implements the rule in SPARK RM 6.1.6 which specifies that only
functions may have convention Ghost explicitly specified. This test
program shows error messages not previously given (compiled with
-gnatc -gnatj60)

     1. package Ghost_Illegal_1
     2.   with SPARK_Mode
     3. is
     4.    --  TU: 6.1.6 LR
     5.    --  Only functions can be explicitly
     6.    --  declared with Convention => Ghost.
     7.
     8.    Ghost_Var : Integer
           |
        >>> "Ghost_Var" may not have Ghost convention, only
            functions are permitted to have Ghost convention

     9.      with Convention => Ghost;
    10.
    11.    X : exception
           |
        >>> "X" may not have Ghost convention, only
            functions are permitted to have Ghost convention

    12.      with Convention => Ghost;
    13.
    14.    procedure Ghost_Proc
                     |
        >>> "Ghost_Proc" may not have Ghost convention,
            only functions are permitted to have Ghost
            convention

    15.      with Convention => Ghost;
    16.
    17.    function Ghost_Func return Boolean
    18.      with Convention => Ghost;
    19. end Ghost_Illegal_1;

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

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

	* sem_prag.adb (Set_Convention_From_Pragma): Check that
	convention Ghost can only apply to functions.
	* einfo.ads, einfo.adb (Is_Ghost_Subprogram): Add clarifying comment.

Attachment: difs
Description: Text document