https://gcc.gnu.org/g:df48963b9553a51023c0d115bdf6205309e04bfe
commit r15-446-gdf48963b9553a51023c0d115bdf6205309e04bfe
Author: Yannick Moy <m...@adacore.com>
Date: Fri Feb 2 18:20:06 2024 +0100
ada: Update of SPARK RM legality rules on ghost code
Update checking of ghost code after a small change in SPARK RM
rules 6.9(15) and 6.9(20), so that the Ghost assertion policy
that matters when checking the validity of a reference to a ghost entity
in an assertion expression is the Ghost assertion policy at the point
of declaration of the entity.
Also fix references to SPARK RM rules in comments, which were off by two
in many cases after the insertion of rules 13 and 14 regarding generic
instantiations.
gcc/ada/
* contracts.adb: Fix references to SPARK RM rules.
* freeze.adb: Same.
* ghost.adb: Fix references to SPARK RM rules.
(Check_Ghost_Context): Update checking of references to
ghost entities in assertion expressions.
* sem_ch6.adb: Fix references to SPARK RM rules.
* sem_prag.adb: Same.
Diff:
---
gcc/ada/contracts.adb | 2 +-
gcc/ada/freeze.adb | 2 +-
gcc/ada/ghost.adb | 44 ++++++++++++++++++++++++--------------------
gcc/ada/sem_ch6.adb | 14 +++++++-------
gcc/ada/sem_prag.adb | 12 ++++++------
5 files changed, 39 insertions(+), 35 deletions(-)
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 810b360fb94e..9fc9e05db687 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1114,7 +1114,7 @@ package body Contracts is
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
-- A Ghost object cannot be of a type that yields a synchronized
- -- object (SPARK RM 6.9(19)).
+ -- object (SPARK RM 6.9(21)).
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index dd4eff1ed199..a980c7e5b47a 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -4094,7 +4094,7 @@ package body Freeze is
<<Skip_Packed>>
-- A Ghost type cannot have a component of protected or task type
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
Error_Msg_N
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 677089039e8b..d220e0e1ec0d 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -121,7 +121,7 @@ package body Ghost is
null;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
elsif Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
@@ -173,9 +173,9 @@ package body Ghost is
--
-- * Be subject to pragma Ghost
- function Is_OK_Pragma (Prag : Node_Id) return Boolean;
+ function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean;
-- Determine whether node Prag is a suitable context for a reference
- -- to a Ghost entity. To qualify as such, Prag must either
+ -- to a Ghost entity Id. To qualify as such, Prag must either
--
-- * Be an assertion expression pragma
--
@@ -318,9 +318,11 @@ package body Ghost is
-- Is_OK_Pragma --
------------------
- function Is_OK_Pragma (Prag : Node_Id) return Boolean is
+ function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean
+ is
procedure Check_Policies (Prag_Nam : Name_Id);
- -- Verify that the Ghost policy in effect is the same as the
+ -- Verify that the Ghost policy in effect at the point of the
+ -- declaration of Ghost entity Id (if present) is the same as the
-- assertion policy for pragma name Prag_Nam. Emit an error if
-- this is not the case.
@@ -330,14 +332,16 @@ package body Ghost is
procedure Check_Policies (Prag_Nam : Name_Id) is
AP : constant Name_Id := Check_Kind (Prag_Nam);
- GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
- -- If the Ghost policy in effect at the point of a Ghost entity
- -- reference is Ignore, then the assertion policy of the pragma
- -- must be Ignore (SPARK RM 6.9(18)).
+ -- If the Ghost policy in effect at the point of the
+ -- declaration of Ghost entity Id is Ignore, then the assertion
+ -- policy of the pragma must be Ignore (SPARK RM 6.9(20)).
- if GP = Name_Ignore and then AP /= Name_Ignore then
+ if Present (Id)
+ and then not Is_Checked_Ghost_Entity (Id)
+ and then AP /= Name_Ignore
+ then
Error_Msg_N
("incompatible ghost policies in effect",
Ghost_Ref);
@@ -388,7 +392,7 @@ package body Ghost is
and then Prag_Id /= Pragma_Predicate
then
-- Ensure that the assertion policy and the Ghost policy are
- -- compatible (SPARK RM 6.9(18)).
+ -- compatible (SPARK RM 6.9(20)).
Check_Policies (Prag_Nam);
return True;
@@ -535,7 +539,7 @@ package body Ghost is
elsif Is_OK_Declaration (Par) then
return True;
- elsif Is_OK_Pragma (Par) then
+ elsif Is_OK_Pragma (Par, Ghost_Id) then
return True;
elsif Is_OK_Statement (Par) then
@@ -576,7 +580,7 @@ package body Ghost is
begin
-- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(13)).
+ -- point of use must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Id)
and then Policy = Name_Ignore
@@ -859,7 +863,7 @@ package body Ghost is
-- When a tagged type is either non-Ghost or checked Ghost and
-- one of its primitives overrides an inherited operation, the
-- overridden operation of the ancestor type must be ignored Ghost
- -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
+ -- if the primitive is ignored Ghost (SPARK RM 6.9(19)).
if Is_Ignored_Ghost_Entity (Subp) then
@@ -900,7 +904,7 @@ package body Ghost is
-- When a tagged type is either non-Ghost or checked Ghost and
-- one of its primitives overrides an inherited operation, the
-- the primitive of the tagged type must be ignored Ghost if the
- -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
+ -- overridden operation is ignored Ghost (SPARK RM 6.9(19)).
elsif Is_Ignored_Ghost_Entity (Over_Subp) then
@@ -950,7 +954,7 @@ package body Ghost is
procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
begin
-- The Ghost policy in effect at the point of declaration of a primitive
- -- operation and a tagged type must match (SPARK RM 6.9(16)).
+ -- operation and a tagged type must match (SPARK RM 6.9(18)).
if Is_Tagged_Type (Typ) then
if Is_Checked_Ghost_Entity (Prim)
@@ -1001,7 +1005,7 @@ package body Ghost is
if Is_Ghost_Entity (Constit_Id) then
-- The Ghost policy in effect at the point of abstract state
- -- declaration and constituent must match (SPARK RM 6.9(15)).
+ -- declaration and constituent must match (SPARK RM 6.9(17)).
if Is_Checked_Ghost_Entity (State_Id)
and then Is_Ignored_Ghost_Entity (Constit_Id)
@@ -1062,7 +1066,7 @@ package body Ghost is
Conc_Typ := Typ;
end if;
- -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
+ -- A Ghost type cannot be concurrent (SPARK RM 6.9(21)). Verify this
-- legality rule first to give a finer-grained diagnostic.
if Present (Conc_Typ) then
@@ -1553,7 +1557,7 @@ package body Ghost is
end if;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
Check_Ghost_Completion
(Prev_Id => Spec_Id,
@@ -1600,7 +1604,7 @@ package body Ghost is
end if;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
Check_Ghost_Completion
(Prev_Id => Prev_Id,
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 17f62d3dfb8a..c0bfe873111d 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -11693,7 +11693,7 @@ package body Sem_Ch6 is
Check_Private_Overriding (B_Typ);
-- The Ghost policy in effect at the point of declaration
-- or a tagged type and a primitive operation must match
- -- (SPARK RM 6.9(16)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -11737,7 +11737,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration
-- of a tagged type and a primitive operation must match
- -- (SPARK RM 6.9(16)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -11770,7 +11770,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration of a
-- tagged type and a primitive operation must match
- -- (SPARK RM 6.9(16)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -12226,7 +12226,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration of a
-- parent subprogram and an overriding subprogram must match
- -- (SPARK RM 6.9(17)).
+ -- (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, Overridden_Subp);
end if;
@@ -12389,7 +12389,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
- -- must match (SPARK RM 6.9(17)).
+ -- must match (SPARK RM 6.9(19)).
Check_Ghost_Overriding (E, S);
end if;
@@ -12598,7 +12598,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
- -- must match (SPARK RM 6.9(17)).
+ -- must match (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, E);
@@ -12751,7 +12751,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration of a parent
-- subprogram and an overriding subprogram must match
- -- (SPARK RM 6.9(17)).
+ -- (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, Overridden_Subp);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 3ebee2968bcf..d7acd4604ded 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -12511,7 +12511,7 @@ package body Sem_Prag is
procedure Check_Ghost_Synchronous is
begin
-- A synchronized abstract state cannot be Ghost and vice
- -- versa (SPARK RM 6.9(19)).
+ -- versa (SPARK RM 6.9(21)).
if Ghost_Seen and Synchronous_Seen then
SPARK_Msg_N ("synchronized state cannot be ghost", State);
@@ -13883,7 +13883,7 @@ package body Sem_Prag is
-- Pragma Assertion_Policy specifying a Ghost policy
-- cannot occur within a Ghost subprogram or package
- -- (SPARK RM 6.9(14)).
+ -- (SPARK RM 6.9(16)).
if Ghost_Mode > None then
Error_Pragma
@@ -17673,7 +17673,7 @@ package body Sem_Prag is
end if;
-- Task unit declared without a definition cannot be subject to
- -- pragma Ghost (SPARK RM 6.9(19)).
+ -- pragma Ghost (SPARK RM 6.9(21)).
elsif Nkind (Stmt) in
N_Single_Task_Declaration | N_Task_Type_Declaration
@@ -17769,7 +17769,7 @@ package body Sem_Prag is
end if;
-- Protected and task types cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
if Nkind (Context) in N_Protected_Body | N_Protected_Definition
then
@@ -17856,7 +17856,7 @@ package body Sem_Prag is
end if;
-- A synchronized object cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
elsif Ekind (Id) = E_Variable then
if Is_Protected_Type (Etype (Id)) then
@@ -29787,7 +29787,7 @@ package body Sem_Prag is
begin
-- The Ghost policy in effect at the point of abstract state
- -- declaration and constituent must match (SPARK RM 6.9(15))
+ -- declaration and constituent must match (SPARK RM 6.9(17))
Check_Ghost_Refinement
(State, State_Id, Constit, Constit_Id);
