procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

contracts.adb (Analyze_Object_Contract): Set and restore the SPARK_Mode for both constants and objects.

Browse source 
2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Object_Contract): Set and restore
	the SPARK_Mode for both constants and objects. Factor out the
	semantic checks concerning Ghost objects.
	* freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a
	concurrent component type.
	(Freeze_Entity): A Ghost type cannot also be concurrent.
	(Freeze_Record_Type): A Ghost record type cannot have a concurrent
	component.
	* sem_prag.adb (Analyze_Abstract_State): A Ghost abstract
	state cannot also be synchronized.
	(Check_Ghost_Synchronous): New routine.
	* sem_util.adb (Yields_Synchronized_Object): Correct the case
	of record components to account for the case where the type has
	no component list.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* expander.adb (Expand): Expand a single protected declaration.
	* exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New
	routine.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear
	in an object declaration as long as it denotes the name.

From-SVN: r229376
This commit is contained in:
Hristian Kirtchev 2015-10-26 15:40:10 +00:00 • committed by Arnaud Charlet
parent c67e519463
commit 58996b09ca
9 changed files with 188 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
gcc/ada/ChangeLog
View file

@ -1,3 +1,31 @@
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Object_Contract): Set and restore
the SPARK_Mode for both constants and objects. Factor out the
semantic checks concerning Ghost objects.
* freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a
concurrent component type.
(Freeze_Entity): A Ghost type cannot also be concurrent.
(Freeze_Record_Type): A Ghost record type cannot have a concurrent
component.
* sem_prag.adb (Analyze_Abstract_State): A Ghost abstract
state cannot also be synchronized.
(Check_Ghost_Synchronous): New routine.
* sem_util.adb (Yields_Synchronized_Object): Correct the case
of record components to account for the case where the type has
no component list.
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* expander.adb (Expand): Expand a single protected declaration.
* exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New
routine.
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear
in an object declaration as long as it denotes the name.
2015-10-26 Hristian Kirtchev <kirtchev@adacore.com>
* sem_ch9.adb (Analyze_Single_Protected_Declaration): The anonymous

100
gcc/ada/contracts.adb
View file

@ -648,10 +648,34 @@ package body Contracts is
end if;
end if;
-- The anonymous object created for a single concurrent type inherits
-- the SPARK_Mode from the type. Due to the timing of contract analysis,
-- delayed pragmas may be subject to the wrong SPARK_Mode, usually that
-- of the enclosing context. To remedy this, restore the original mode
-- of the related anonymous object.
if Is_Single_Concurrent_Object (Obj_Id)
and then Present (SPARK_Pragma (Obj_Id))
then
Restore_Mode := True;
Save_SPARK_Mode_And_Set (Obj_Id, Mode);
end if;
-- Constant-related checks
if Ekind (Obj_Id) = E_Constant then
-- Analyze indicator Part_Of
Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-- Check whether the lack of indicator Part_Of agrees with the
-- placement of the constant with respect to the state space.
if No (Prag) then
Check_Missing_Part_Of (Obj_Id);
end if;
-- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
-- This check is relevant only when SPARK_Mode is on, as it is not
-- a standard Ada legality rule. Internally-generated constants that
@ -666,32 +690,10 @@ package body Contracts is
Error_Msg_N ("constant cannot be volatile", Obj_Id);
end if;
Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-- Check whether the lack of indicator Part_Of agrees with the
-- placement of the constant with respect to the state space.
if No (Prag) then
Check_Missing_Part_Of (Obj_Id);
end if;
-- Variable-related checks
else pragma Assert (Ekind (Obj_Id) = E_Variable);
-- The anonymous object created for a single concurrent type inherits
-- the SPARK_Mode from the type. Due to the timing of contract
-- analysis, delayed pragmas may be subject to the wrong SPARK_Mode,
-- usually that of the enclosing context. To remedy this, restore the
-- original SPARK_Mode of the related variable.
if Is_Single_Concurrent_Object (Obj_Id)
and then Present (SPARK_Pragma (Obj_Id))
then
Restore_Mode := True;
Save_SPARK_Mode_And_Set (Obj_Id, Mode);
end if;
-- Analyze all external properties
Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
@ -834,44 +836,42 @@ package body Contracts is
& "protected type %"), Obj_Id);
end if;
end if;
if Is_Ghost_Entity (Obj_Id) then
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
if Is_Effectively_Volatile (Obj_Id) then
Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
-- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
elsif Is_Imported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
elsif Is_Exported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
end if;
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
if Restore_Mode then
Restore_SPARK_Mode (Mode);
end if;
end if;
-- A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
-- exception to this is the object that represents the dispatch table of
-- a Ghost tagged type, as the symbol needs to be exported.
-- Common checks
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
-- A Ghost object cannot be of a type that yields a synchronized
-- object (SPARK RM 6.9(19)).
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
-- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
-- SPARK RM 6.9(19)).
elsif Is_Effectively_Volatile (Obj_Id) then
Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
-- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)).
-- One exception to this is the object that represents the dispatch
-- table of a Ghost tagged type, as the symbol needs to be exported.
elsif Is_Exported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
elsif Is_Imported (Obj_Id) then
Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
end if;
end if;
-- Restore the SPARK_Mode of the enclosing context after all delayed
-- pragmas have been analyzed.
if Restore_Mode then
Restore_SPARK_Mode (Mode);
end if;
end Analyze_Object_Contract;
-----------------------------------

