This patch removes the (incorrect) implementation of the following rule:
SPARK RM 6.9 (11) - A non-ghost library unit package or generic package
specification shall not require a completion solely because of ghost
declarations. [In other words, if a library unit package or generic package
specification requires a body, then it must still require a body if all of
the ghost declarations therein were to be removed.
The patch also updates references to SPARK RM 6.9 in various compiler files.
Tested on x86_64-pc-linux-gnu, committed on trunk
2015-05-22 Hristian Kirtchev <kirtc...@adacore.com>
* ghost.adb (Check_Ghost_Completion): Update references to SPARK
RM 6.9 rules.
(Check_Ghost_Policy): Update references to SPARK RM 6.9 rules.
* sem_ch3.adb (Analyze_Object_Declaration): Update references
to SPARK RM 6.9 rules.
(Check_Completion): Ghost entities do not require a special form of
completion.
* sem_ch6.adb (Analyze_Generic_Subprogram_Body): Update references
to SPARK RM 6.9 rules.
(Analyze_Subprogram_Body_Helper): Update references to SPARK RM 6.9
rules.
* sem_ch7.adb (Analyze_Package_Body_Helper): Update references
to SPARK RM 6.9 rules.
(Requires_Completion_In_Body): Ghost entities do not require a special
form of completion.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 223484)
+++ sem_ch3.adb (working copy)
@@ -4055,7 +4055,7 @@
-- The Ghost policy in effect at the point of declaration
-- and at the point of completion must match
- -- (SPARK RM 6.9(15)).
+ -- (SPARK RM 6.9(14)).
if Present (Prev_Entity)
and then Is_Ghost_Entity (Prev_Entity)
@@ -4237,7 +4237,7 @@
Set_Is_Ghost_Entity (Id);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(16)).
+ -- point of completion must match (SPARK RM 6.9(14)).
if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then
Check_Ghost_Completion (Prev_Entity, Id);
@@ -10937,12 +10937,6 @@
if Is_Intrinsic_Subprogram (E) then
null;
- -- A Ghost entity declared in a non-Ghost package does not force the
- -- need for a body (SPARK RM 6.9(11)).
-
- elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (E) then
- null;
-
-- The following situation requires special handling: a child unit
-- that appears in the context clause of the body of its parent:
@@ -19964,7 +19958,7 @@
Set_Is_Ghost_Entity (Full_T);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(15)).
+ -- point of completion must match (SPARK RM 6.9(14)).
Check_Ghost_Completion (Priv_T, Full_T);
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb (revision 223476)
+++ sem_ch7.adb (working copy)
@@ -750,7 +750,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(15)).
+ -- point of completion must match (SPARK RM 6.9(14)).
Check_Ghost_Completion (Spec_Id, Body_Id);
end if;
@@ -2527,12 +2527,6 @@
then
return False;
- -- A Ghost entity declared in a non-Ghost package does not force the
- -- need for a body (SPARK RM 6.9(11)).
-
- elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (Id) then
- return False;
-
-- Otherwise test to see if entity requires a completion. Note that
-- subprogram entities whose declaration does not come from source are
-- ignored here on the basis that we assume the expander will provide an
Index: ghost.adb
===================================================================
--- ghost.adb (revision 223476)
+++ ghost.adb (working copy)
@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
--- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2014-2015, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@@ -106,7 +106,7 @@
begin
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(15)).
+ -- point of completion must match (SPARK RM 6.9(14)).
if Is_Checked_Ghost_Entity (Partial_View)
and then Policy = Name_Ignore
@@ -411,7 +411,7 @@
else
Error_Msg_N
- ("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
+ ("ghost entity cannot appear in this context (SPARK RM 6.9(11))",
Ghost_Ref);
end if;
end Check_Ghost_Context;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 223476)
+++ sem_ch6.adb (working copy)
@@ -1267,7 +1267,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and at
- -- the point of completion must match (SPARK RM 6.9(15)).
+ -- the point of completion must match (SPARK RM 6.9(14)).
Check_Ghost_Completion (Gen_Id, Body_Id);
end if;
@@ -3265,7 +3265,7 @@
Set_Is_Ghost_Entity (Body_Id);
-- The Ghost policy in effect at the point of declaration and
- -- at the point of completion must match (SPARK RM 6.9(15)).
+ -- at the point of completion must match (SPARK RM 6.9(14)).
Check_Ghost_Completion (Spec_Id, Body_Id);
end if;
