[Ada] Work on pragma SPARK_Mode

Arnaud Charlet charlet@adacore.com
Tue Jan 21 12:03:00 GMT 2014


This patch redoes the data structures for pragma SPARK_Mode so
that the tree captures full information on the SPARK_Mode setting
in all cases, so that it can easily be accessed by gnat2why.

It also fully implements the error checking on "monotonicity" of
SPARK_Mode settings, and also properly checks for duplicate pragmas
in a configuration pragma file.

The following program:

     1. package body PSMode is
     2.    pragma SPARK_Mode (On);
     3.    procedure q is begin null; end;
     4. begin
     5.    pragma SPARK_Mode (Off);
     6.    Z := 2;
     7. end PSMode;

     1. package PSMode is
     2.    pragma SPARK_Mode (On);
     3.    X : Integer := 12;
     4.    Y : Integer := 2 ** X;
     5.    procedure q;
     6. private
     7.    pragma SPARK_Mode (Off);
     8.    Z : Integer;
     9. end PSMode;

compiled with a gnat.adc file that looks like:

     1. pragma SPARK_Mode (On);
     2. pragma SPARK_Mode (On);

gets the following errors compiled with -gnatj60

psmode.adb:2:23: cannot define SPARK mode "on", mode is
                 less restrictive than mode "off" defined
                 at psmode.ads:7
gnat.adc:2:01: pragma "Spark_Mode" duplicates pragma
               declared at line 1

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-01-21  Robert Dewar  <dewar@adacore.com>

	* atree.ads, atree.adb: Add Node33 and Set_Node33.
	* einfo.ads, einfo.adb (SPARK_Pragma): New field (SPARK_Aux_Pragma):
	New field (SPARK_Pragma_Inherited): New flag
	(SPARK_Aux_Pragma_Inherited): New flag (SPARK_Mode_Pragmas):
	Removed.
	* lib.ads, lib.adb: Remove SPARK_Mode_Pragma, no longer used.
	* opt.ads (SPARK_Mode_Pragma): New global variable.
	* sem.ads: Add Save_SPARK_Mode_Pragma field to Scope_Stack_Entry.
	* sem_ch3.adb: Use new SPARK_Mode data structures.
	* sem_ch6.adb: Set SPARK_Mode fields in subprogram specs and bodies.
	* sem_ch7.adb: Set SPARK_Mode fields in package spec and body entities.
	* sem_ch8.adb (Push_Scope): Save SPARK_Mode_Pragma.
	(Pop_Scope): Restore SPARK_Mode_Pragma.
	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Rewrite for
	new data structures.

-------------- next part --------------
Index: atree.adb
===================================================================
--- atree.adb	(revision 206872)
+++ atree.adb	(working copy)
@@ -2595,6 +2595,12 @@
          return Node_Id (Nodes.Table (N + 5).Field8);
       end Node32;
 
+      function Node33 (N : Node_Id) return Node_Id is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         return Node_Id (Nodes.Table (N + 5).Field9);
+      end Node33;
+
       function List1 (N : Node_Id) return List_Id is
       begin
          pragma Assert (N <= Nodes.Last);
@@ -5336,6 +5342,12 @@
          Nodes.Table (N + 5).Field8 := Union_Id (Val);
       end Set_Node32;
 
+      procedure Set_Node33 (N : Node_Id; Val : Node_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 5).Field9 := Union_Id (Val);
+      end Set_Node33;
+
       procedure Set_List1 (N : Node_Id; Val : List_Id) is
       begin
          pragma Assert (N <= Nodes.Last);
Index: atree.ads
===================================================================
--- atree.ads	(revision 206872)
+++ atree.ads	(working copy)
@@ -1209,6 +1209,9 @@
       function Node32 (N : Node_Id) return Node_Id;
       pragma Inline (Node32);
 
+      function Node33 (N : Node_Id) return Node_Id;
+      pragma Inline (Node33);
+
       function List1 (N : Node_Id) return List_Id;
       pragma Inline (List1);
 
@@ -2509,6 +2512,9 @@
       procedure Set_Node32 (N : Node_Id; Val : Node_Id);
       pragma Inline (Set_Node32);
 
+      procedure Set_Node33 (N : Node_Id; Val : Node_Id);
+      pragma Inline (Set_Node33);
+
       procedure Set_List1 (N : Node_Id; Val : List_Id);
       pragma Inline (Set_List1);
 
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 206832)
+++ einfo.adb	(working copy)
@@ -248,9 +248,9 @@
 
    --    Thunk_Entity                    Node31
 
-   --    SPARK_Mode_Pragmas              Node32
+   --    SPARK_Pragma                    Node32
 
-   --    (unused)                        Node33
+   --    SPARK_Aux_Pragma                Node33
 
    --    (unused)                        Node34
 
@@ -554,9 +554,9 @@
    --    May_Inherit_Delayed_Rep_Aspects Flag262
    --    Has_Visible_Refinement          Flag263
    --    Has_Body_References             Flag264
