diff mbox

[Ada] Ghost legality rules and SPARK_Mode

Message ID 20141107134844.GA6556@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 7, 2014, 1:48 p.m. UTC 
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  <kirtchev@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.
diff mbox

Patch

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;