22
gcc/ada/exp_ch9.adb
View file

@ -11388,14 +11388,28 @@ package body Exp_Ch9 is
end loop;
end Expand_N_Selective_Accept;
-------------------------------------------
-- Expand_N_Single_Protected_Declaration --
-------------------------------------------
-- A single protected declaration should never be present after semantic
-- analysis because it is transformed into a protected type declaration
-- and an accompanying anonymous object. This routine ensures that the
-- transformation takes place.
procedure Expand_N_Single_Protected_Declaration (N : Node_Id) is
begin
raise Program_Error;
end Expand_N_Single_Protected_Declaration;
--------------------------------------
-- Expand_N_Single_Task_Declaration --
--------------------------------------
-- Single task declarations should never be present after semantic
-- analysis, since we expect them to be replaced by a declaration of an
-- anonymous task type, followed by a declaration of the task object. We
-- include this routine to make sure that is happening.
-- A single task declaration should never be present after semantic
-- analysis because it is transformed into a task type declaration and
-- an accompanying anonymous object. This routine ensures that the
-- transformation takes place.
procedure Expand_N_Single_Task_Declaration (N : Node_Id) is
begin

15
gcc/ada/exp_ch9.ads
View file

@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
-- Copyright (C) 1992-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- --
@ -266,12 +266,13 @@ package Exp_Ch9 is
-- allows these two nodes to be found from the type, without benefit of
-- further attributes, using Corresponding_Record.
procedure Expand_N_Requeue_Statement (N : Node_Id);
procedure Expand_N_Selective_Accept (N : Node_Id);
procedure Expand_N_Single_Task_Declaration (N : Node_Id);
procedure Expand_N_Task_Body (N : Node_Id);
procedure Expand_N_Task_Type_Declaration (N : Node_Id);
procedure Expand_N_Timed_Entry_Call (N : Node_Id);
procedure Expand_N_Requeue_Statement (N : Node_Id);
procedure Expand_N_Selective_Accept (N : Node_Id);
procedure Expand_N_Single_Protected_Declaration (N : Node_Id);
procedure Expand_N_Single_Task_Declaration (N : Node_Id);
procedure Expand_N_Task_Body (N : Node_Id);
procedure Expand_N_Task_Type_Declaration (N : Node_Id);
procedure Expand_N_Timed_Entry_Call (N : Node_Id);
procedure Expand_Protected_Body_Declarations
(N : Node_Id;

5
gcc/ada/expander.adb
View file

@ -432,6 +432,9 @@ package body Expander is
when N_Selective_Accept =>
Expand_N_Selective_Accept (N);
when N_Single_Protected_Declaration =>
Expand_N_Single_Protected_Declaration (N);
when N_Single_Task_Declaration =>
Expand_N_Single_Task_Declaration (N);
@ -471,7 +474,7 @@ package body Expander is
when N_Variant_Part =>
Expand_N_Variant_Part (N);
-- For all other node kinds, no expansion activity required
-- For all other node kinds, no expansion activity required
when others =>
null;

45
gcc/ada/freeze.adb
View file

@ -2806,6 +2806,15 @@ package body Freeze is
then
Set_Alignment (Arr, Alignment (Component_Type (Arr)));
end if;
-- A Ghost type cannot have a component of protected or task type
-- (SPARK RM 6.9(19)).
if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
Error_Msg_N
("ghost array type & cannot have concurrent component type",
Arr);
end if;
end Freeze_Array_Type;
-------------------------------
@ -4341,6 +4350,25 @@ package body Freeze is
Next_Component (Comp);
end loop;
end if;
-- A Ghost type cannot have a component of protected or task type
-- (SPARK RM 6.9(19)).
if Is_Ghost_Entity (Rec) then
Comp := First_Component (Rec);
while Present (Comp) loop
if Comes_From_Source (Comp)
and then Is_Concurrent_Type (Etype (Comp))
then
Error_Msg_Name_1 := Chars (Rec);
Error_Msg_N
("component & of ghost type % cannot be concurrent",
Comp);
end if;
Next_Component (Comp);
end loop;
end if;
end if;
-- Make sure that if we have an iterator aspect, then we have
@ -5091,12 +5119,19 @@ package body Freeze is
end if;
end;
-- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
if Is_Ghost_Entity (E) then
if Is_Ghost_Entity (E)
and then Is_Effectively_Volatile (E)
then
Error_Msg_N ("ghost type & cannot be volatile", E);
-- 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(8))
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