+   --    SPARK_Pragma_Inherited          Flag265
+   --    SPARK_Aux_Pragma_Inherited      Flag266
 
-   --    (unused)                        Flag265
-   --    (unused)                        Flag266
    --    (unused)                        Flag267
    --    (unused)                        Flag268
    --    (unused)                        Flag269
@@ -2835,9 +2835,27 @@
       return Ureal21 (Id);
    end Small_Value;
 
-   function SPARK_Mode_Pragmas (Id : E) return N is
+   function SPARK_Aux_Pragma (Id : E) return N is
    begin
       pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Node33 (Id);
+   end SPARK_Aux_Pragma;
+
+   function SPARK_Aux_Pragma_Inherited (Id : E) return B is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Flag266 (Id);
+   end SPARK_Aux_Pragma_Inherited;
+
+   function SPARK_Pragma (Id : E) return N is
+   begin
+      pragma Assert
         (Ekind_In (Id, E_Function,         --  subprogram variants
                        E_Generic_Function,
                        E_Generic_Procedure,
@@ -2848,8 +2866,23 @@
                        E_Package,
                        E_Package_Body));
       return Node32 (Id);
-   end SPARK_Mode_Pragmas;
+   end SPARK_Pragma;
 
+   function SPARK_Pragma_Inherited (Id : E) return B is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Flag265 (Id);
+   end SPARK_Pragma_Inherited;
+
    function Spec_Entity (Id : E) return E is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -5527,9 +5560,29 @@
       Set_Ureal21 (Id, V);
    end Set_Small_Value;
 
-   procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) is
+   procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is
    begin
       pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Node33 (Id, V);
+   end Set_SPARK_Aux_Pragma;
+
+   procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Flag266 (Id, V);
+   end Set_SPARK_Aux_Pragma_Inherited;
+
+   procedure Set_SPARK_Pragma (Id : E; V : N) is
+   begin
+      pragma Assert
         (Ekind_In (Id, E_Function,         --  subprogram variants
                        E_Generic_Function,
                        E_Generic_Procedure,
@@ -5541,8 +5594,24 @@
                        E_Package_Body));
 
       Set_Node32 (Id, V);
-   end Set_SPARK_Mode_Pragmas;
+   end Set_SPARK_Pragma;
 
+   procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Flag265 (Id, V);
+   end Set_SPARK_Pragma_Inherited;
+
    procedure Set_Spec_Entity (Id : E; V : E) is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -8227,6 +8296,8 @@
       W ("Sec_Stack_Needed_For_Return",     Flag167 (Id));
       W ("Size_Depends_On_Discriminant",    Flag177 (Id));
       W ("Size_Known_At_Compile_Time",      Flag92  (Id));
+      W ("SPARK_Aux_Pragma_Inherited",      Flag266 (Id));
+      W ("SPARK_Pragma_Inherited",          Flag265 (Id));
       W ("Static_Elaboration_Desired",      Flag77  (Id));
       W ("Strict_Alignment",                Flag145 (Id));
       W ("Suppress_Elaboration_Warnings",   Flag148 (Id));
@@ -9366,7 +9437,7 @@
               E_Package_Body                               |
               E_Procedure                                  |
               E_Subprogram_Body                            =>
-            Write_Str ("SPARK_Mode_Pragmas");
+            Write_Str ("SPARK_Pragma");
 
          when others                                       =>
             Write_Str ("Field32??");
@@ -9380,6 +9451,11 @@
    procedure Write_Field33_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Generic_Package                            |
+              E_Package                                    |
+              E_Package_Body                               =>
+            Write_Str ("SPARK_Aux_Pragma");
+
          when others                                       =>
             Write_Str ("Field33??");
       end case;
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 206832)
+++ einfo.ads	(working copy)
@@ -3801,11 +3801,36 @@
 --       Small of the type, either as given in a representation clause, or
 --       as computed (as a power of two) by the compiler.
 
---    SPARK_Mode_Pragmas (Node32)
+--    SPARK_Aux_Pragma (Node33)
+--       Present in package spec and body entities. For a package spec entity
+--       it relates to the SPARK mode setting for the private part. This field
+--       points to the N_Pragma node that applies to the private part. This is
+--       either set with a local SPARK_Mode pragma in the private part or it is
+--       inherited from the SPARK mode that applies to the rest of the spec.
+--       For a package body, it similarly applies to the SPARK mode setting for
+--       the elaboration sequence after the BEGIN. In the case where the pragma
+--       is inherited, the SPARK_Aux_Pragma_Inherited flag is set in the
+--       package spec or body entity.
+
+--    SPARK_Aux_Pragma_Inherited (Flag266)
+--       Present in the entities of subprogram specs and bodies as well as
+--       in package specs and bodies. Set if the SPARK_Aux_Pragma field
+--       points to a pragma that is inherited, rather than a local one.
+
+--    SPARK_Pragma (Node32)
 --       Present in the entities of subprogram specs and bodies as well as in
