===================================================================
@@ -10068,6 +10068,11 @@
-- 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 @@
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 @@
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 @@
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)).
===================================================================
@@ -2806,6 +2806,15 @@
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 @@
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 @@
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
===================================================================
@@ -20121,7 +20121,8 @@
--------------------------------
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,11 +20155,16 @@
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)))
then
@@ -20181,7 +20187,7 @@
-- 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
===================================================================
@@ -648,10 +648,34 @@
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 @@
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 @@
& "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;
-----------------------------------
This patch implements the following SPARK RM 6.9(19) rule: A ghost type shall not have a task or protected part. A ghost object shall not be of a type which yields synchronized objects. A ghost object shall not have a volatile part. A synchronized state abstraction shall not be a ghost state abstraction. ------------ -- Source -- ------------ -- yso.ads -- Yields synchronized object with Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control; package YSO with SPARK_Mode is -- Protected interface type Prot_Iface is protected interface; -- Protected type protected type Prot_Typ is entry Ent; end Prot_Typ; -- Synchronized interface type Sync_Iface is synchronized interface; -- Task interface type Task_Iface is task interface; -- Task type task type Task_Typ; -- Array type type Arr_Typ is array (1 .. 5) of Prot_Typ; -- Descendant of Suspension_Object type Sus_Obj is new Suspension_Object; -- Record type type Rec_Typ is record Comp_1 : Prot_Typ; Comp_2 : Task_Typ; Comp_3 : Arr_Typ; Comp_4 : Sus_Obj; Comp_5 : Suspension_Object; end record with Volatile; -- Type extension type Deriv_Typ is new Rec_Typ; end YSO; -- lr19.ads th Ada.Synchronous_Task_Control; use Ada.Synchronous_Task_Control; with YSO; use YSO; package LR19 with SPARK_Mode, -- A synchronized state abstraction shall not be a ghost state -- abstraction. Abstract_State => ((Error_1 with Ghost, Synchronous), -- Error (Error_2 with Synchronous, Ghost)) -- Error is -- A ghost type shall not have a task or protected type protected type Prot_Typ is end Prot_Typ; task type Task_Typ; protected type Error_3 with Ghost is end Error_3; -- Error protected Error_4 with Ghost is end Error_4; -- Error task type Error_5 with Ghost; -- Error task Error_6 with Ghost; -- Error type Error_7 is record Comp : Prot_Typ; -- Error end record with Ghost, Volatile; type Error_8 is array (1 .. 3) of Task_Typ with Ghost; -- Error -- A ghost object shall not be of a type which yields a synchonized object Error_9 : Prot_Typ with Ghost; -- Error Error_10 : Task_Typ with Ghost; -- Error Error_11 : Arr_Typ with Ghost; -- Error Error_12 : Sus_Obj with Ghost; -- Error Error_13 : Suspension_Object with Ghost; -- Error Error_14 : Rec_Typ with Ghost; -- Error Error_15 : Deriv_Typ with Ghost; -- Error -- A ghost object shall not have a [n effectively?] volatile part type Vol_Int is new Integer range 1 .. 5 with Volatile; type Vol_Rec is record Comp : Vol_Int; end record with Volatile; Error_16 : Integer with Ghost, Volatile; -- Error Error_17 : Vol_Int with Ghost; -- Error Error_18 : Vol_Rec with Ghost; -- Error end LR19; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c lr19.ads lr19.ads:10:27: synchronized state cannot be ghost lr19.ads:11:27: synchronized state cannot be ghost lr19.ads:18:32: aspect "GHOST" cannot apply to a protected type lr19.ads:19:27: aspect "GHOST" cannot apply to a protected type lr19.ads:20:27: aspect "GHOST" cannot apply to a task type lr19.ads:21:22: aspect "GHOST" cannot apply to a task type lr19.ads:23:09: ghost type "Error_7" cannot be volatile lr19.ads:24:07: component "Comp" of ghost type "ERROR_7" cannot be concurrent lr19.ads:27:04: ghost array type "ERROR_8" cannot have concurrent component type lr19.ads:31:04: ghost object "Error_9" cannot be synchronized lr19.ads:31:29: aspect "GHOST" cannot apply to a protected object lr19.ads:32:04: ghost object "Error_10" cannot be synchronized lr19.ads:32:29: aspect "GHOST" cannot apply to a task object lr19.ads:33:04: ghost object "Error_11" cannot be synchronized lr19.ads:34:04: ghost object "Error_12" cannot be synchronized lr19.ads:35:04: ghost object "Error_13" cannot be synchronized lr19.ads:36:04: ghost object "Error_14" cannot be synchronized lr19.ads:37:04: ghost object "Error_15" cannot be synchronized lr19.ads:47:04: ghost object "Error_16" cannot be volatile lr19.ads:48:04: ghost object "Error_17" cannot be volatile lr19.ads:49:04: ghost object "Error_18" cannot be volatile Tested on x86_64-pc-linux-gnu, committed on trunk 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.