This patch decouples the semantic and legality rules of Ghost entities from the
presence of aspect/pragma SPARK_Mode. This way non-SPARK code can utilize Ghost
annotations.
------------
-- Source --
------------
-- ghost_decl.ads
package Ghost_Decl is
X : Integer := 0 with Ghost;
Y : Integer := X;
end Ghost_Decl;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c ghost_decl.ads
ghost_decl.ads:3:19: ghost entity cannot appear in this context (SPARK RM
6.9(12))
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-11-07 Hristian Kirtchev <kirtc...@adacore.com>
* freeze.adb (Freeze_Entity): Issue an error regardless of the
SPARK_Mode when a ghost type is effectively volatile.
* sem_ch3.adb (Analyze_Object_Contract): Decouple the checks
related to Ghost from SPARK_Mode.
* sem_res.adb (Check_Ghost_Policy): Issue an error regardless
of the SPARK_Mode when the Ghost policies do not match.
* sem_util.adb (Check_Ghost_Completion): Issue an error regardless
of the SPARK_Mode when the Ghost policies do not match.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 217215)
+++ sem_ch3.adb (working copy)
@@ -3185,24 +3185,22 @@
Obj_Id);
end if;
end if;
+ end if;
- if Is_Ghost_Entity (Obj_Id) then
+ if Is_Ghost_Entity (Obj_Id) then
- -- A Ghost object cannot be effectively volatile
- -- (SPARK RM 6.9(8)).
+ -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
- if Is_Effectively_Volatile (Obj_Id) then
- SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+ 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)).
+ -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
- elsif Is_Imported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ elsif Is_Imported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
- elsif Is_Exported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
- end if;
+ elsif Is_Exported (Obj_Id) then
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
end if;
end if;
@@ -3256,10 +3254,10 @@
if Is_Ghost_Entity (Obj_Id) then
if Is_Exported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id);
+ Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
elsif Is_Imported (Obj_Id) then
- SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id);
+ Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
end if;
end if;
end Analyze_Object_Contract;
@@ -4788,8 +4786,6 @@
when Class_Wide_Kind =>
Set_Ekind (Id, E_Class_Wide_Subtype);
- Set_First_Entity (Id, First_Entity (T));
- Set_Last_Entity (Id, Last_Entity (T));
Set_Class_Wide_Type (Id, Class_Wide_Type (T));
Set_Cloned_Subtype (Id, T);
Set_Is_Tagged_Type (Id, True);
Index: freeze.adb
===================================================================
--- freeze.adb (revision 217223)
+++ freeze.adb (working copy)
@@ -2398,6 +2398,24 @@
Set_Has_Non_Standard_Rep (Base_Type (Arr), True);
Set_Is_Bit_Packed_Array (Base_Type (Arr), True);
Set_Is_Packed (Base_Type (Arr), True);
+
+ -- Make sure that we have the necessary routines to
+ -- implement the packing, and complain now if not.
+
+ declare
+ CS : constant Int := UI_To_Int (Csiz);
+ RE : constant RE_Id := Get_Id (CS);
+
+ begin
+ if RE /= RE_Null
+ and then not RTE_Available (RE)
+ then
+ Error_Msg_CRT
+ ("packing of " & UI_Image (Csiz)
+ & "-bit components",
+ First_Subtype (Etype (Arr)));
+ end if;
+ end;
end if;
end;
end if;
@@ -2650,37 +2668,6 @@
Create_Packed_Array_Impl_Type (Arr);
Freeze_And_Append (Packed_Array_Impl_Type (Arr), N, Result);
- -- Make sure that we have the necessary routines to implement the
- -- packing, and complain now if not. Note that we only test this
- -- for constrained array types.
-
- if Is_Constrained (Arr)
- and then Is_Bit_Packed_Array (Arr)
- and then Present (Packed_Array_Impl_Type (Arr))
- and then Is_Array_Type (Packed_Array_Impl_Type (Arr))
- then
- declare
- CS : constant Uint := Component_Size (Arr);
- RE : constant RE_Id := Get_Id (UI_To_Int (CS));
-
- begin
- if RE /= RE_Null
- and then not RTE_Available (RE)
- then
- Error_Msg_CRT
- ("packing of " & UI_Image (CS) & "-bit components",
- First_Subtype (Etype (Arr)));
-
- -- Cancel the packing
-
- Set_Is_Packed (Base_Type (Arr), False);
- Set_Is_Bit_Packed_Array (Base_Type (Arr), False);
- Set_Packed_Array_Impl_Type (Arr, Empty);
- goto Skip_Packed;
- end if;
- end;
- end if;
-
-- Size information of packed array type is copied to the array
-- type, since this is really the representation. But do not
-- override explicit existing size values. If the ancestor subtype
@@ -2702,8 +2689,6 @@
end if;
end if;
- <<Skip_Packed>>
-
-- For non-packed arrays set the alignment of the array to the
-- alignment of the component type if it is unknown. Skip this
-- in atomic case (atomic arrays may need larger alignments).
@@ -4835,7 +4820,7 @@
if Is_Ghost_Entity (E)
and then Is_Effectively_Volatile (E)
then
- SPARK_Msg_N ("ghost type & cannot be volatile", E);
+ Error_Msg_N ("ghost type & cannot be volatile", E);
end if;
-- Deal with special cases of freezing for subtype
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 217215)
+++ sem_util.adb (working copy)
@@ -2688,18 +2688,18 @@
then
Error_Msg_Sloc := Sloc (Full_View);
- SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
- SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View);
- SPARK_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy Check", Partial_View);
+ Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View);
elsif Is_Ignored_Ghost_Entity (Partial_View)
and then Policy = Name_Check
then
Error_Msg_Sloc := Sloc (Full_View);
- SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View);
- SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
- SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View);
+ Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
+ Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View);
+ Error_Msg_N ("\& completed # with ghost policy Check", Partial_View);
end if;
end Check_Ghost_Completion;
@@ -2722,8 +2722,8 @@
-- The parent type of a Ghost type extension must be Ghost
elsif not Is_Ghost_Entity (Parent_Typ) then
- SPARK_Msg_N ("type extension & cannot be ghost", Typ);
- SPARK_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
return;
end if;
@@ -2735,8 +2735,8 @@
Iface := Node (Iface_Elmt);
if not Is_Ghost_Entity (Iface) then
- SPARK_Msg_N ("type extension & cannot be ghost", Typ);
- SPARK_Msg_NE ("\interface type & is not ghost", Typ, Iface);
+ Error_Msg_N ("type extension & cannot be ghost", Typ);
+ Error_Msg_NE ("\interface type & is not ghost", Typ, Iface);
return;
end if;
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 217215)
+++ sem_res.adb (working copy)
@@ -846,16 +846,16 @@
if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
Error_Msg_Sloc := Sloc (Err_N);
- SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
- SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
- SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id);
elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
Error_Msg_Sloc := Sloc (Err_N);
- SPARK_Msg_N ("incompatible ghost policies in effect", Err_N);
- SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
- SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
+ Error_Msg_N ("incompatible ghost policies in effect", Err_N);
+ Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id);
+ Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id);
end if;
end Check_Ghost_Policy;
@@ -873,7 +873,7 @@
-- its behavior or value.
else
- SPARK_Msg_N
+ Error_Msg_N
("ghost entity cannot appear in this context (SPARK RM 6.9(12))",
Ghost_Ref);
end if;
@@ -7089,12 +7089,13 @@
("volatile object cannot appear in this context "
& "(SPARK RM 7.1.3(13))", N);
end if;
+ end if;
+ end if;
- -- A Ghost entity must appear in a specific context
+ -- A Ghost entity must appear in a specific context
- elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then
- Check_Ghost_Context (E, N);
- end if;
+ if Is_Ghost_Entity (E) and then Comes_From_Source (N) then
+ Check_Ghost_Context (E, N);
end if;
end Resolve_Entity_Name;