---       package specs and bodies. Points to a list of SPARK_Mode pragmas that
---       apply to the related construct. Add note of what this is used for ???
+--       package specs and bodies. Points to the N_Pragma node that applies to
+--       the spec or body. This is either set by a local SPARK_Mode pragma or
+--       is inherited from the context (from an outer scope for the spec case
+--       or from the spec for the body case). In the case where it is inherited
+--       the flag SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma
+--       is applicable.
 
+--    SPARK_Pragma_Inherited (Flag265)
+--       Present in the entities of subprogram specs and bodies as well as in
+--       package specs and bodies. Set if the SPARK_Pragma field points to a
+--       pragma that is inherited, rather than a local one.
+
 --    Spec_Entity (Node19)
 --       Defined in package body entities. Points to corresponding package
 --       spec entity. Also defined in subprogram body parameters in the
@@ -5455,7 +5480,7 @@
    --    Subprograms_For_Type                (Node29)
    --    Corresponding_Equality              (Node30)   (implicit /= only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Elaboration_Entity_Required         (Flag174)
    --    Default_Expressions_Processed       (Flag108)
@@ -5493,6 +5518,7 @@
    --    Return_Present                      (Flag54)
    --    Returns_By_Ref                      (Flag90)
    --    Sec_Stack_Needed_For_Return         (Flag167)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Uses_Sec_Stack                      (Flag95)
    --    Address_Clause                      (synth)
    --    First_Formal                        (synth)
@@ -5655,7 +5681,8 @@
    --    Package_Instantiation               (Node26)
    --    Current_Use_Clause                  (Node27)
    --    Finalizer                           (Node28)   (non-generic case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Aux_Pragma                    (Node33)
+   --    SPARK_Pragma                        (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Discard_Names                       (Flag88)
@@ -5674,6 +5701,8 @@
    --    Is_Private_Descendant               (Flag53)
    --    Is_Visible_Lib_Unit                 (Flag116)
    --    Renamed_In_Spec                     (Flag231)  (non-generic case only)
+   --    SPARK_Aux_Pragma_Inherited          (Flag266)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Static_Elaboration_Desired          (Flag77)   (non-generic case only)
    --    Has_Null_Abstract_State             (synth)
    --    Is_Wrapper_Package                  (synth)    (non-generic case only)
@@ -5688,9 +5717,12 @@
    --    Scope_Depth_Value                   (Uint22)
    --    Contract                            (Node24)
    --    Finalizer                           (Node28)   (non-generic case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Aux_Pragma                    (Node33)
+   --    SPARK_Pragma                        (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Has_Anonymous_Master                (Flag253)
+   --    SPARK_Aux_Pragma_Inherited          (Flag266)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Scope_Depth                         (synth)
 
    --  E_Private_Type
@@ -5735,7 +5767,7 @@
    --    Extra_Formals                       (Node28)
    --    Static_Initialization               (Node30)   (init_proc only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Delay_Cleanups                      (Flag114)
    --    Discard_Names                       (Flag88)
@@ -5774,6 +5806,7 @@
    --    No_Return                           (Flag113)
    --    Requires_Overriding                 (Flag213)  (non-generic case only)
    --    Sec_Stack_Needed_For_Return         (Flag167)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Address_Clause                      (synth)
    --    First_Formal                        (synth)
    --    First_Formal_With_Extras            (synth)
@@ -5907,7 +5940,8 @@
    --    Scope_Depth_Value                   (Uint22)
    --    Contract                            (Node24)
    --    Extra_Formals                       (Node28)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Scope_Depth                         (synth)
 
    --  E_Subprogram_Type
@@ -6609,7 +6643,10 @@
    function Size_Depends_On_Discriminant        (Id : E) return B;
    function Size_Known_At_Compile_Time          (Id : E) return B;
    function Small_Value                         (Id : E) return R;
-   function SPARK_Mode_Pragmas                  (Id : E) return N;
+   function SPARK_Aux_Pragma                    (Id : E) return N;
+   function SPARK_Aux_Pragma_Inherited          (Id : E) return B;
+   function SPARK_Pragma                        (Id : E) return N;
+   function SPARK_Pragma_Inherited              (Id : E) return B;
    function Spec_Entity                         (Id : E) return E;
    function Static_Elaboration_Desired          (Id : E) return B;
    function Static_Initialization               (Id : E) return N;
@@ -7232,7 +7269,10 @@
    procedure Set_Size_Depends_On_Discriminant    (Id : E; V : B := True);
    procedure Set_Size_Known_At_Compile_Time      (Id : E; V : B := True);
    procedure Set_Small_Value                     (Id : E; V : R);
-   procedure Set_SPARK_Mode_Pragmas              (Id : E; V : N);
+   procedure Set_SPARK_Aux_Pragma                (Id : E; V : N);
+   procedure Set_SPARK_Aux_Pragma_Inherited      (Id : E; V : B := True);
+   procedure Set_SPARK_Pragma                    (Id : E; V : N);
+   procedure Set_SPARK_Pragma_Inherited          (Id : E; V : B := True);
    procedure Set_Spec_Entity                     (Id : E; V : E);
    procedure Set_Static_Elaboration_Desired      (Id : E; V : B);
    procedure Set_Static_Initialization           (Id : E; V : N);
@@ -7994,7 +8034,10 @@
    pragma Inline (Size_Depends_On_Discriminant);
    pragma Inline (Size_Known_At_Compile_Time);
    pragma Inline (Small_Value);
-   pragma Inline (SPARK_Mode_Pragmas);
+   pragma Inline (SPARK_Aux_Pragma);
+   pragma Inline (SPARK_Aux_Pragma_Inherited);
+   pragma Inline (SPARK_Pragma);
+   pragma Inline (SPARK_Pragma_Inherited);
    pragma Inline (Spec_Entity);
    pragma Inline (Static_Elaboration_Desired);
    pragma Inline (Static_Initialization);
@@ -8414,7 +8457,10 @@
    pragma Inline (Set_Size_Depends_On_Discriminant);
    pragma Inline (Set_Size_Known_At_Compile_Time);
    pragma Inline (Set_Small_Value);
-   pragma Inline (Set_SPARK_Mode_Pragmas);
+   pragma Inline (Set_SPARK_Aux_Pragma);
+   pragma Inline (Set_SPARK_Aux_Pragma_Inherited);
+   pragma Inline (Set_SPARK_Pragma);
+   pragma Inline (Set_SPARK_Pragma_Inherited);
    pragma Inline (Set_Spec_Entity);
    pragma Inline (Set_Static_Elaboration_Desired);
    pragma Inline (Set_Static_Initialization);
Index: lib.adb
===================================================================
--- lib.adb	(revision 206804)
+++ lib.adb	(working copy)
@@ -166,11 +166,6 @@
       return Units.Table (U).Source_Index;
    end Source_Index;
 
-   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id is
-   begin
-      return Units.Table (U).SPARK_Mode_Pragma;
-   end SPARK_Mode_Pragma;
-
    function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type is
    begin
       return Units.Table (U).Unit_File_Name;
@@ -259,11 +254,6 @@
       Units.Table (U).OA_Setting := C;
    end Set_OA_Setting;
 
-   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id) is
-   begin
-      Units.Table (U).SPARK_Mode_Pragma := N;
-   end Set_SPARK_Mode_Pragma;
-
    procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type) is
    begin
       Units.Table (U).Unit_Name := N;
Index: lib.ads
===================================================================
--- lib.ads	(revision 206804)
+++ lib.ads	(working copy)
@@ -371,10 +371,6 @@
    --      Set when the entry is created by a call to Lib.Load and then cannot
    --      be changed.
 
-   --    SPARK_Mode_Pragma
-   --      Pointer to the configuration pragma SPARK_Mode that applies to the
-   --      whole unit. Add note of what this is used for ???
-
    --    Unit_File_Name
    --      The name of the source file containing the unit. Set when the entry
    --      is created by a call to Lib.Load, and then cannot be changed.
@@ -426,7 +422,6 @@
    function Munit_Index       (U : Unit_Number_Type) return Nat;
    function OA_Setting        (U : Unit_Number_Type) return Character;
    function Source_Index      (U : Unit_Number_Type) return Source_File_Index;
-   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id;
    function Unit_File_Name    (U : Unit_Number_Type) return File_Name_Type;
    function Unit_Name         (U : Unit_Number_Type) return Unit_Name_Type;
    --  Get value of named field from given units table entry
@@ -445,7 +440,6 @@
    procedure Set_Main_CPU          (U : Unit_Number_Type; P : Int);
    procedure Set_Main_Priority     (U : Unit_Number_Type; P : Int);
    procedure Set_OA_Setting        (U : Unit_Number_Type; C : Character);
-   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id);
    procedure Set_Unit_Name         (U : Unit_Number_Type; N : Unit_Name_Type);
    --  Set value of named field for given units table entry. Note that we
    --  do not have an entry for each possible field, since some of the fields
@@ -749,10 +743,8 @@
    pragma Inline (Set_Main_CPU);
    pragma Inline (Set_Main_Priority);
    pragma Inline (Set_OA_Setting);
-   pragma Inline (Set_SPARK_Mode_Pragma);
    pragma Inline (Set_Unit_Name);
    pragma Inline (Source_Index);
-   pragma Inline (SPARK_Mode_Pragma);
    pragma Inline (Unit_File_Name);
    pragma Inline (Unit_Name);
 
Index: opt.ads
===================================================================
--- opt.ads	(revision 206871)
+++ opt.ads	(working copy)
@@ -1,5 +1,5 @@
 ------------------------------------------------------------------------------
---                                SPARK                                          --
+--                                                                          --
 --                         GNAT COMPILER COMPONENTS                         --
 --                                                                          --
 --                                  O P T                                   --
@@ -1272,6 +1272,11 @@
    --  GNAT
    --  Current SPARK mode setting
 
+   SPARK_Mode_Pragma : Node_Id := Empty;
+   --  GNAT
+   --  If the current SPARK_Mode (above) was set by a pragma, this records
+   --  the pragma that set this mode.
+
    SPARK_Switches_File_Name : String_Ptr := null;
    --  GNAT
    --  Set to non-null file name by use of the -gnates switch to specify
@@ -1909,8 +1914,13 @@
    --  start of analyzing each unit.
 
    SPARK_Mode_Config : SPARK_Mode_Type := None;
+   --  GNAT
    --  The setting of SPARK_Mode from configuration pragmas
 
+   SPARK_Mode_Pragma_Config : Node_Id := Empty;
+   --  If a SPARK_Mode pragma appeared in the configuration pragmas (setting
+   --  SPARK_Mode_Config appropriately), then this points to the N_Pragma node.
+
    Use_VADS_Size_Config : Boolean;
    --  GNAT
    --  This is the value of the configuration switch that controls the use of
@@ -2056,6 +2066,7 @@
       Polling_Required               : Boolean;
       Short_Descriptors              : Boolean;
       SPARK_Mode                     : SPARK_Mode_Type;
+      SPARK_Mode_Pragma              : Node_Id;
       Use_VADS_Size                  : Boolean;
    end record;
 
Index: sem.ads
===================================================================
--- sem.ads	(revision 206844)
+++ sem.ads	(working copy)
@@ -478,6 +478,9 @@
       Save_SPARK_Mode : SPARK_Mode_Type;
       --  Setting of SPARK_Mode on entry to restore on exit
 
+      Save_SPARK_Mode_Pragma : Node_Id;
+      --  Setting of SPARK_Mode_Pragma on entry to restore on exit
+
       Is_Transient : Boolean;
       --  Marks transient scopes (see Exp_Ch7 body for details)
 
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 206844)
+++ sem_ch3.adb	(working copy)
@@ -2162,15 +2162,15 @@
          --  it is and the mode is Off, the package body is considered to be in
          --  regular Ada and does not require refinement.
 
-         elsif Mode_Is_Off (SPARK_Mode_Pragmas (Body_Id)) then
+         elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
             return False;
 
          --  The body's SPARK_Mode may be inherited from a similar pragma that
          --  appears in the private declarations of the spec. The pragma we are
-         --  interested appears as the second entry in SPARK_Mode_Pragmas.
+         --  interested appears as the second entry in SPARK_Pragma.
 
-         elsif Present (SPARK_Mode_Pragmas (Spec_Id))
-           and then Mode_Is_Off (Next_Pragma (SPARK_Mode_Pragmas (Spec_Id)))
+         elsif Present (SPARK_Pragma (Spec_Id))
+           and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
          then
             return False;
 
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 206844)
+++ sem_ch6.adb	(working copy)
@@ -1186,6 +1186,9 @@
             end loop;
          end;
 
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
+
          Analyze_Declarations (Declarations (N));
          Check_Completion;
          Analyze (Handled_Statement_Sequence (N));
@@ -2923,6 +2926,8 @@
             Reference_Body_Formals (Spec_Id, Body_Id);
          end if;
 
+         Set_Ekind (Body_Id, E_Subprogram_Body);
+
          if Nkind (N) = N_Subprogram_Body_Stub then
             Set_Corresponding_Spec_Of_Stub (N, Spec_Id);
 
@@ -2989,9 +2994,17 @@
 
             --  Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
 
-            if Present (SPARK_Mode_Pragmas (Spec_Id)) then
-               SPARK_Mode :=
-                 Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+            if Present (SPARK_Pragma (Spec_Id)) then
+               SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
+               SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+               Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+            --  Otherwise set from context
+
+            else
+               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
             end if;
 
             --  Make sure that the subprogram is immediately visible. For
@@ -3003,7 +3016,6 @@
 
          Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
          Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
-         Set_Ekind (Body_Id, E_Subprogram_Body);
          Set_Scope (Body_Id, Scope (Spec_Id));
          Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
 
@@ -3550,8 +3562,9 @@
    ------------------------------------
 
    procedure Analyze_Subprogram_Declaration (N : Node_Id) is
-      Scop       : constant Entity_Id  := Current_Scope;
+      Scop       : constant Entity_Id := Current_Scope;
       Designator : Entity_Id;
+
       Is_Completion : Boolean;
       --  Indicates whether a null procedure declaration is a completion
 
@@ -3585,6 +3598,9 @@
 
       Generate_Definition (Designator);
 
+      Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (Designator, True);
+
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
          Write_Name (Chars (Designator));
Index: sem_ch7.adb
===================================================================
--- sem_ch7.adb	(revision 206844)
+++ sem_ch7.adb	(working copy)
@@ -346,13 +346,29 @@
 
       Push_Scope (Spec_Id);
 
-      --  Set SPARK_Mode from spec if package spec had SPARK_Mode pragma
+      --  Set SPARK_Mode from private part of spec if it has a SPARK pragma.
+      --  Note that in the default case, SPARK_Aux_Pragma will be a copy of
+      --  SPARK_Pragma in the spec, so this properly handles the case where
+      --  there is no explicit SPARK_Pragma mode in the private part.
 
-      if Present (SPARK_Mode_Pragmas (Spec_Id)) then
-         SPARK_Mode :=
-           Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+      if Present (SPARK_Pragma (Spec_Id)) then
+         SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
+         SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+      --  Otherwise set from context
+
+      else
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
       end if;
 
+      --  Set elaboration code SPARK mode the same for now
+
+      Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+      Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+
       Set_Categorization_From_Pragmas (N);
 
       Install_Visible_Declarations (Spec_Id);
@@ -798,6 +814,13 @@
       Set_Etype    (Id, Standard_Void_Type);
       Set_Contract (Id, Make_Contract (Sloc (Id)));
 
+      --  Inherit spark mode from context for now
+
+      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited     (Id, True);
+      Set_SPARK_Aux_Pragma_Inherited (Id, True);
+
       --  Analyze aspect specifications immediately, since we need to recognize
       --  things like Pure early enough to diagnose violations during analysis.
 
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb	(revision 206870)
+++ sem_ch8.adb	(working copy)
@@ -7400,6 +7400,7 @@
       Check_Policy_List        := SST.Save_Check_Policy_List;
       Default_Pool             := SST.Save_Default_Storage_Pool;
       SPARK_Mode               := SST.Save_SPARK_Mode;
+      SPARK_Mode_Pragma        := SST.Save_SPARK_Mode_Pragma;
 
       if Debug_Flag_W then
          Write_Str ("<-- exiting scope: ");
@@ -7474,6 +7475,7 @@
          SST.Save_Check_Policy_List        := Check_Policy_List;
          SST.Save_Default_Storage_Pool     := Default_Pool;
          SST.Save_SPARK_Mode               := SPARK_Mode;
+         SST.Save_SPARK_Mode_Pragma        := SPARK_Mode_Pragma;
 
          if Scope_Stack.Last > Scope_Stack.First then
             SST.Component_Alignment_Default := Scope_Stack.Table
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 206878)
+++ sem_prag.adb	(working copy)
@@ -18056,116 +18056,58 @@
          --  pragma SPARK_Mode [(On | Off | Auto)];
 
          when Pragma_SPARK_Mode => SPARK_Mod : declare
