[Ada] Prohibit concurrent types in Ghost regions
This patch ensures that single concurrent type declarations are marked as Ghost when they appear within a Ghost region. In addition, the patch verifies that no concurrent type is declared within a Ghost region and issues an error. ------------ -- Source -- ------------ -- types.ads package Types with Ghost is protected Prot_Obj is -- Error end Prot_Obj; protected type Prot_Typ is -- Error end Prot_Typ; task Task_Obj; -- Error task type Task_Typ; -- Error end Types; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c types.ads types.ads:2:14: ghost type "Prot_Obj" cannot be concurrent types.ads:5:19: ghost type "Prot_Typ" cannot be concurrent types.ads:8:09: ghost type "Task_Obj" cannot be concurrent types.ads:10:14: ghost type "Task_Typ" cannot be concurrent 2018-01-11 Hristian Kirtchev <kirtchev@adacore.com> gcc/ada/ * freeze.adb (Freeze_Entity): Ensure that a Ghost type is not concurrent, nor effectively volatile. * ghost.adb (Check_Ghost_Type): New routine. * ghost.ads (Check_Ghost_Type): New routine. * sem_util.adb (Is_Declaration): Reimplemented. The routine can now consider specific subsets of declarations. (Is_Declaration_Other_Than_Renaming): Removed. Its functionality is replicated by Is_Declaration. * sem_util.ads (Is_Declaration): New parameter profile. Update the comment on usage. (Is_Declaration_Other_Than_Renaming): Removed. From-SVN: r256521
This commit is contained in:
Hristian Kirtchev
Pierre-Marie de Rodat
parent
5efc1c00c8
commit
a85dbeec8d
@ -1,3 +1,17 @@
|
||||
2018-01-11 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Entity): Ensure that a Ghost type is not
|
||||
concurrent, nor effectively volatile.
|
||||
* ghost.adb (Check_Ghost_Type): New routine.
|
||||
* ghost.ads (Check_Ghost_Type): New routine.
|
||||
* sem_util.adb (Is_Declaration): Reimplemented. The routine can now
|
||||
consider specific subsets of declarations.
|
||||
(Is_Declaration_Other_Than_Renaming): Removed. Its functionality is
|
||||
replicated by Is_Declaration.
|
||||
* sem_util.ads (Is_Declaration): New parameter profile. Update the
|
||||
comment on usage.
|
||||
(Is_Declaration_Other_Than_Renaming): Removed.
|
||||
|
||||
2018-01-11 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* sem_ch5.adb (Analyze_Assignment): Assignments to variables that act
|
||||
|
||||
@ -5517,6 +5517,11 @@ package body Freeze is
|
||||
-- Case of a type or subtype being frozen
|
||||
|
||||
else
|
||||
-- Verify several SPARK legality rules related to Ghost types now
|
||||
-- that the type is frozen.
|
||||
|
||||
Check_Ghost_Type (E);
|
||||
|
||||
-- We used to check here that a full type must have preelaborable
|
||||
-- initialization if it completes a private type specified with
|
||||
-- pragma Preelaborable_Initialization, but that missed cases where
|
||||
@ -5567,21 +5572,6 @@ package body Freeze is
|
||||
end if;
|
||||
end;
|
||||
|
||||
if Is_Ghost_Entity (E) then
|
||||
|
||||
-- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify
|
||||
-- this legality rule first to five a finer-grained diagnostic.
|
||||
|
||||
if Is_Concurrent_Type (E) then
|
||||
Error_Msg_N ("ghost type & cannot be concurrent", E);
|
||||
|
||||
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
|
||||
|
||||
elsif Is_Effectively_Volatile (E) then
|
||||
Error_Msg_N ("ghost type & cannot be volatile", E);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- Deal with special cases of freezing for subtype
|
||||
|
||||
if E /= Base_Type (E) then
|
||||
|
||||
@ -806,6 +806,42 @@ package body Ghost is
|
||||
end if;
|
||||
end Check_Ghost_Refinement;
|
||||
|
||||
----------------------
|
||||
-- Check_Ghost_Type --
|
||||
----------------------
|
||||
|
||||
procedure Check_Ghost_Type (Typ : Entity_Id) is
|
||||
Conc_Typ : Entity_Id;
|
||||
Full_Typ : Entity_Id;
|
||||
|
||||
begin
|
||||
if Is_Ghost_Entity (Typ) then
|
||||
Conc_Typ := Empty;
|
||||
Full_Typ := Typ;
|
||||
|
||||
if Is_Single_Concurrent_Type (Typ) then
|
||||
Conc_Typ := Anonymous_Object (Typ);
|
||||
Full_Typ := Conc_Typ;
|
||||
|
||||
elsif Is_Concurrent_Type (Typ) then
|
||||
Conc_Typ := Typ;
|
||||
end if;
|
||||
|
||||
-- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
|
||||
-- legality rule first to give a finer-grained diagnostic.
|
||||
|
||||
if Present (Conc_Typ) then
|
||||
Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
|
||||
end if;
|
||||
|
||||
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
|
||||
|
||||
if Is_Effectively_Volatile (Full_Typ) then
|
||||
Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
|
||||
end if;
|
||||
end if;
|
||||
end Check_Ghost_Type;
|
||||
|
||||
------------------
|
||||
-- Ghost_Entity --
|
||||
------------------
|
||||
|
||||
@ -68,6 +68,10 @@ package Ghost is
|
||||
-- Verify that the Ghost policy of constituent Constit_Id is compatible
|
||||
-- with the Ghost policy of abstract state State_I.
|
||||
|
||||
procedure Check_Ghost_Type (Typ : Entity_Id);
|
||||
-- Verify that Ghost type Typ is neither concurrent, nor effectively
|
||||
-- volatile.
|
||||
|
||||
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
|
||||
-- Determine whether type Typ implements at least one Ghost interface
|
||||
|
||||
|
||||
@ -13368,40 +13368,113 @@ package body Sem_Util is
|
||||
-- Is_Declaration --
|
||||
--------------------
|
||||
|
||||
function Is_Declaration (N : Node_Id) return Boolean is
|
||||
begin
|
||||
return
|
||||
Is_Declaration_Other_Than_Renaming (N)
|
||||
or else Is_Renaming_Declaration (N);
|
||||
end Is_Declaration;
|
||||
|
||||
----------------------------------------
|
||||
-- Is_Declaration_Other_Than_Renaming --
|
||||
----------------------------------------
|
||||
|
||||
function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is
|
||||
function Is_Declaration
|
||||
(N : Node_Id;
|
||||
Body_OK : Boolean := True;
|
||||
Concurrent_OK : Boolean := True;
|
||||
Formal_OK : Boolean := True;
|
||||
Generic_OK : Boolean := True;
|
||||
Instantiation_OK : Boolean := True;
|
||||
Renaming_OK : Boolean := True;
|
||||
Stub_OK : Boolean := True;
|
||||
Subprogram_OK : Boolean := True;
|
||||
Type_OK : Boolean := True) return Boolean
|
||||
is
|
||||
begin
|
||||
case Nkind (N) is
|
||||
when N_Abstract_Subprogram_Declaration
|
||||
| N_Exception_Declaration
|
||||
| N_Expression_Function
|
||||
| N_Full_Type_Declaration
|
||||
| N_Generic_Package_Declaration
|
||||
|
||||
-- Body declarations
|
||||
|
||||
when N_Proper_Body =>
|
||||
return Body_OK;
|
||||
|
||||
-- Concurrent type declarations
|
||||
|
||||
when N_Protected_Type_Declaration
|
||||
| N_Single_Protected_Declaration
|
||||
| N_Single_Task_Declaration
|
||||
| N_Task_Type_Declaration
|
||||
=>
|
||||
return Concurrent_OK or Type_OK;
|
||||
|
||||
-- Formal declarations
|
||||
|
||||
when N_Formal_Abstract_Subprogram_Declaration
|
||||
| N_Formal_Concrete_Subprogram_Declaration
|
||||
| N_Formal_Object_Declaration
|
||||
| N_Formal_Package_Declaration
|
||||
| N_Formal_Type_Declaration
|
||||
=>
|
||||
return Formal_OK;
|
||||
|
||||
-- Generic declarations
|
||||
|
||||
when N_Generic_Package_Declaration
|
||||
| N_Generic_Subprogram_Declaration
|
||||
=>
|
||||
return Generic_OK;
|
||||
|
||||
-- Generic instantiations
|
||||
|
||||
when N_Function_Instantiation
|
||||
| N_Package_Instantiation
|
||||
| N_Procedure_Instantiation
|
||||
=>
|
||||
return Instantiation_OK;
|
||||
|
||||
-- Generic renaming declarations
|
||||
|
||||
when N_Generic_Renaming_Declaration =>
|
||||
return Generic_OK or Renaming_OK;
|
||||
|
||||
-- Renaming declarations
|
||||
|
||||
when N_Exception_Renaming_Declaration
|
||||
| N_Object_Renaming_Declaration
|
||||
| N_Package_Renaming_Declaration
|
||||
| N_Subprogram_Renaming_Declaration
|
||||
=>
|
||||
return Renaming_OK;
|
||||
|
||||
-- Stub declarations
|
||||
|
||||
when N_Body_Stub =>
|
||||
return Stub_OK;
|
||||
|
||||
-- Subprogram declarations
|
||||
|
||||
when N_Abstract_Subprogram_Declaration
|
||||
| N_Entry_Declaration
|
||||
| N_Expression_Function
|
||||
| N_Subprogram_Declaration
|
||||
=>
|
||||
return Subprogram_OK;
|
||||
|
||||
-- Type declarations
|
||||
|
||||
when N_Full_Type_Declaration
|
||||
| N_Incomplete_Type_Declaration
|
||||
| N_Private_Extension_Declaration
|
||||
| N_Private_Type_Declaration
|
||||
| N_Subtype_Declaration
|
||||
=>
|
||||
return Type_OK;
|
||||
|
||||
-- Miscellaneous
|
||||
|
||||
when N_Component_Declaration
|
||||
| N_Exception_Declaration
|
||||
| N_Implicit_Label_Declaration
|
||||
| N_Number_Declaration
|
||||
| N_Object_Declaration
|
||||
| N_Package_Declaration
|
||||
| N_Private_Extension_Declaration
|
||||
| N_Private_Type_Declaration
|
||||
| N_Subprogram_Declaration
|
||||
| N_Subtype_Declaration
|
||||
=>
|
||||
return True;
|
||||
|
||||
when others =>
|
||||
return False;
|
||||
end case;
|
||||
end Is_Declaration_Other_Than_Renaming;
|
||||
end Is_Declaration;
|
||||
|
||||
--------------------------------
|
||||
-- Is_Declared_Within_Variant --
|
||||
|
||||
@ -1561,11 +1561,39 @@ package Sem_Util is
|
||||
-- declarations. In Ada 2012 it also covers type and subtype declarations
|
||||
-- with aspects: Invariant, Predicate, and Default_Initial_Condition.
|
||||
|
||||
function Is_Declaration (N : Node_Id) return Boolean;
|
||||
-- Determine whether arbitrary node N denotes a declaration
|
||||
|
||||
function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean;
|
||||
-- Determine whether arbitrary node N denotes a non-renaming declaration
|
||||
function Is_Declaration
|
||||
(N : Node_Id;
|
||||
Body_OK : Boolean := True;
|
||||
Concurrent_OK : Boolean := True;
|
||||
Formal_OK : Boolean := True;
|
||||
Generic_OK : Boolean := True;
|
||||
Instantiation_OK : Boolean := True;
|
||||
Renaming_OK : Boolean := True;
|
||||
Stub_OK : Boolean := True;
|
||||
Subprogram_OK : Boolean := True;
|
||||
Type_OK : Boolean := True) return Boolean;
|
||||
-- Determine whether arbitrary node N denotes a declaration depending
|
||||
-- on the allowed subsets of declarations. Set the following flags to
|
||||
-- consider specific subsets of declarations:
|
||||
--
|
||||
-- * Body_OK - body declarations
|
||||
--
|
||||
-- * Concurrent_OK - concurrent type declarations
|
||||
--
|
||||
-- * Formal_OK - formal declarations
|
||||
--
|
||||
-- * Generic_OK - generic declarations, including generic renamings
|
||||
--
|
||||
-- * Instantiation_OK - generic instantiations
|
||||
--
|
||||
-- * Renaming_OK - renaming declarations, including generic renamings
|
||||
--
|
||||
-- * Stub_OK - stub declarations
|
||||
--
|
||||
-- * Subprogram_OK - entry, expression function, and subprogram
|
||||
-- declarations.
|
||||
--
|
||||
-- * Type_OK - type declarations, including concurrent types
|
||||
|
||||
function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean;
|
||||
-- Returns True iff component Comp is declared within a variant part
|
||||
|
||||
Loading…
Reference in New Issue
Block a user