+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
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
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);
& "protected type %"), Obj_Id);
end if;
end if;
+ end if;
- if Is_Ghost_Entity (Obj_Id) then
+ -- Common checks
- -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
+ if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
- if Is_Effectively_Volatile (Obj_Id) then
- Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+ -- A Ghost object cannot be of a type that yields a synchronized
+ -- object (SPARK RM 6.9(19)).
- -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
+ if Yields_Synchronized_Object (Obj_Typ) then
+ Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
- elsif Is_Imported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
+ -- SPARK RM 6.9(19)).
- elsif Is_Exported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
- end if;
- end if;
+ elsif Is_Effectively_Volatile (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
+ -- 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.
- 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.
-
- if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
- if Is_Exported (Obj_Id) then
+ 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;
-----------------------------------
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
-- --
-- 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- --
-- 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;
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);
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;
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;
-------------------------------
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
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
-- 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;
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 --
---------------------------
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);
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)).
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.
--------------------------------
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
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)))
-- 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
projects / gcc.git / commitdiff