-            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id);
-            --  Associate a SPARK_Mode pragma with the context where it lives.
-            --  If the context is a package spec or a body, the routine checks
-            --  the consistency between modes of visible/private declarations
-            --  and body declarations/statements.
+            Body_Id : Entity_Id;
+            Context : Node_Id;
+            Mode    : Name_Id;
+            Mode_Id : SPARK_Mode_Type;
+            Spec_Id : Entity_Id;
+            Stmt    : Node_Id;
 
-            procedure Check_Spark_Mode_Conformance
-              (Governing_Id : Entity_Id;
-               New_Id       : Entity_Id);
-            --  Verify the "monotonicity" of SPARK modes between two entities.
-            --  The order of modes is Off < Auto < On. Governing_Id establishes
-            --  the mode of the context. New_Id is the desired new mode.
+            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
+            --  Verify the monotonicity of SPARK modes between the new pragma
+            --  N, and the old pragma, Old_Pragma, that was inherited. If
+            --  Old_Pragma is Empty, the call has no effect, otherwise we
+            --  verify that the new mode is less restrictive than the old mode.
+            --  For example, if the old mode is ON, then the new mode can be
+            --  anything. But if the old mode is OFF, then the only allowed
+            --  new mode is also OFF. If there is no error, this routine also
+            --  sets SPARK_Mode_Pragma to N, and SPARK_Mode to Mode_Id.
 