21
gcc/ada/sem_prag.adb
View file

@ -10068,6 +10068,11 @@ package body Sem_Prag is
-- Opt is not a duplicate property and sets the flag Status.
-- (SPARK RM 7.1.4(2))
procedure Check_Ghost_Synchronous;
-- Ensure that the abstract state is not subject to both Ghost
-- and Synchronous simple options. Emit an error if this is the
-- case.
procedure Create_Abstract_State
(Nam : Name_Id;
Decl : Node_Id;
@ -10320,6 +10325,20 @@ package body Sem_Prag is
Status := True;
end Check_Duplicate_Property;
-----------------------------
-- Check_Ghost_Synchronous --
-----------------------------
procedure Check_Ghost_Synchronous is
begin
-- A synchronized abstract state cannot be Ghost and vice
-- versa (SPARK RM 6.9(19)).
if Ghost_Seen and Synchronous_Seen then
SPARK_Msg_N ("synchronized state cannot be ghost", State);
end if;
end Check_Ghost_Synchronous;
---------------------------
-- Create_Abstract_State --
---------------------------
@ -10464,6 +10483,7 @@ package body Sem_Prag is
elsif Chars (Opt) = Name_Ghost then
Check_Duplicate_Option (Opt, Ghost_Seen);
Check_Ghost_Synchronous;
if Present (State_Id) then
Set_Is_Ghost_Entity (State_Id);
@ -10473,6 +10493,7 @@ package body Sem_Prag is
elsif Chars (Opt) = Name_Synchronous then
Check_Duplicate_Option (Opt, Synchronous_Seen);
Check_Ghost_Synchronous;
-- Option Part_Of without an encapsulating state is
-- illegal (SPARK RM 7.1.4(9)).

7
gcc/ada/sem_res.adb
View file

@ -6993,6 +6993,13 @@ package body Sem_Res is
return True;
end if;
-- The volatile object acts as the name of a renaming declaration
elsif Nkind (Context) = N_Object_Renaming_Declaration
and then Name (Context) = Obj_Ref
then
return True;
-- The volatile object appears as an actual parameter in a call to an
-- instance of Unchecked_Conversion whose result is renamed.

18
gcc/ada/sem_util.adb
View file

@ -20121,7 +20121,8 @@ package body Sem_Util is
--------------------------------
function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is
Id : Entity_Id;
Has_Sync_Comp : Boolean := False;
Id : Entity_Id;
begin
-- An array type yields a synchronized object if its component type
@ -20154,10 +20155,15 @@ package body Sem_Util is
Id := First_Entity (Typ);
while Present (Id) loop
if Comes_From_Source (Id) then
if Ekind (Id) = E_Component
and then not Yields_Synchronized_Object (Etype (Id))
then
return False;
if Ekind (Id) = E_Component then
if Yields_Synchronized_Object (Etype (Id)) then
Has_Sync_Comp := True;
-- The component does not yield a synchronized object
else
return False;
end if;
elsif Ekind (Id) = E_Discriminant
and then Present (Expression (Parent (Id)))
@ -20181,7 +20187,7 @@ package body Sem_Util is
-- If we get here, then all discriminants lack default values and all
-- components are of a type that yields a synchronized object.
return True;
return Has_Sync_Comp;
-- A synchronized interface type yields a synchronized object by default