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 <[email protected]>
* 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.
Index: einfo.ads
===================================================================
--- einfo.ads (revision 207120)
+++ einfo.ads (working copy)
@@ -2343,11 +2343,15 @@
-- Is_Ghost_Entity (synthesized)
-- Applies to all entities. Yields True for a subprogram or a whole
--- object that has convention Ghost.
+-- object that has convention Ghost. For now only functions can have
+-- Ghost convention, so this will be false for other than functions,
+-- but we expect that to change in the future.
-- Is_Ghost_Subprogram (synthesized)
-- Applies to all entities. Yields True for a subprogram that has a Ghost
--- convention.
+-- convention. Note: for now, only ghost functions are allowed, so this
+-- will always be false for procedures, but that is expected to change in
+-- the future.
-- Is_Hidden (Flag57)
-- Defined in all entities. Set for all entities declared in the
Index: einfo.adb
===================================================================
--- einfo.adb (revision 207120)
+++ einfo.adb (working copy)
@@ -6886,6 +6886,10 @@
-- Is_Ghost_Entity --
---------------------
+ -- Note: coding below allows for ghost variables. They are not currently
+ -- implemented, so we will always get False for variables, but that is
+ -- expected to change in the future.
+
function Is_Ghost_Entity (Id : E) return B is
begin
if Present (Id) and then Ekind (Id) = E_Variable then
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 207134)
+++ sem_prag.adb (working copy)
@@ -6029,7 +6029,8 @@
-- Set convention in entity E, and also flag that the entity has a
-- convention pragma. If entity is for a private or incomplete type,
-- also set convention and flag on underlying type. This procedure
- -- also deals with the special case of C_Pass_By_Copy convention.
+ -- also deals with the special case of C_Pass_By_Copy convention,
+ -- and error checks for inappropriate convention specification.
-------------------------------
-- Diagnose_Multiple_Pragmas --
@@ -6191,6 +6192,16 @@
procedure Set_Convention_From_Pragma (E : Entity_Id) is
begin
+ -- Ghost convention is allowed only for functions
+
+ if Ekind (E) /= E_Function and then C = Convention_Ghost then
+ Error_Msg_N
+ ("& may not have Ghost convention", E);
+ Error_Msg_N
+ ("\only functions are permitted to have Ghost convention", E);
+ return;
+ end if;
+
-- Ada 2005 (AI-430): Check invalid attempt to change convention
-- for an overridden dispatching operation. Technically this is
-- an amendment and should only be done in Ada 2005 mode. However,
@@ -6201,11 +6212,11 @@
and then Present (Overridden_Operation (E))
and then C /= Convention (Overridden_Operation (E))
then
- -- An attempt to override a subprogram with a ghost subprogram
+ -- An attempt to override a function with a ghost function
-- appears as a mismatch in conventions.
if C = Convention_Ghost then
- Error_Msg_N ("ghost subprogram & cannot be overriding", E);
+ Error_Msg_N ("ghost function & cannot be overriding", E);
else
Error_Pragma_Arg
("cannot change convention for overridden dispatching "
@@ -6401,7 +6412,7 @@
if Is_Ghost_Subprogram (E)
and then Present (Overridden_Operation (E))
then
- Error_Msg_N ("ghost subprogram & cannot be overriding", E);
+ Error_Msg_N ("ghost function & cannot be overriding", E);
end if;
-- Go to renamed subprogram if present, since convention applies to