-            procedure Check_Pragma_Conformance
-              (Governing_Mode : Node_Id;
-               New_Mode       : Node_Id);
-            --  Verify the "monotonicity" of two SPARK_Mode pragmas. The order
-            --  of modes is Off < Auto < On. Governing_Mode is the established
-            --  mode dictated by the context. New_Mode attempts to redefine the
-            --  governing mode.
-
             function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
             --  Convert a value of type SPARK_Mode_Type to corresponding name
 
-            ------------------
-            -- Chain_Pragma --
-            ------------------
-
-            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
-               Existing_Prag : constant Node_Id :=
-                                 SPARK_Mode_Pragmas (Context);
-
-            begin
-               --  Chain existing pragmas to this one, checking consistency
-
-               if Present (Existing_Prag) then
-                  Check_Pragma_Conformance
-                    (Governing_Mode => Existing_Prag,
-                     New_Mode       => Prag);
-
-                  Set_Next_Pragma (Prag, Existing_Prag);
-               end if;
-
-               Set_SPARK_Mode_Pragmas (Context, Prag);
-            end Chain_Pragma;
-
-            ----------------------------------
-            -- Check_Spark_Mode_Conformance --
-            ----------------------------------
-
-            procedure Check_Spark_Mode_Conformance
-              (Governing_Id : Entity_Id;
-               New_Id       : Entity_Id)
-            is
-               Gov_Prag : constant Node_Id :=
-                            SPARK_Mode_Pragmas (Governing_Id);
-               New_Prag : constant Node_Id := SPARK_Mode_Pragmas (New_Id);
-
-            begin
-               --  Nothing to do when one or both entities lack a mode
-
-               if No (Gov_Prag) or else No (New_Prag) then
-                  return;
-               end if;
-
-               --  Do not compare the modes of a package spec and body when the
-               --  spec mode appears in the private part. In this case the spec
-               --  mode does not affect the body.
-
-               if Ekind_In (Governing_Id, E_Generic_Package, E_Package)
-                 and then Ekind (New_Id) = E_Package_Body
-                 and then Is_Private_SPARK_Mode (Gov_Prag)
-               then
-                  null;
-
-               --  Test the pragmas
-
-               else
-                  Check_Pragma_Conformance
-                    (Governing_Mode => Gov_Prag,
-                     New_Mode       => New_Prag);
-               end if;
-            end Check_Spark_Mode_Conformance;
-
             ------------------------------
             -- Check_Pragma_Conformance --
             ------------------------------
 
-            procedure Check_Pragma_Conformance
-              (Governing_Mode : Node_Id;
-               New_Mode       : Node_Id)
-            is
-               Gov_M : constant SPARK_Mode_Type :=
-                         Get_SPARK_Mode_From_Pragma (Governing_Mode);
-               New_M : constant SPARK_Mode_Type :=
-                         Get_SPARK_Mode_From_Pragma (New_Mode);
-
+            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
             begin
-               --  The new mode is less restrictive than the established mode
+               if Present (Old_Pragma) then
+                  pragma Assert (Nkind (Old_Pragma) = N_Pragma);
 
-               if Gov_M < New_M then
-                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (New_M);
-                  Error_Msg_N ("cannot define 'S'P'A'R'K mode %", New_Mode);
+                  declare
+                     Gov_M : constant SPARK_Mode_Type :=
+                                Get_SPARK_Mode_From_Pragma (Old_Pragma);
 
-                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (Gov_M);
-                  Error_Msg_Sloc   := Sloc (Governing_Mode);
-                  Error_Msg_N
-                    ("\mode is less restrictive than mode % defined #",
-                     New_Mode);
+                  begin
+                     --  New mode less restrictive than the established mode
+
+                     if Gov_M < Mode_Id then
+                        Error_Msg_Name_1 := Mode;
+                        Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1);
+
+                        Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode);
+                        Error_Msg_Sloc   := Sloc (SPARK_Mode_Pragma);
+                        Error_Msg_N
+                          ("\mode is less restrictive than mode "
+                           & "% defined #", Arg1);
+                        raise Pragma_Exit;
+                     end if;
+                  end;
                end if;
+
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
             end Check_Pragma_Conformance;
 
             -------------------------
@@ -18190,15 +18132,6 @@
                end if;
             end Get_SPARK_Mode_Name;
 
-            --  Local variables
-
-            Body_Id : Entity_Id;
-            Context : Node_Id;
-            Mode    : Name_Id;
-            Mode_Id : SPARK_Mode_Type;
-            Spec_Id : Entity_Id;
-            Stmt    : Node_Id;
-
          --  Start of processing for SPARK_Mod
 
          begin
@@ -18217,20 +18150,30 @@
 
             Mode_Id := Get_SPARK_Mode_Type (Mode);
             Context := Parent (N);
-            SPARK_Mode := Mode_Id;
 
-            --  The pragma appears in a configuration file
+            --  The pragma appears in a configuration pragmas file
 
             if No (Context) then
                Check_Valid_Configuration_Pragma;
 
+               if Present (SPARK_Mode_Pragma) then
+                  Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+                  Error_Msg_N ("pragma% duplicates pragma declared#", N);
+                  raise Pragma_Exit;
+               end if;
+
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
+
             --  When the pragma is placed before the declaration of a unit, it
             --  configures the whole unit.
 
             elsif Nkind (Context) = N_Compilation_Unit then
                Check_Valid_Configuration_Pragma;
-                  Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
 
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
+
             --  The pragma applies to a [library unit] subprogram or package
 
             else
@@ -18238,8 +18181,8 @@
 
                if Mode_Id = Auto then
                   Error_Pragma_Arg
-                    ("mode `Auto` can only apply to the configuration variant "
-                     & "of pragma %", Arg1);
+                    ("mode `Auto` is only allowed when pragma % appears as "
+                     & "a configuration pragma", Arg1);
                end if;
 
                --  Verify the placement of the pragma with respect to package
@@ -18255,6 +18198,7 @@
                         Error_Msg_Name_1 := Pname;
                         Error_Msg_Sloc   := Sloc (Stmt);
                         Error_Msg_N ("pragma% duplicates pragma declared#", N);
+                        raise Pragma_Exit;
                      end if;
 
                   --  Skip internally generated code
@@ -18262,15 +18206,31 @@
                   elsif not Comes_From_Source (Stmt) then
                      null;
 
-                  --  The pragma applies to a package or subprogram declaration
+                  --  The pragma applies to a package declaration
 
                   elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
-                                        N_Generic_Subprogram_Declaration,
-                                        N_Package_Declaration,
+                                        N_Package_Declaration)
+                  then
+                     Spec_Id := Defining_Unit_Name (Specification (Stmt));
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+
+                     return;
+
+                  --  The pragma applies to a subprogram declaration
+
+                  elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
                                         N_Subprogram_Declaration)
                   then
                      Spec_Id := Defining_Unit_Name (Specification (Stmt));
-                     Chain_Pragma (Spec_Id, N);
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
                      return;
 
                   --  The pragma does not apply to a legal construct, issue an
@@ -18304,48 +18264,79 @@
                   end if;
                end if;
 
-               --  The pragma is at the top level of a package spec or appears
-               --  as an aspect on a subprogram.
+               --  The pragma is at the top level of a package spec
 
-               --    function F ... with SPARK_Mode => ...;
-
                --    package P is
                --       pragma SPARK_Mode;
 
-               if Nkind_In (Context, N_Function_Specification,
-                                     N_Package_Specification,
-                                     N_Procedure_Specification)
+               --      or
+
+               --    package P is
+               --      ...
+               --    private
+               --      pragma SPARK_Mode;
+
+               if Nkind (Context) = N_Package_Specification then
+                  Spec_Id := Defining_Unit_Name (Context);
+
+                  --  Pragma applies to private part
+
+                  if List_Containing (N) = Private_Declarations (Context) then
+                     Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
+
+                  --  Pragma applies to public part
+
+                  else
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+                  end if;
+
+               --  The pragma appears as an aspect on a subprogram.
+
+               --    function F ... with SPARK_Mode => ...;
+
+               elsif Nkind_In (Context, N_Function_Specification,
+                                        N_Procedure_Specification)
                then
                   Spec_Id := Defining_Unit_Name (Context);
-                  Chain_Pragma (Spec_Id, N);
+                  Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
 
-               --  Pragma is immediately within a package or subprogram body
+                  Set_SPARK_Pragma           (Spec_Id, N);
+                  Set_SPARK_Pragma_Inherited (Spec_Id, False);
 
-               --    function F ... is
-               --       pragma SPARK_Mode;
+               --  Pragma is immediately within a package body
 
                --    package body P is
                --       pragma SPARK_Mode;
 
-               elsif Nkind_In (Context, N_Package_Body,
-                                        N_Subprogram_Body)
-               then
+               elsif Nkind (Context) = N_Package_Body then
                   Spec_Id := Corresponding_Spec (Context);
+                  Body_Id := Defining_Entity (Context);
+                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
 
-                  if Nkind (Context) = N_Subprogram_Body then
-                     Context := Specification (Context);
-                  end if;
+                  Set_SPARK_Pragma               (Body_Id, N);
+                  Set_SPARK_Pragma_Inherited     (Body_Id, False);
+                  Set_SPARK_Aux_Pragma           (Body_Id, N);
+                  Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
 
-                  Body_Id := Defining_Entity (Context);
+               --  Pragma is immediately within a subprogram body
 
-                  Chain_Pragma (Body_Id, N);
+               --    function F ... is
+               --       pragma SPARK_Mode;
 
-                  --  Verify that the SPARK modes are consistent between
-                  --  body and spec, if any.
+               elsif Nkind (Context) = N_Subprogram_Body then
+                  Spec_Id := Corresponding_Spec (Context);
+                  Context := Specification (Context);
+                  Body_Id := Defining_Entity (Context);
+                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
 
-                  if Present (Spec_Id) then
-                     Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
-                  end if;
+                  Set_SPARK_Pragma           (Body_Id, N);
+                  Set_SPARK_Pragma_Inherited (Body_Id, False);
 
                --  The pragma applies to the statements of a package body
 
@@ -18359,9 +18350,10 @@
                   Context := Parent (Context);
                   Spec_Id := Corresponding_Spec (Context);
                   Body_Id := Defining_Unit_Name (Context);
+                  Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
 
-                  Chain_Pragma (Body_Id, N);
-                  Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
+                  Set_SPARK_Aux_Pragma           (Body_Id, N);
+                  Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
 
                --  The pragma does not apply to a legal construct, issue error
 


More information about the Gcc-patches mailing list