[Ada] Synchronization of SPARK implementation against reference manual

Arnaud Charlet charlet@adacore.com
Mon Jan 27 16:35:00 GMT 2014


This patch updates the implementation of various SPARK features by removing
obsolete checks based on old rules and introduces new cheks to satisfy the
latest version of the SPARK reference manual. The tools now produce superior
error messages that reference various SPARK manual sections where possible.

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

2014-01-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb (Is_Input_Only_State): Removed.
	(Is_Non_Volatile_State): Removed.
	(Is_Output_State): Removed.
	* einfo.ads (Is_Input_Only_State): Remove attribute and
	subprogram. Update related entity.
	(Is_Non_Volatile_State):
	Remove attribute and subprogram. Update related entity.
	(Is_Output_State): Removed attribute and subprogram. Update
	related entity.
	* exp_ch6.adb (Expand_Subprogram_Contract): Update comment on
	generated code.
	* sem_ch3.adb (Analyze_Declarations): Analyze the contract of
	an object, not just variables.
	(Analyze_Object_Contract): New routine.
	(Analyze_Variable_Contract): Removed.
	(Process_Discriminants): Detect an illegal use of volatile
	discriminant in SPARK mode.
	* sem_ch5.adb (Analyze_Iterator_Specification):
	Detect an illegal use of volatile loop variable.
	(Analyze_Loop_Parameter_Specification): Detect an illegal use
	of volatile loop variable.
	* sem_ch6.adb (Process_Formals): Update the volatile object
	detection. Detect an illegal formal of mode IN OUT or OUT in
	SPARK mode. Enhance the error messages with references.
	* sem_ch12.adb (Instantiate_Object): Update the volatile object
	detection. Enhance the error messages with references.
	* sem_prag.adb (Analyze_Abstract_State): Enhance the error
	messages with references.
	(Analyze_Contract_Case): Enhance the error messages with references.
	(Analyze_External_Property): Call Check_Duplicate_Property to process
	an external property.
	(Analyze_External_Property_In_Decl_Part): New routine.
	(Analyze_External_State_In_Decl_Part): Removed.
	(Analyze_Global_Item): Detect an illegal
	use of a volatile constant. Detect an illegal use
	of a variable with enabled Effective_Reads. Enhance
	the error messages with references. Remove obsolete
	checks concerning Input_Only and Output_Only states.
	(Analyze_Initialization_Item): Enhance the error messages
	with references.
	(Analyze_Initializes_In_Decl_Part): Do not
	collect the states and variables when the initialization list
	is null.
	(Analyze_Input_Item): Enhance the error messages with references.
	(Analyze_Input_Output): Enhance the error messages with references.
	(Analyze_Pragma): Enhance the error messages with references.
	(Analyze_Refinement_Clause): Code reformatting.
	(Analyze_Refined_Depends_In_Decl_Part):
	Rename global variable Global to Reg_Global and update all
	occurrences. Add local variables D7 and D8. Update the error
	messages with references. Update the call to Collect_Global_Items.
	(Analyze_Refined_Global_In_Decl_Part): Add local variables
	Has_Proof_In_State, Proof_In_Constits and Proof_In_Items. Update
	the call to Collect_Global_Items.  Account for a Proof_In state
	in null / useless refinement checks. Verify the coverage of
	Proof_In states.
	(Check_Dependency_Clause): Remove local variable
	Out_Constits. Remove the retrieval and removal of constituents
	for an Output_Only state. Remove the reporting of unused
	Output_Only state constituents.
	(Check_Duplicate_Mode): Enhance
	the error message with a reference.
	(Check_Duplicate_Property): New routine.
	(Check_Duplicate_Option): Enhance the error message with a reference.
	(Check_External_Properties): Enhance the error message with a reference.
	(Check_Function_Return): Enhance the error message with a reference.
	(Check_In_Out_States): Update
	comment on usage. Add a specialized error message for Proof_In
	constituents. Enhance the error message with a reference.
	(Check_Input_States): Update comment on usage. Account for
	possible Proof_In constituents. Enhance the error message
	with a areference.
	(Check_Matching_Constituent): Enhance the error message with a
	reference.
	(Check_Matching_State): Enchance the error message with a reference.
	(Check_Mode): Add local variable From_Global. Update the call to
	Find_Mode.  Emit more precise error messages concerning extra items
	(Check_Mode_Restriction_In_Enclosing_Context): Consider
	pragma Refined_Global.	Enhance the error message with a
	reference.
	(Check_Mode_Restriction_In_Function): Enhance the error message with
	a reference.
	(Check_Output_States): Update comment on usage. Add local variable
	Posted.  Account for possible Proof_In constituents. Produce a detailed
	list of missing constituents.
	(Check_Proof_In_States): New routine.
	(Check_Refined_Global_Item): Handle Proof_In
	constituents. Enchance the error message with a reference.
	(Collect_Global_Items): Add formal parameters Proof_In_Items
	and Has_Proof_In_State. Update the comment on usage. Account
	for Proof_In items.
	(Create_Or_Modify_Clause): Enchance
	the error message with a reference.
	(Find_Mode): Add
	formal parameter From_Global. Update the comment on usage.
	Detect when the mode is governed by pragma [Refined_]Global.
	(Output_Constituents): Removed.
	(Report_Extra_Constituents):
	Report extra Proof_In constituents.
	(Report_Unused_Constituents): Removed.
	(Usage_Error): Code reformatting. Enhance the error
	messages with reference.
	* sem_prag.ads (Analyze_External_Property_In_Decl_Part): New routine.
	(Analyze_External_State_In_Decl_Part): Removed.
	* sem_res.adb (Resolve_Actuals): Update the volatile object
	detection. Enhance the error message with a reference.
	(Resolve_Entity_Name): Update the volatile object
	detection. Enhance the error message with a reference.
	* sem_util.adb (Is_Refined_State): Add a guard to avoid a crash.
	(Is_SPARK_Volatile_Object): New routine.
	(Has_Volatile_Component): New routine.
	* sem_util.ads (Is_Delegate): Alphabetized.
	(Is_SPARK_Volatile_Object): New routine.
	(Has_Volatile_Component): New routine.
	* snames.ads-tmpl: Remove names Name_Input_Only and Name_Output_Only.

-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 207120)
+++ sem_ch3.adb	(working copy)
@@ -91,10 +91,10 @@
    --  abstract interface types implemented by a record type or a derived
    --  record type.
 
-   procedure Analyze_Variable_Contract (Var_Id : Entity_Id);
-   --  Analyze all delayed aspects chained on the contract of variable Var_Id
-   --  as if they appeared at the end of the declarative region. The aspects
-   --  to be considered are:
+   procedure Analyze_Object_Contract (Obj_Id : Entity_Id);
+   --  Analyze all delayed aspects chained on the contract of object Obj_Id as
+   --  if they appeared at the end of the declarative region. The aspects to be
+   --  considered are:
    --    Async_Readers
    --    Async_Writers
    --    Effective_Reads
@@ -2478,10 +2478,8 @@
          elsif Nkind (Decl) = N_Subprogram_Declaration then
             Analyze_Subprogram_Contract (Defining_Entity (Decl));
 
-         elsif Nkind (Decl) = N_Object_Declaration
-           and then Ekind (Defining_Entity (Decl)) = E_Variable
-         then
-            Analyze_Variable_Contract (Defining_Entity (Decl));
+         elsif Nkind (Decl) = N_Object_Declaration then
+            Analyze_Object_Contract (Defining_Entity (Decl));
          end if;
 
          Next (Decl);
@@ -3071,6 +3069,106 @@
       end if;
    end Analyze_Number_Declaration;
 
+   -----------------------------
+   -- Analyze_Object_Contract --
+   -----------------------------
+
+   procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
+      AR_Val : Boolean := False;
+      AW_Val : Boolean := False;
+      ER_Val : Boolean := False;
+      EW_Val : Boolean := False;
+      Items  : Node_Id;
+      Nam    : Name_Id;
+      Prag   : Node_Id;
+      Seen   : Boolean := False;
+
+   begin
+      if Ekind (Obj_Id) = E_Constant then
+
+         --  A constant cannot be volatile. This check is only relevant when
+         --  SPARK_Mode is on as it is not standard Ada legality rule. Do not
+         --  flag internally-generated constants that map generic formals to
+         --  actuals in instantiations.
+
+         if SPARK_Mode = On
+           and then Is_SPARK_Volatile_Object (Obj_Id)
+           and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
+         then
+            Error_Msg_N
+              ("constant cannot be volatile (SPARK RM 7.1.3(4))", Obj_Id);
+         end if;
+
+      else pragma Assert (Ekind (Obj_Id) = E_Variable);
+
+         --  The following checks are only relevant when SPARK_Mode is on as
+         --  they are not standard Ada legality rules.
+
+         if SPARK_Mode = On then
+
+            --  A non-volatile object cannot have volatile components
+
+            if not Is_SPARK_Volatile_Object (Obj_Id)
+              and then Has_Volatile_Component (Etype (Obj_Id))
+            then
+               Error_Msg_N
+                 ("non-volatile variable & cannot have volatile components "
+                  & "(SPARK RM 7.1.3(6))", Obj_Id);
+
+            --  The declaration of a volatile object must appear at the library
+            --  level.
+
+            elsif Is_SPARK_Volatile_Object (Obj_Id)
+              and then not Is_Library_Level_Entity (Obj_Id)
+            then
+               Error_Msg_N
+                 ("volatile variable & must be declared at library level "
+                  & "(SPARK RM 7.1.3(5))", Obj_Id);
+            end if;
+         end if;
+
+         --  Examine the contract
+
+         Items := Contract (Obj_Id);
+
+         if Present (Items) then
+
+            --  Analyze classification pragmas
+
+            Prag := Classifications (Items);
+            while Present (Prag) loop
+               Nam := Pragma_Name (Prag);
+
+               if Nam = Name_Async_Readers then
+                  Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
+                  Seen := True;
+
+               elsif Nam = Name_Async_Writers then
+                  Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
+                  Seen := True;
+
+               elsif Nam = Name_Effective_Reads then
+                  Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
+                  Seen := True;
+
+               else pragma Assert (Nam = Name_Effective_Writes);
+                  Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
+                  Seen := True;
+               end if;
+
+               Prag := Next_Pragma (Prag);
+            end loop;
+         end if;
+
+         --  Once all external properties have been processed, verify their
+         --  mutual interaction.
+
+         if Seen then
+            Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
+         end if;
+      end if;
+   end Analyze_Object_Contract;
+
    --------------------------------
    -- Analyze_Object_Declaration --
    --------------------------------
@@ -4889,73 +4987,6 @@
       end if;
    end Analyze_Subtype_Indication;
 
-   -------------------------------
-   -- Analyze_Variable_Contract --
-   -------------------------------
-
-   procedure Analyze_Variable_Contract (Var_Id : Entity_Id) is
-      Items  : constant Node_Id := Contract (Var_Id);
-      AR_Val : Boolean := False;
-      AW_Val : Boolean := False;
-      ER_Val : Boolean := False;
-      EW_Val : Boolean := False;
-      Nam    : Name_Id;
-      Prag   : Node_Id;
-      Seen   : Boolean := False;
-
-   begin
-      --  The declaration of a volatile variable must appear at the library
-      --  level. The check is only relevant when SPARK_Mode is on as it is not
-      --  standard Ada legality rule.
-
-      if SPARK_Mode = On
-        and then Is_Volatile_Object (Var_Id)
-        and then not Is_Library_Level_Entity (Var_Id)
-      then
-         Error_Msg_N
-           ("volatile variable & must be declared at library level (SPARK RM "
-            & "7.1.3(3))", Var_Id);
-      end if;
-
-      --  Examine the contract
-
-      if Present (Items) then
-
-         --  Analyze classification pragmas
-
-         Prag := Classifications (Items);
-         while Present (Prag) loop
-            Nam := Pragma_Name (Prag);
-
-            if Nam = Name_Async_Readers then
-               Analyze_External_State_In_Decl_Part (Prag, AR_Val);
-               Seen := True;
-
-            elsif Nam = Name_Async_Writers then
-               Analyze_External_State_In_Decl_Part (Prag, AW_Val);
-               Seen := True;
-
-            elsif Nam = Name_Effective_Reads then
-               Analyze_External_State_In_Decl_Part (Prag, ER_Val);
-               Seen := True;
-
-            else pragma Assert (Nam = Name_Effective_Writes);
-               Analyze_External_State_In_Decl_Part (Prag, EW_Val);
-               Seen := True;
-            end if;
-
-            Prag := Next_Pragma (Prag);
-         end loop;
-      end if;
-
-      --  Once all external properties have been processed, verify their mutual
-      --  interaction.
-
-      if Seen then
-         Check_External_Properties (Var_Id, AR_Val, AW_Val, ER_Val, EW_Val);
-      end if;
-   end Analyze_Variable_Contract;
-
    --------------------------
    -- Analyze_Variant_Part --
    --------------------------
@@ -18076,6 +18107,16 @@
             end if;
          end if;
 
+         --  A discriminant cannot be volatile. This check is only relevant
+         --  when SPARK_Mode is on as it is not standard Ada legality rule.
+
+         if SPARK_Mode = On
+           and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
+         then
+            Error_Msg_N
+              ("discriminant cannot be volatile (SPARK RM 7.1.3(6))", Discr);
+         end if;
+
          Next (Discr);
       end loop;
 
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 207120)
+++ sem_ch5.adb	(working copy)
@@ -1921,6 +1921,14 @@
             end loop;
          end if;
       end if;
+
+      --  A loop parameter cannot be volatile. This check is peformed only when
+      --  SPARK_Mode is on as it is not a standard Ada legality check.
+
+      if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Ent) then
+         Error_Msg_N
+           ("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Ent);
+      end if;
    end Analyze_Iterator_Specification;
 
    -------------------
@@ -2550,6 +2558,14 @@
             end if;
          end;
       end if;
+
+      --  A loop parameter cannot be volatile. This check is peformed only when
+      --  SPARK_Mode is on as it is not a standard Ada legality check.
+
+      if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
+         Error_Msg_N
+           ("loop parameter cannot be volatile (SPARK RM 7.1.3(6))", Id);
+      end if;
    end Analyze_Loop_Parameter_Specification;
 
    ----------------------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 207135)
+++ einfo.adb	(working copy)
@@ -6912,28 +6912,6 @@
       end if;
    end Is_Ghost_Subprogram;
 
-   -------------------------
-   -- Is_Input_Only_State --
-   -------------------------
-
-   function Is_Input_Only_State (Id : E) return B is
-   begin
-      return
-        Ekind (Id) = E_Abstract_State
-          and then Has_Option (Id, Name_Input_Only);
-   end Is_Input_Only_State;
-
-   ---------------------------
-   -- Is_Non_Volatile_State --
-   ---------------------------
-
-   function Is_Non_Volatile_State (Id : E) return B is
-   begin
-      return
-        Ekind (Id) = E_Abstract_State
-          and then Has_Option (Id, Name_Non_Volatile);
-   end Is_Non_Volatile_State;
-
    -------------------
    -- Is_Null_State --
    -------------------
@@ -6944,17 +6922,6 @@
         Ekind (Id) = E_Abstract_State and then Nkind (Parent (Id)) = N_Null;
    end Is_Null_State;
 
-   ---------------------
-   -- Is_Output_State --
-   ---------------------
-
-   function Is_Output_Only_State (Id : E) return B is
-   begin
-      return
-        Ekind (Id) = E_Abstract_State
-          and then Has_Option (Id, Name_Output_Only);
-   end Is_Output_Only_State;
-
    -----------------------------------
    -- Is_Package_Or_Generic_Package --
    -----------------------------------
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 207135)
+++ einfo.ads	(working copy)
@@ -2400,10 +2400,6 @@
 --       inherited by their instances. It is also set on the body entities
 --       of inlined subprograms. See also Has_Pragma_Inline.
 
---    Is_Input_Only_State (synthesized)
---       Applies to all entities, true for abstract states that are subject to
---       option Input_Only.
-
 --    Is_Instantiated (Flag126)
 --       Defined in generic packages and generic subprograms. Set if the unit
 --       is instantiated from somewhere in the extended main source unit. This
@@ -2593,10 +2589,6 @@
 --       set right, at which point, these comments can be removed, and the
 --       tests for static subtypes greatly simplified.
 
---    Is_Non_Volatile_State (synthesized)
---       Applies to all entities, true for abstract states that are subject to
---       option Non_Volatile.
-
 --    Is_Null_Init_Proc (Flag178)
 --       Defined in procedure entities. Set for generated init proc procedures
 --       (used to initialize composite types), if the code for the procedure
@@ -2637,10 +2629,6 @@
 --       Applies to all entities, true for ordinary fixed point types and
 --       subtypes.
 
---    Is_Output_Only_State (synthesized)
---       Applies to all entities, true for abstract states that are subject to
---       option Output_Only.
-
 --    Is_Package_Or_Generic_Package (synthesized)
 --       Applies to all entities. True for packages and generic packages.
 --       False for all other entities.
@@ -5167,10 +5155,7 @@
    --    Has_Non_Null_Refinement             (synth)
    --    Has_Null_Refinement                 (synth)
    --    Is_External_State                   (synth)
-   --    Is_Input_Only_State                 (synth)
    --    Is_Null_State                       (synth)
-   --    Is_Output_Only_State                (synth)
-   --    Is_Non_Volatile_State               (synth)
 
    --  E_Access_Protected_Subprogram_Type
    --    Equivalent_Type                     (Node18)
@@ -6787,10 +6772,7 @@
    function Is_Finalizer                        (Id : E) return B;
    function Is_Ghost_Entity                     (Id : E) return B;
    function Is_Ghost_Subprogram                 (Id : E) return B;
-   function Is_Input_Only_State                 (Id : E) return B;
-   function Is_Non_Volatile_State               (Id : E) return B;
    function Is_Null_State                       (Id : E) return B;
-   function Is_Output_Only_State                (Id : E) return B;
    function Is_Package_Or_Generic_Package       (Id : E) return B;
    function Is_Prival                           (Id : E) return B;
    function Is_Protected_Component              (Id : E) return B;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 207136)
+++ sem_prag.adb	(working copy)
@@ -204,21 +204,23 @@
    --  in identifiers to represent these attribute references.
 
    procedure Collect_Global_Items
-     (Prag             : Node_Id;
-      In_Items         : in out Elist_Id;
-      In_Out_Items     : in out Elist_Id;
-      Out_Items        : in out Elist_Id;
-      Has_In_State     : out Boolean;
-      Has_In_Out_State : out Boolean;
-      Has_Out_State    : out Boolean;
-      Has_Null_State   : out Boolean);
+     (Prag               : Node_Id;
+      In_Items           : in out Elist_Id;
+      In_Out_Items       : in out Elist_Id;
+      Out_Items          : in out Elist_Id;
+      Proof_In_Items     : in out Elist_Id;
+      Has_In_State       : out Boolean;
+      Has_In_Out_State   : out Boolean;
+      Has_Out_State      : out Boolean;
+      Has_Proof_In_State : out Boolean;
+      Has_Null_State     : out Boolean);
    --  Subsidiary to the analysis of pragma Refined_Depends/Refined_Global.
-   --  Prag denotes pragma [Refined_]Global. Gather all input, in out and
-   --  output items of Prag in lists In_Items, In_Out_Items and Out_Items.
-   --  Flags Has_In_State, Has_In_Out_State and Has_Out_State are set when
-   --  there is at least one abstract state with visible refinement available
-   --  in the corresponding mode. Flag Has_Null_State is set when at least
-   --  state has a null refinement.
+   --  Prag denotes pragma [Refined_]Global. Gather all input, in out, output
+   --  and Proof_In items of Prag in lists In_Items, In_Out_Items, Out_Items
+   --  and Proof_In_Items. Flags Has_In_State, Has_In_Out_State, Has_Out_State
+   --  and Has_Proof_In_State are set when there is at least one abstract state
+   --  with visible refinement available in the corresponding mode. Flag
+   --  Has_Null_State is set when at least state has a null refinement.
 
    procedure Collect_Subprogram_Inputs_Outputs
      (Subp_Id      : Entity_Id;
@@ -402,16 +404,16 @@
             if Nkind (Case_Guard) = N_Others_Choice then
                if Others_Seen then
                   Error_Msg_N
-                    ("only one others choice allowed in aspect Contract_Cases",
-                     Case_Guard);
+                    ("only one others choice allowed in aspect Contract_Cases "
+                     & "(SPARK RM 6.1.3(1))", Case_Guard);
                else
                   Others_Seen := True;
                end if;
 
             elsif Others_Seen then
                Error_Msg_N
-                 ("others must be the last choice in aspect Contract_Cases",
-                  N);
+                 ("others must be the last choice in aspect Contract_Cases "
+                  & "(SPARK RM 6.1.3(1))", N);
             end if;
 
             --  Preanalyze the case guard and consequence
@@ -717,13 +719,15 @@
                   Error_Msg_Name_1 := Name_Result;
                   Error_Msg_N
                     ("prefix of attribute % must denote the enclosing "
-                     & "function", Item);
+                     & "function (SPARK RM 6.1.5(11))", Item);
 
                --  Function'Result is allowed to appear on the output side of a
                --  dependency clause.
 
                elsif Is_Input then
-                  Error_Msg_N ("function result cannot act as input", Item);
+                  Error_Msg_N
+                    ("function result cannot act as input (SPARK RM 6.1.5(6))",
+                     Item);
 
                elsif Null_Seen then
                   Error_Msg_N
@@ -753,7 +757,7 @@
                      if not Is_Last then
                         Error_Msg_N
                           ("null output list must be the last clause in a "
-                           & "dependency relation", Item);
+                           & "dependency relation (SPARK RM 6.1.5(12))", Item);
 
                      --  Catch a useless dependence of the form:
                      --    null =>+ ...
@@ -817,7 +821,7 @@
                      then
                         Error_Msg_N
                           ("input of a null output list appears in multiple "
-                           & "input lists", Item);
+                           & "input lists (SPARK RM 6.1.5(13))", Item);
                      end if;
 
                      --  Add an input or a self-referential output to the list
@@ -852,7 +856,8 @@
                         elsif Has_Visible_Refinement (Item_Id) then
                            Error_Msg_NE
                              ("cannot mention state & in global refinement, "
-                              & "use its constituents instead", Item, Item_Id);
+                              & "use its constituents instead (SPARK RM "
+                              & "6.1.5(3))", Item, Item_Id);
                            return;
                         end if;
                      end if;
@@ -871,15 +876,15 @@
                   else
                      Error_Msg_N
                         ("item must denote variable, state or formal "
-                         & "parameter", Item);
+                         & "parameter (SPARK RM 6.1.5(1))", Item);
                   end if;
 
                --  All other input/output items are illegal
 
                else
                   Error_Msg_N
-                    ("item must denote variable, state or formal parameter",
-                     Item);
+                    ("item must denote variable, state or formal parameter "
+                     & "(SPARK RM 6.1.5(1))", Item);
                end if;
             end if;
          end Analyze_Input_Output;
@@ -936,8 +941,8 @@
       begin
          if Ekind (Spec_Id) = E_Function and then not Result_Seen then
             Error_Msg_NE
-              ("result of & must appear in exactly one output list",
-               N, Spec_Id);
+              ("result of & must appear in exactly one output list (SPARK RM "
+               & "6.1.5(10))", N, Spec_Id);
          end if;
       end Check_Function_Return;
 
@@ -952,22 +957,26 @@
          Self_Ref : Boolean)
       is
          procedure Find_Mode
-           (Is_Input  : out Boolean;
-            Is_Output : out Boolean);
+           (Is_Input    : out Boolean;
+            Is_Output   : out Boolean;
+            From_Global : out Boolean);
          --  Find the mode of Item_Id. Flags Is_Input and Is_Output are set
-         --  depending on the mode.
+         --  depending on the mode. Flag From_Global is set when the mode is
+         --  determined by pragma [Refined_]Global.
 
          ---------------
          -- Find_Mode --
          ---------------
 
          procedure Find_Mode
-           (Is_Input  : out Boolean;
-            Is_Output : out Boolean)
+           (Is_Input    : out Boolean;
+            Is_Output   : out Boolean;
+            From_Global : out Boolean)
          is
          begin
-            Is_Input  := False;
-            Is_Output := False;
+            Is_Input    := False;
+            Is_Output   := False;
+            From_Global := False;
 
             --  Abstract state cases
 
@@ -978,28 +987,20 @@
 
                if Global_Seen then
                   if Appears_In (Subp_Inputs, Item_Id) then
-                     Is_Input := True;
+                     Is_Input    := True;
+                     From_Global := True;
                   end if;
 
                   if Appears_In (Subp_Outputs, Item_Id) then
-                     Is_Output := True;
+                     Is_Output   := True;
+                     From_Global := True;
                   end if;
 
-               --  Otherwise the mode of the state is the one defined in pragma
-               --  Abstract_State. An In_Out state lacks both Input_Only and
-               --  Output_Only modes.
+               --  Otherwise the state has a default IN OUT mode
 
-               elsif not Is_Input_Only_State (Item_Id)
-                 and then not Is_Output_Only_State (Item_Id)
-               then
+               else
                   Is_Input  := True;
                   Is_Output := True;
-
-               elsif Is_Input_Only_State (Item_Id) then
-                  Is_Input := True;
-
-               elsif Is_Output_Only_State (Item_Id) then
-                  Is_Output := True;
                end if;
 
             --  Parameter cases
@@ -1048,11 +1049,13 @@
                   if Appears_In (Subp_Inputs, Item_Id)
                     or else Is_Unconstrained_Or_Tagged_Item (Item_Id)
                   then
-                     Is_Input := True;
+                     Is_Input    := True;
+                     From_Global := True;
                   end if;
 
                   if Appears_In (Subp_Outputs, Item_Id) then
-                     Is_Output := True;
+                     Is_Output   := True;
+                     From_Global := True;
                   end if;
 
                --  Otherwise the variable has a default IN OUT mode
@@ -1068,32 +1071,49 @@
 
          Item_Is_Input  : Boolean;
          Item_Is_Output : Boolean;
+         From_Global    : Boolean;
 
       --  Start of processing for Check_Mode
 
       begin
-         Find_Mode (Item_Is_Input, Item_Is_Output);
+         Find_Mode (Item_Is_Input, Item_Is_Output, From_Global);
 
          --  Input item
 
          if Is_Input then
             if not Item_Is_Input then
-               Error_Msg_NE
-                 ("item & must have mode `IN` or `IN OUT`", Item, Item_Id);
+               if From_Global then
+                  Error_Msg_NE
+                    ("item & must have mode `IN` or `IN OUT`", Item, Item_Id);
+               else
+                  Error_Msg_NE
+                    ("item & appears as extra in input list", Item, Item_Id);
+               end if;
             end if;
 
          --  Self-referential item
 
          elsif Self_Ref then
             if not Item_Is_Input or else not Item_Is_Output then
-               Error_Msg_NE ("item & must have mode `IN OUT`", Item, Item_Id);
+               if From_Global then
+                  Error_Msg_NE
+                    ("item & must have mode `IN OUT`", Item, Item_Id);
+               else
+                  Error_Msg_NE
+                    ("item & appears as extra in In_Out list", Item, Item_Id);
+               end if;
             end if;
 
          --  Output item
 
          elsif not Item_Is_Output then
-            Error_Msg_NE
-              ("item & must have mode `OUT` or `IN OUT`", Item, Item_Id);
+            if From_Global then
+               Error_Msg_NE
+                 ("item & must have mode `OUT` or `IN OUT`", Item, Item_Id);
+            else
+               Error_Msg_NE
+                 ("item & appears as extra in output list", Item, Item_Id);
+            end if;
          end if;
       end Check_Mode;
 
@@ -1121,14 +1141,14 @@
 
             if Is_Input then
                Error_Msg_NE
-                 ("item & must appear in at least one input list of aspect "
-                  & "Depends", Item, Item_Id);
+                 ("item & must appear in at least one input dependence list "
+                  & "(SPARK RM 6.1.5(8))", Item, Item_Id);
 
-               --  Case of OUT parameter for which Is_Input is set
+               --  Refine the error message for unconstrained OUT parameters
+               --  by giving the reason for the illegality.
 
-               if Nkind (Item) = N_Defining_Identifier
-                 and then Ekind (Item) = E_Out_Parameter
-               then
+               if Ekind (Item_Id) = E_Out_Parameter then
+
                   --  One case is an unconstrained array where the bounds
                   --  must be read, if we have this case, output a message
                   --  indicating why the OUT parameter is read.
@@ -1167,8 +1187,8 @@
 
             else
                Error_Msg_NE
-                 ("item & must appear in exactly one output list of aspect "
-                  & "Depends", Item, Item_Id);
+                 ("item & must appear in exactly one output dependence list "
+                  & "(SPARK RM 6.1.5(10))", Item, Item_Id);
             end if;
          end Usage_Error;
 
@@ -1375,7 +1395,9 @@
             --  appear in the input list of a relation.
 
             elsif Is_Attribute_Result (Output) then
-               Error_Msg_N ("function result cannot depend on itself", Output);
+               Error_Msg_N
+                 ("function result cannot depend on itself (SPARK RM "
+                  & "6.1.5(10))", Output);
                return;
             end if;
 
@@ -1683,11 +1705,11 @@
       end if;
    end Analyze_Depends_In_Decl_Part;
 
-   -----------------------------------------
-   -- Analyze_External_State_In_Decl_Part --
-   -----------------------------------------
+   --------------------------------------------
+   -- Analyze_External_Property_In_Decl_Part --
+   --------------------------------------------
 
-   procedure Analyze_External_State_In_Decl_Part
+   procedure Analyze_External_Property_In_Decl_Part
      (N        : Node_Id;
       Expr_Val : out Boolean)
    is
@@ -1701,16 +1723,19 @@
       --  The Async / Effective pragmas must apply to a volatile object other
       --  than a formal subprogram parameter.
 
-      if Is_Volatile_Object (Obj) then
+      if Is_SPARK_Volatile_Object (Obj) then
          if Is_Entity_Name (Obj)
            and then Present (Entity (Obj))
            and then Is_Formal (Entity (Obj))
          then
             Error_Msg_N
-              ("external state % cannot apply to a formal parameter", N);
+              ("external property % cannot apply to a formal parameter "
+               & "(SPARK RM 7.1.3(2))", N);
          end if;
       else
-         Error_Msg_N ("external state % must apply to a volatile object", N);
+         Error_Msg_N
+           ("external property % must apply to a volatile object (SPARK RM "
+            & "7.1.3(2))", N);
       end if;
 
       --  Ensure that the expression (if present) is static Boolean. A missing
@@ -1725,10 +1750,11 @@
             Expr_Val := Is_True (Expr_Value (Expr));
          else
             Error_Msg_Name_1 := Pragma_Name (N);
-            Error_Msg_N ("expression of % must be static", Expr);
+            Error_Msg_N
+              ("expression of % must be static (SPARK RM 7.1.2(5))", Expr);
          end if;
       end if;
-   end Analyze_External_State_In_Decl_Part;
+   end Analyze_External_Property_In_Decl_Part;
 
    ---------------------------------
    -- Analyze_Global_In_Decl_Part --
@@ -1833,19 +1859,31 @@
                if Is_Formal (Item_Id) then
                   if Scope (Item_Id) = Spec_Id then
                      Error_Msg_N
-                       ("global item cannot reference formal parameter", Item);
+                       ("global item cannot reference formal parameter "
+                        & "(SPARK RM 6.1.4(6))", Item);
                      return;
                   end if;
 
+               --  A constant cannot act as a global item. Do this check first
+               --  to provide a better error diagnostic.
+
+               elsif Ekind (Item_Id) = E_Constant then
+                  Error_Msg_N
+                    ("global item cannot denote a constant (SPARK RM "
+                     & "6.1.4(7))", Item);
+
                --  The only legal references are those to abstract states and
                --  variables.
 
                elsif not Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
                   Error_Msg_N
-                    ("global item must denote variable or state", Item);
+                    ("global item must denote variable or state (SPARK RM "
+                     & "6.1.4(4))", Item);
                   return;
                end if;
 
+               --  State related checks
+
                if Ekind (Item_Id) = E_Abstract_State then
 
                   --  The state acts as a constituent of some other state.
@@ -1868,9 +1906,27 @@
                   elsif Has_Visible_Refinement (Item_Id) then
                      Error_Msg_NE
                        ("cannot mention state & in global refinement, use its "
-                        & "constituents instead", Item, Item_Id);
+                        & "constituents instead (SPARK RM 6.1.4(8))",
+                        Item, Item_Id);
                      return;
                   end if;
+
+               --  Variable related checks
+
+               else
+                  --  A volatile object with property Effective_Reads set to
+                  --  True must have mode Output or In_Out.
+
+                  if Is_SPARK_Volatile_Object (Item_Id)
+                    and then Effective_Reads_Enabled (Item_Id)
+                    and then Global_Mode = Name_Input
+                  then
+                     Error_Msg_NE
+                       ("volatile global item & with property Effective_Reads "
+                        & "must have mode In_Out or Output (SPARK RM "
+                        & "7.1.3(11))", Item, Item_Id);
+                     return;
+                  end if;
                end if;
 
                --  When the item renames an entire object, replace the item
@@ -1884,38 +1940,12 @@
             --  Some form of illegal construct masquerading as a name
 
             else
-               Error_Msg_N ("global item must denote variable or state", Item);
+               Error_Msg_N
+                 ("global item must denote variable or state (SPARK RM "
+                  & "6.1.4(4))", Item);
                return;
             end if;
 
-            --  At this point we know that the global item is one of the two
-            --  valid choices. Perform mode- and usage-specific checks.
-
-            if Ekind (Item_Id) = E_Abstract_State
-              and then Is_External_State (Item_Id)
-            then
-               --  A global item of mode In_Out or Output cannot denote an
-               --  external Input_Only state.
-
-               if Is_Input_Only_State (Item_Id)
-                 and then Nam_In (Global_Mode, Name_In_Out, Name_Output)
-               then
-                  Error_Msg_N
-                    ("global item of mode In_Out or Output cannot reference "
-                     & "External Input_Only state", Item);
-
-               --  A global item of mode In_Out or Input cannot reference an
-               --  external Output_Only state.
-
-               elsif Is_Output_Only_State (Item_Id)
-                 and then Nam_In (Global_Mode, Name_In_Out, Name_Input)
-               then
-                  Error_Msg_N
-                    ("global item of mode In_Out or Input cannot reference "
-                     & "External Output_Only state", Item);
-               end if;
-            end if;
-
             --  Verify that an output does not appear as an input in an
             --  enclosing subprogram.
 
@@ -1928,19 +1958,20 @@
             --  a standard Ada legality rule.
 
             if SPARK_Mode = On
-              and then Is_Volatile_Object (Item)
+              and then Is_SPARK_Volatile_Object (Item)
               and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
             then
-               Error_Msg_N
-                 ("volatile object cannot act as global item of a function "
-                  & "(SPARK RM 7.1.3(5))", Item);
+               Error_Msg_NE
+                 ("volatile object & cannot act as global item of a function "
+                  & "(SPARK RM 7.1.3(9))", Item, Item_Id);
             end if;
 
             --  The same entity might be referenced through various way. Check
             --  the entity of the item rather than the item itself.
 
             if Contains (Seen, Item_Id) then
-               Error_Msg_N ("duplicate global item", Item);
+               Error_Msg_N
+                 ("duplicate global item (SPARK RM 6.1.4(11))", Item);
 
             --  Add the entity of the current item to the list of processed
             --  items.
@@ -1960,7 +1991,7 @@
          is
          begin
             if Status then
-               Error_Msg_N ("duplicate global mode", Mode);
+               Error_Msg_N ("duplicate global mode (SPARK RM 6.1.4(9))", Mode);
             end if;
 
             Status := True;
@@ -1986,7 +2017,10 @@
             Context := Scope (Subp_Id);
             while Present (Context) and then Context /= Standard_Standard loop
                if Is_Subprogram (Context)
-                 and then Present (Get_Pragma (Context, Pragma_Global))
+                 and then
+                   (Present (Get_Pragma (Context, Pragma_Global))
+                      or else
+                    Present (Get_Pragma (Context, Pragma_Refined_Global)))
                then
                   Collect_Subprogram_Inputs_Outputs
                     (Subp_Id      => Context,
@@ -2001,8 +2035,8 @@
                     and then not Appears_In (Outputs, Item_Id)
                   then
                      Error_Msg_NE
-                       ("global item & cannot have mode In_Out or Output",
-                        Item, Item_Id);
+                       ("global item & cannot have mode In_Out or Output "
+                        & "(SPARK RM 6.1.4(12))", Item, Item_Id);
                      Error_Msg_NE
                        ("\item already appears as input of subprogram &",
                         Item, Context);
@@ -2025,7 +2059,8 @@
          begin
             if Ekind (Spec_Id) = E_Function then
                Error_Msg_N
-                 ("global mode & not applicable to functions", Mode);
+                 ("global mode & is not applicable to functions (SPARK RM "
+                  & "6.1.4(10))", Mode);
             end if;
          end Check_Mode_Restriction_In_Function;
 
@@ -2460,12 +2495,15 @@
                      Error_Msg_Name_1 := Chars (Pack_Id);
                      Error_Msg_NE
                        ("initialization item & must appear in the visible "
-                        & "declarations of package %", Item, Item_Id);
+                        & "declarations of package % (SPARK RM 7.1.5(7))",
+                        Item, Item_Id);
 
                   --  Detect a duplicate use of the same initialization item
 
                   elsif Contains (Items_Seen, Item_Id) then
-                     Error_Msg_N ("duplicate initialization item", Item);
+                     Error_Msg_N
+                       ("duplicate initialization item (SPARK RM 7.1.5(5))",
+                        Item);
 
                   --  The item is legal, add it to the list of processed states
                   --  and variables.
@@ -2479,15 +2517,16 @@
 
                else
                   Error_Msg_N
-                    ("initialization item must denote variable or state",
-                     Item);
+                    ("initialization item must denote variable or state "
+                     & "(SPARK RM 7.1.5(3))", Item);
                end if;
 
             --  Some form of illegal construct masquerading as a name
 
             else
                Error_Msg_N
-                 ("initialization item must denote variable or state", Item);
+                 ("initialization item must denote variable or state (SPARK "
+                  & "RM 7.1.5(3))", Item);
             end if;
          end if;
       end Analyze_Initialization_Item;
@@ -2555,12 +2594,14 @@
                         Error_Msg_Name_1 := Chars (Pack_Id);
                         Error_Msg_NE
                           ("input item & cannot denote a visible variable or "
-                           & "state in package %", Input, Input_Id);
+                           & "state of package % (SPARK RM 7.1.5(4))",
+                           Input, Input_Id);
 
                      --  Detect a duplicate use of the same input item
 
                      elsif Contains (Inputs_Seen, Input_Id) then
-                        Error_Msg_N ("duplicate input item", Input);
+                        Error_Msg_N
+                          ("duplicate input item (SPARK RM 7.1.5(5))", Input);
 
                      --  Input is legal, add it to the list of processed inputs
 
@@ -2677,22 +2718,22 @@
    begin
       Set_Analyzed (N);
 
-      --  Initialize the various lists used during analysis
+      --  Nothing to do when the initialization list is empty
 
-      Collect_States_And_Variables;
-
-      --  All done if result is null
-
       if Nkind (Inits) = N_Null then
          return;
       end if;
 
-      --  Single and multiple initialization clauses must appear as an
-      --  aggregate. If this is not the case, then either the parser or
-      --  the analysis of the pragma failed to produce an aggregate.
+      --  Single and multiple initialization clauses appear as an aggregate. If
+      --  this is not the case, then either the parser or the analysis of the
+      --  pragma failed to produce an aggregate.
 
       pragma Assert (Nkind (Inits) = N_Aggregate);
 
+      --  Initialize the various lists used during analysis
+
+      Collect_States_And_Variables;
+
       if Present (Expressions (Inits)) then
          Init := First (Expressions (Inits));
          while Present (Init) loop
@@ -9674,6 +9715,14 @@
                   Status : in out Boolean);
                --  Flag Status denotes whether a particular option has been
                --  seen while processing a state. This routine verifies that
+               --  Opt is not a duplicate option and sets the flag Status.
+
+               procedure Check_Duplicate_Property
+                 (Prop   : Node_Id;
+                  Status : in out Boolean);
+               --  Flag Status denotes whether a particular property has been
+               --  seen while processing option External. This routine verifies
+               --  that Prop is not a duplicate property and sets flag Status.
                --  Opt is not a duplicate property and sets the flag Status.
 
                -----------------------------
@@ -9802,7 +9851,7 @@
                      else
                         Error_Msg_N
                           ("expression of external state property must be "
-                           & "static", Expr);
+                           & "static (SPARK RM 7.1.2(5))", Expr);
                      end if;
 
                   --  The lack of expression defaults the property to True
@@ -9815,19 +9864,19 @@
 
                   if Nkind (Prop) = N_Identifier then
                      if Chars (Prop) = Name_Async_Readers then
-                        Check_Duplicate_Option (Prop, AR_Seen);
+                        Check_Duplicate_Property (Prop, AR_Seen);
                         AR_Val := Expr_Val;
 
                      elsif Chars (Prop) = Name_Async_Writers then
-                        Check_Duplicate_Option (Prop, AW_Seen);
+                        Check_Duplicate_Property (Prop, AW_Seen);
                         AW_Val := Expr_Val;
 
                      elsif Chars (Prop) = Name_Effective_Reads then
-                        Check_Duplicate_Option (Prop, ER_Seen);
+                        Check_Duplicate_Property (Prop, ER_Seen);
                         ER_Val := Expr_Val;
 
                      else
-                        Check_Duplicate_Option (Prop, EW_Seen);
+                        Check_Duplicate_Property (Prop, EW_Seen);
                         EW_Val := Expr_Val;
                      end if;
 
@@ -9889,12 +9938,31 @@
                is
                begin
                   if Status then
-                     Error_Msg_N ("duplicate state option", Opt);
+                     Error_Msg_N
+                       ("duplicate state option (SPARK RM 7.1.4(1))", Opt);
                   end if;
 
                   Status := True;
                end Check_Duplicate_Option;
 
+               ------------------------------
+               -- Check_Duplicate_Property --
+               ------------------------------
+
+               procedure Check_Duplicate_Property
+                 (Prop   : Node_Id;
+                  Status : in out Boolean)
+               is
+               begin
+                  if Status then
+                     Error_Msg_N
+                       ("duplicate external property (SPARK RM 7.1.4(2))",
+                        Prop);
+                  end if;
+
+                  Status := True;
+               end Check_Duplicate_Property;
+
                --  Local variables
 
                Errors    : constant Nat := Serious_Errors_Detected;
@@ -9960,10 +10028,20 @@
                        and then Chars (Opt) = Name_External
                      then
                         Analyze_External_Option (Opt);
+
+                     --  When an erroneous option Part_Of is without a parent
+                     --  state, it appears in the list of expression of the
+                     --  aggregate rather than the component associations.
+
+                     elsif Chars (Opt) = Name_Part_Of then
+                        Error_Msg_N
+                          ("option Part_Of must denote an abstract state "
+                           & "(SPARK RM 7.1.4(9))", Opt);
+
                      else
                         Error_Msg_N
-                          ("simple option not allowed in state declaration",
-                           Opt);
+                          ("simple option not allowed in state declaration "
+                           & "(SPARK RM 7.1.4(3))", Opt);
                      end if;
 
                      Next (Opt);
@@ -10876,7 +10954,8 @@
             --  If we get here, then the pragma applies to a non-object
             --  construct, issue a generic error.
 
-            Error_Pragma ("pragma % must apply to a volatile object");
+            Error_Pragma
+              ("pragma % must apply to a volatile object (SPARK RM 7.1.3(2))");
          end Async_Effective;
 
          ------------------
@@ -18023,7 +18102,7 @@
             then
                Error_Msg_NE
                  ("useless refinement, package & does not define abstract "
-                  & "states", N, Spec_Id);
+                  & "states (SPARK RM 7.2.2(3))", N, Spec_Id);
                return;
             end if;
 
@@ -20619,12 +20698,12 @@
       Depends      : Node_Id;
       --  The corresponding Depends pragma along with its clauses
 
-      Global : Node_Id := Empty;
-      --  The corresponding Refined_Global pragma (if any)
-
       Out_Items : Elist_Id := No_Elist;
       --  All output items as defined in pragma Refined_Global (if any)
 
+      Ref_Global : Node_Id := Empty;
+      --  The corresponding Refined_Global pragma (if any)
+
       Refinements : List_Id := No_List;
       --  The clauses of pragma Refined_Depends
 
@@ -20649,14 +20728,6 @@
          --  clause Ref_Clause. If flag Do_Checks is set, the routine reports
          --  missed or extra input items.
 
-         function Output_Constituents (State_Id : Entity_Id) return Elist_Id;
-         --  Given a state denoted by State_Id, return a list of all output
-         --  constituents that may be referenced within Refined_Depends. The
-         --  contents of the list depend on whether Refined_Global is present.
-
-         procedure Report_Unused_Constituents (Constits : Elist_Id);
-         --  Emit errors for all constituents found in list Constits
-
          ------------------
          -- Inputs_Match --
          ------------------
@@ -20969,86 +21040,6 @@
             return Result;
          end Inputs_Match;
 
-         -------------------------
-         -- Output_Constituents --
-         -------------------------
-
-         function Output_Constituents (State_Id : Entity_Id) return Elist_Id is
-            Item_Elmt : Elmt_Id;
-            Item_Id   : Entity_Id;
-            Result    : Elist_Id := No_Elist;
-
-         begin
-            --  The related subprogram is subject to pragma Refined_Global. All
-            --  usable output constituents are defined in its output item list.
-
-            if Present (Global) then
-               Item_Elmt := First_Elmt (Out_Items);
-               while Present (Item_Elmt) loop
-                  Item_Id := Node (Item_Elmt);
-
-                  --  The constituent is part of the refinement of the input
-                  --  state, add it to the result list.
-
-                  if Refined_State (Item_Id) = State_Id then
-                     Add_Item (Item_Id, Result);
-                  end if;
-
-                  Next_Elmt (Item_Elmt);
-               end loop;
-
-            --  When pragma Refined_Global is not present, the usable output
-            --  constituents are all the constituents as defined in pragma
-            --  Refined_State. Note that the elements are copied because the
-            --  algorithm trims the list and this should not be reflected in
-            --  the state itself.
-
-            else
-               Result := New_Copy_Elist (Refinement_Constituents (State_Id));
-            end if;
-
-            return Result;
-         end Output_Constituents;
-
-         --------------------------------
-         -- Report_Unused_Constituents --
-         --------------------------------
-
-         procedure Report_Unused_Constituents (Constits : Elist_Id) is
-            Constit : Entity_Id;
-            Elmt    : Elmt_Id;
-            Posted  : Boolean := False;
-
-         begin
-            if Present (Constits) then
-               Elmt := First_Elmt (Constits);
-               while Present (Elmt) loop
-                  Constit := Node (Elmt);
-
-                  --  A constituent must always refine a state
-
-                  pragma Assert (Present (Refined_State (Constit)));
-
-                  --  When a state has a visible refinement and its mode is
-                  --  Output_Only, all its constituents must be used as
-                  --  outputs.
-
-                  if not Posted then
-                     Posted := True;
-                     Error_Msg_NE
-                       ("output only state & must be replaced by all its "
-                        & "constituents in dependence refinement",
-                        N, Refined_State (Constit));
-                  end if;
-
-                  Error_Msg_NE
-                    ("\  constituent & is missing in output list", N, Constit);
-
-                  Next_Elmt (Elmt);
-               end loop;
-            end if;
-         end Report_Unused_Constituents;
-
          --  Local variables
 
          Dep_Output      : constant Node_Id := First (Choices (Dep_Clause));
@@ -21071,10 +21062,6 @@
          --  Flag set when the output of clause Dep_Clause is a state with
          --  visible refinement.
 
-         Out_Constits : Elist_Id := No_Elist;
-         --  This list contains the entities all output constituents of state
-         --  Dep_Id as defined in pragma Refined_State.
-
       --  Start of processing for Check_Dependency_Clause
 
       begin
@@ -21177,15 +21164,6 @@
                   elsif Has_Non_Null_Refinement (Dep_Id) then
                      Has_Refined_State := True;
 
-                     --  Store the entities of all output constituents of an
-                     --  Output_Only state with visible refinement.
-
-                     if No (Out_Constits)
-                       and then Is_Output_Only_State (Dep_Id)
-                     then
-                        Out_Constits := Output_Constituents (Dep_Id);
-                     end if;
-
                      if Is_Entity_Name (Ref_Output) then
                         Ref_Id := Entity_Of (Ref_Output);
 
@@ -21204,12 +21182,6 @@
                         then
                            Has_Constituent := True;
                            Remove (Ref_Clause);
-
-                           --  The matching constituent may act as an output
-                           --  for an Output_Only state. Remove the item from
-                           --  the available output constituents.
-
-                           Remove (Out_Constits, Ref_Id);
                         end if;
                      end if;
 
@@ -21296,11 +21268,6 @@
                   Ref_Clause);
             end if;
          end if;
-
-         --  Emit errors for all unused constituents of an Output_Only state
-         --  with visible refinement.
-
-         Report_Unused_Constituents (Out_Constits);
       end Check_Dependency_Clause;
 
       --------------------------
@@ -21343,8 +21310,8 @@
       --  The following are dummy variables that capture unused output of
       --  routine Collect_Global_Items.
 
-      D1, D2         : Elist_Id := No_Elist;
-      D3, D4, D5, D6 : Boolean;
+      D1, D2, D3         : Elist_Id := No_Elist;
+      D4, D5, D6, D7, D8 : Boolean;
 
    --  Start of processing for Analyze_Refined_Depends_In_Decl_Part
 
@@ -21357,8 +21324,8 @@
 
       if No (Depends) then
          Error_Msg_NE
-           ("useless refinement, subprogram & lacks dependence clauses",
-            N, Spec_Id);
+           ("useless refinement, subprogram & lacks dependence clauses (SPARK "
+            & "RM 7.2.5(2))", N, Spec_Id);
          return;
       end if;
 
@@ -21371,7 +21338,7 @@
       if Nkind (Deps) = N_Null then
          Error_Msg_NE
            ("useless refinement, subprogram & does not depend on abstract "
-            & "state with visible refinement", N, Spec_Id);
+            & "state with visible refinement (SPARK RM 7.2.5(2))", N, Spec_Id);
          return;
       end if;
 
@@ -21395,18 +21362,20 @@
          --  verifying the use of constituents that apply to output states with
          --  visible refinement.
 
-         Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
+         Ref_Global := Get_Pragma (Body_Id, Pragma_Refined_Global);
 
-         if Present (Global) then
+         if Present (Ref_Global) then
             Collect_Global_Items
-              (Prag             => Global,
-               In_Items         => D1,
-               In_Out_Items     => D2,
-               Out_Items        => Out_Items,
-               Has_In_State     => D3,
-               Has_In_Out_State => D4,
-               Has_Out_State    => D5,
-               Has_Null_State   => D6);
+              (Prag               => Ref_Global,
+               In_Items           => D1,
+               In_Out_Items       => D2,
+               Out_Items          => Out_Items,
+               Proof_In_Items     => D3,
+               Has_In_State       => D4,
+               Has_In_Out_State   => D5,
+               Has_Out_State      => D6,
+               Has_Proof_In_State => D7,
+               Has_Null_State     => D8);
          end if;
 
          if Nkind (Refs) = N_Null then
@@ -21455,29 +21424,32 @@
       Global : Node_Id;
       --  The corresponding Global pragma
 
-      Has_In_State     : Boolean := False;
-      Has_In_Out_State : Boolean := False;
-      Has_Out_State    : Boolean := False;
+      Has_In_State       : Boolean := False;
+      Has_In_Out_State   : Boolean := False;
+      Has_Out_State      : Boolean := False;
+      Has_Proof_In_State : Boolean := False;
       --  These flags are set when the corresponding Global pragma has a state
-      --  of mode Input, In_Out and Output respectively with a visible
+      --  of mode Input, In_Out, Output or Proof_In respectively with a visible
       --  refinement.
 
       Has_Null_State : Boolean := False;
       --  This flag is set when the corresponding Global pragma has at least
       --  one state with a null refinement.
 
-      In_Constits     : Elist_Id := No_Elist;
-      In_Out_Constits : Elist_Id := No_Elist;
-      Out_Constits    : Elist_Id := No_Elist;
-      --  These lists contain the entities of all Input, In_Out and Output
-      --  constituents that appear in Refined_Global and participate in state
-      --  refinement.
+      In_Constits       : Elist_Id := No_Elist;
+      In_Out_Constits   : Elist_Id := No_Elist;
+      Out_Constits      : Elist_Id := No_Elist;
+      Proof_In_Constits : Elist_Id := No_Elist;
+      --  These lists contain the entities of all Input, In_Out, Output and
+      --  Proof_In constituents that appear in Refined_Global and participate
+      --  in state refinement.
 
-      In_Items     : Elist_Id := No_Elist;
-      In_Out_Items : Elist_Id := No_Elist;
-      Out_Items    : Elist_Id := No_Elist;
-      --  These list contain the entities of all Input, In_Out and Output items
-      --  defined in the corresponding Global pragma.
+      In_Items       : Elist_Id := No_Elist;
+      In_Out_Items   : Elist_Id := No_Elist;
+      Out_Items      : Elist_Id := No_Elist;
+      Proof_In_Items : Elist_Id := No_Elist;
+      --  These list contain the entities of all Input, In_Out, Output and
+      --  Proof_In items defined in the corresponding Global pragma.
 
       procedure Check_In_Out_States;
       --  Determine whether the corresponding Global pragma mentions In_Out
@@ -21487,23 +21459,30 @@
       --    2) there is at least one Input and one Output constituent
       --    3) not all constituents are present and one of them is of mode
       --       Output.
-      --  This routine may remove elements from In_Constits, In_Out_Constits
-      --  and Out_Constits.
+      --  This routine may remove elements from In_Constits, In_Out_Constits,
+      --  Out_Constits and Proof_In_Constits.
 
       procedure Check_Input_States;
       --  Determine whether the corresponding Global pragma mentions Input
       --  states with visible refinement and if so, ensure that at least one of
       --  its constituents appears as an Input item in Refined_Global.
-      --  This routine may remove elements from In_Constits, In_Out_Constits
-      --  and Out_Constits.
+      --  This routine may remove elements from In_Constits, In_Out_Constits,
+      --  Out_Constits and Proof_In_Constits.
 
       procedure Check_Output_States;
       --  Determine whether the corresponding Global pragma mentions Output
       --  states with visible refinement and if so, ensure that all of its
-      --  constituents appear as Output items in Refined_Global. This routine
-      --  may remove elements from In_Constits, In_Out_Constits and
-      --  Out_Constits.
+      --  constituents appear as Output items in Refined_Global.
+      --  This routine may remove elements from In_Constits, In_Out_Constits,
+      --  Out_Constits and Proof_In_Constits.
 
+      procedure Check_Proof_In_States;
+      --  Determine whether the corresponding Global pragma mentions Proof_In
+      --  states with visible refinement and if so, ensure that at least one of
+      --  its constituents appears as a Proof_In item in Refined_Global.
+      --  This routine may remove elements from In_Constits, In_Out_Constits,
+      --  Out_Constits and Proof_In_Constits.
+
       procedure Check_Refined_Global_List
         (List        : Node_Id;
          Global_Mode : Name_Id := Name_Input);
@@ -21564,6 +21543,16 @@
                elsif Present_Then_Remove (Out_Constits, Constit_Id) then
                   Out_Seen := True;
 
+               --  A Proof_In constituent cannot participate in the completion
+               --  of an Output state.
+
+               elsif Present_Then_Remove (Proof_In_Constits, Constit_Id) then
+                  Error_Msg_Name_1 := Chars (State_Id);
+                  Error_Msg_NE
+                    ("constituent & of state % must have mode Input, In_Out "
+                     & "or Output in global refinement (SPARK RM 7.2.4(5))",
+                     N, Constit_Id);
+
                else
                   Has_Missing := True;
                end if;
@@ -21591,7 +21580,7 @@
             else
                Error_Msg_NE
                  ("global refinement of state & redefines the mode of its "
-                  & "constituents", N, State_Id);
+                  & "constituents (SPARK RM 7.2.4(5))", N, State_Id);
             end if;
          end Check_Constituent_Usage;
 
@@ -21632,7 +21621,8 @@
          procedure Check_Constituent_Usage (State_Id : Entity_Id);
          --  Determine whether at least one constituent of state State_Id with
          --  visible refinement is used and has mode Input. Ensure that the
-         --  remaining constituents do not have In_Out or Output modes.
+         --  remaining constituents do not have In_Out, Output or Proof_In
+         --  modes.
 
          -----------------------------
          -- Check_Constituent_Usage --
@@ -21654,15 +21644,16 @@
                   In_Seen := True;
 
                --  The constituent appears in the global refinement, but has
-               --  mode In_Out or Output.
+               --  mode In_Out, Output or Proof_In.
 
                elsif Present_Then_Remove (In_Out_Constits, Constit_Id)
                  or else Present_Then_Remove (Out_Constits, Constit_Id)
+                 or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
                then
                   Error_Msg_Name_1 := Chars (State_Id);
                   Error_Msg_NE
                     ("constituent & of state % must have mode Input in global "
-                     & "refinement", N, Constit_Id);
+                     & "refinement (SPARK RM 7.2.4(5))", N, Constit_Id);
                end if;
 
                Next_Elmt (Constit_Elmt);
@@ -21724,6 +21715,7 @@
          procedure Check_Constituent_Usage (State_Id : Entity_Id) is
             Constit_Elmt : Elmt_Id;
             Constit_Id   : Entity_Id;
+            Posted       : Boolean := False;
 
          begin
             Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
@@ -21733,14 +21725,32 @@
                if Present_Then_Remove (Out_Constits, Constit_Id) then
                   null;
 
-               else
-                  Remove (In_Constits, Constit_Id);
-                  Remove (In_Out_Constits, Constit_Id);
+               --  The constituent appears in the global refinement, but has
+               --  mode Input, In_Out or Proof_In.
 
+               elsif Present_Then_Remove (In_Constits, Constit_Id)
+                 or else Present_Then_Remove (In_Out_Constits, Constit_Id)
+                 or else Present_Then_Remove (Proof_In_Constits, Constit_Id)
+               then
                   Error_Msg_Name_1 := Chars (State_Id);
                   Error_Msg_NE
                     ("constituent & of state % must have mode Output in "
-                     & "global refinement", N, Constit_Id);
+                     & "global refinement (SPARK RM 7.2.4(5))", N, Constit_Id);
+
+               --  The constituent is altogether missing
+
+               else
+                  if not Posted then
+                     Posted := True;
+                     Error_Msg_NE
+                       ("output state & must be replaced by all its "
+                        & "constituents in global refinement (SPARK RM "
+                        & "7.2.5(3))", N, State_Id);
+                  end if;
+
+                  Error_Msg_NE
+                    ("\  constituent & is missing in output list",
+                     N, Constit_Id);
                end if;
 
                Next_Elmt (Constit_Elmt);
@@ -21777,6 +21787,90 @@
          end if;
       end Check_Output_States;
 
+      ---------------------------
+      -- Check_Proof_In_States --
+      ---------------------------
+
+      procedure Check_Proof_In_States is
+         procedure Check_Constituent_Usage (State_Id : Entity_Id);
+         --  Determine whether at least one constituent of state State_Id with
+         --  visible refinement is used and has mode Proof_In. Ensure that the
+         --  remaining constituents do not have Input, In_Out or Output modes.
+
+         -----------------------------
+         -- Check_Constituent_Usage --
+         -----------------------------
+
+         procedure Check_Constituent_Usage (State_Id : Entity_Id) is
+            Constit_Elmt  : Elmt_Id;
+            Constit_Id    : Entity_Id;
+            Proof_In_Seen : Boolean := False;
+
+         begin
+            Constit_Elmt := First_Elmt (Refinement_Constituents (State_Id));
+            while Present (Constit_Elmt) loop
+               Constit_Id := Node (Constit_Elmt);
+
+               --  At least one of the constituents appears as Proof_In
+
+               if Present_Then_Remove (Proof_In_Constits, Constit_Id) then
+                  Proof_In_Seen := True;
+
+               --  The constituent appears in the global refinement, but has
+               --  mode Input, In_Out or Output.
+
+               elsif Present_Then_Remove (In_Constits, Constit_Id)
+                 or else Present_Then_Remove (In_Out_Constits, Constit_Id)
+                 or else Present_Then_Remove (Out_Constits, Constit_Id)
+               then
+                  Error_Msg_Name_1 := Chars (State_Id);
+                  Error_Msg_NE
+                    ("constituent & of state % must have mode Proof_In in "
+                     & "global refinement (SPARK RM 7.2.4(5))", N, Constit_Id);
+               end if;
+
+               Next_Elmt (Constit_Elmt);
+            end loop;
+
+            --  Not one of the constituents appeared as Proof_In
+
+            if not Proof_In_Seen then
+               Error_Msg_NE
+                 ("global refinement of state & must include at least one "
+                  & "constituent of mode Proof_In", N, State_Id);
+            end if;
+         end Check_Constituent_Usage;
+
+         --  Local variables
+
+         Item_Elmt : Elmt_Id;
+         Item_Id   : Entity_Id;
+
+      --  Start of processing for Check_Proof_In_States
+
+      begin
+         --  Inspect the Proof_In items of the corresponding Global pragma
+         --  looking for a state with a visible refinement.
+
+         if Has_Proof_In_State and then Present (Proof_In_Items) then
+            Item_Elmt := First_Elmt (Proof_In_Items);
+            while Present (Item_Elmt) loop
+               Item_Id := Node (Item_Elmt);
+
+               --  Ensure that at least one of the constituents is utilized and
+               --  is of mode Proof_In
+
+               if Ekind (Item_Id) = E_Abstract_State
+                 and then Has_Non_Null_Refinement (Item_Id)
+               then
+                  Check_Constituent_Usage (Item_Id);
+               end if;
+
+               Next_Elmt (Item_Elmt);
+            end loop;
+         end if;
+      end Check_Proof_In_States;
+
       -------------------------------
       -- Check_Refined_Global_List --
       -------------------------------
@@ -21836,6 +21930,9 @@
 
                elsif Global_Mode = Name_Output then
                   Add_Item (Item_Id, Out_Constits);
+
+               elsif Global_Mode = Name_Proof_In then
+                  Add_Item (Item_Id, Proof_In_Constits);
                end if;
 
             --  When not a constituent, ensure that both occurrences of the
@@ -21856,11 +21953,15 @@
                   Inconsistent_Mode_Error (Name_Output);
                end if;
 
+            elsif Contains (Proof_In_Items, Item_Id) then
+               null;
+
             --  The item does not appear in the corresponding Global pragma, it
             --  must be an extra.
 
             else
-               Error_Msg_NE ("extra global item &", Item, Item_Id);
+               Error_Msg_NE
+                 ("extra global item & (SPARK RM 7.2.4(3))", Item, Item_Id);
             end if;
          end Check_Refined_Global_Item;
 
@@ -21981,6 +22082,7 @@
          Report_Extra_Constituents_In_List (In_Constits);
          Report_Extra_Constituents_In_List (In_Out_Constits);
          Report_Extra_Constituents_In_List (Out_Constits);
+         Report_Extra_Constituents_In_List (Proof_In_Constits);
       end Report_Extra_Constituents;
 
       --  Local variables
@@ -22008,14 +22110,16 @@
       --  Extract all relevant items from the corresponding Global pragma
 
       Collect_Global_Items
-        (Prag             => Global,
-         In_Items         => In_Items,
-         In_Out_Items     => In_Out_Items,
-         Out_Items        => Out_Items,
-         Has_In_State     => Has_In_State,
-         Has_In_Out_State => Has_In_Out_State,
-         Has_Out_State    => Has_Out_State,
-         Has_Null_State   => Has_Null_State);
+        (Prag               => Global,
+         In_Items           => In_Items,
+         In_Out_Items       => In_Out_Items,
+         Out_Items          => Out_Items,
+         Proof_In_Items     => Proof_In_Items,
+         Has_In_State       => Has_In_State,
+         Has_In_Out_State   => Has_In_Out_State,
+         Has_Out_State      => Has_Out_State,
+         Has_Proof_In_State => Has_Proof_In_State,
+         Has_Null_State     => Has_Null_State);
 
       --  The corresponding Global pragma must mention at least one state with
       --  a visible refinement at the point Refined_Global is processed. States
@@ -22024,6 +22128,7 @@
       if not Has_In_State
         and then not Has_In_Out_State
         and then not Has_Out_State
+        and then not Has_Proof_In_State
         and then not Has_Null_State
       then
          Error_Msg_NE
@@ -22040,7 +22145,8 @@
         and then
           (Present (In_Items)
             or else Present (In_Out_Items)
-            or else Present (Out_Items))
+            or else Present (Out_Items)
+            or else Present (Proof_In_Items))
         and then not Has_Null_State
       then
          Error_Msg_NE
@@ -22083,6 +22189,13 @@
          Check_Output_States;
       end if;
 
+      --  For Proof_In states with visible refinement, at least one constituent
+      --  must be used as Proof_In in the global refinement.
+
+      if Serious_Errors_Detected = Errors then
+         Check_Proof_In_States;
+      end if;
+
       --  Emit errors for all constituents that belong to other states with
       --  visible refinement that do not appear in Global.
 
@@ -22275,7 +22388,8 @@
                Error_Msg_Name_1 := Chars (Spec_Id);
                Error_Msg_NE
                  ("cannot use & in refinement, constituent is not a hidden "
-                  & "state of package %", Constit, Constit_Id);
+                  & "state of package % (SPARK RM 7.2.2(9))",
+                  Constit, Constit_Id);
             end Check_Matching_Constituent;
 
             --  Local variables
@@ -22335,8 +22449,8 @@
 
                   else
                      Error_Msg_NE
-                       ("constituent & must denote a variable or state",
-                        Constit, Constit_Id);
+                       ("constituent & must denote a variable or state (SPARK "
+                        & "RM 7.2.2(5))", Constit, Constit_Id);
                   end if;
 
                --  The constituent is illegal
@@ -22362,7 +22476,8 @@
 
             if Contains (Refined_States_Seen, State_Id) then
                Error_Msg_NE
-                 ("duplicate refinement of state &", State, State_Id);
+                 ("duplicate refinement of state & (SPARK RM 7.2.2(8))",
+                  State, State_Id);
                return;
             end if;
 
@@ -22432,25 +22547,28 @@
                        ("& must denote an abstract state", State, State_Id);
                   end if;
 
-                  --  Enforce SPARK RM (6.1.5(4)): A global item shall not
-                  --  denote a state abstraction whose refinement is visible
-                  --  (a state abstraction cannot be named within its enclosing
-                  --  package's body other than in its refinement).
+                  --  A global item cannot denote a state abstraction whose
+                  --  refinement is visible, in other words a state abstraction
+                  --  cannot be named within its enclosing package's body other
+                  --  than in its refinement.
 
                   if Has_Body_References (State_Id) then
                      declare
-                        Ref : Elmt_Id;
-                        Nod : Node_Id;
+                        Ref      : Node_Id;
+                        Ref_Elmt : Elmt_Id;
+
                      begin
-                        Ref := First_Elmt (Body_References (State_Id));
-                        while Present (Ref) loop
-                           Nod := Node (Ref);
+                        Ref_Elmt := First_Elmt (Body_References (State_Id));
+                        while Present (Ref_Elmt) loop
+                           Ref := Node (Ref_Elmt);
+
                            Error_Msg_N
-                             ("global reference to & not allowed "
-                              & "(SPARK RM 6.1.5(4))", Nod);
+                             ("global reference to & not allowed (SPARK RM "
+                              & "6.1.4(8))", Ref);
                            Error_Msg_Sloc := Sloc (State);
-                           Error_Msg_N ("\refinement of & is visible#", Nod);
-                           Next_Elmt (Ref);
+                           Error_Msg_N ("\refinement of & is visible#", Ref);
+
+                           Next_Elmt (Ref_Elmt);
                         end loop;
                      end;
                   end if;
@@ -22783,7 +22901,8 @@
 
       else
          Error_Msg_N
-           ("illegal combination of external state properties", Item);
+           ("illegal combination of external properties (SPARK RM 7.1.2(6))",
+            Item);
       end if;
    end Check_External_Properties;
 
@@ -22927,14 +23046,16 @@
    --------------------------
 
    procedure Collect_Global_Items
-     (Prag             : Node_Id;
-      In_Items         : in out Elist_Id;
-      In_Out_Items     : in out Elist_Id;
-      Out_Items        : in out Elist_Id;
-      Has_In_State     : out Boolean;
-      Has_In_Out_State : out Boolean;
-      Has_Out_State    : out Boolean;
-      Has_Null_State   : out Boolean)
+     (Prag               : Node_Id;
+      In_Items           : in out Elist_Id;
+      In_Out_Items       : in out Elist_Id;
+      Out_Items          : in out Elist_Id;
+      Proof_In_Items     : in out Elist_Id;
+      Has_In_State       : out Boolean;
+      Has_In_Out_State   : out Boolean;
+      Has_Out_State      : out Boolean;
+      Has_Proof_In_State : out Boolean;
+      Has_Null_State     : out Boolean)
    is
       procedure Process_Global_List
         (List : Node_Id;
@@ -22979,6 +23100,8 @@
                      Has_In_Out_State := True;
                   elsif Mode = Name_Output then
                      Has_Out_State := True;
+                  elsif Mode = Name_Proof_In then
+                     Has_Proof_In_State := True;
                   end if;
                end if;
             end if;
@@ -22991,6 +23114,8 @@
                Add_Item (Item_Id, In_Out_Items);
             elsif Mode = Name_Output then
                Add_Item (Item_Id, Out_Items);
+            elsif Mode = Name_Proof_In then
+               Add_Item (Item_Id, Proof_In_Items);
             end if;
          end Process_Global_Item;
 
@@ -23063,10 +23188,11 @@
    begin
       --  Assume that no states have been encountered
 
-      Has_In_State     := False;
-      Has_In_Out_State := False;
-      Has_Out_State    := False;
-      Has_Null_State   := False;
+      Has_In_State       := False;
+      Has_In_Out_State   := False;
+      Has_Out_State      := False;
+      Has_Proof_In_State := False;
+      Has_Null_State     := False;
 
       Process_Global_List (Items);
    end Collect_Global_Items;
Index: sem_prag.ads
===================================================================
--- sem_prag.ads	(revision 207120)
+++ sem_prag.ads	(working copy)
@@ -60,7 +60,7 @@
    --  Perform full analysis of delayed pragma Depends. This routine is also
    --  capable of performing basic analysis of pragma Refined_Depends.
 
-   procedure Analyze_External_State_In_Decl_Part
+   procedure Analyze_External_Property_In_Decl_Part
      (N        : Node_Id;
       Expr_Val : out Boolean);
    --  Perform full analysis of delayed pragmas Async_Readers, Async_Writers,
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 207120)
+++ sem_ch12.adb	(working copy)
@@ -9846,11 +9846,11 @@
 
       if SPARK_Mode = On
         and then Present (Actual)
-        and then Is_Volatile_Object (Actual)
+        and then Is_SPARK_Volatile_Object (Actual)
       then
          Error_Msg_N
            ("volatile object cannot act as actual in generic instantiation "
-            & "(SPARK RM 7.1.3(4))", Actual);
+            & "(SPARK RM 7.1.3(8))", Actual);
       end if;
 
       return List;
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 207134)
+++ sem_util.adb	(working copy)
@@ -3729,14 +3729,9 @@
          else
             Item_Id := Entity_Of (Item);
 
-            --  Defend against junk
-
-            if No (Item_Id) then
-               return False;
-            end if;
-
             return
-              Ekind (Item_Id) = E_Abstract_State
+              Present (Item_Id)
+                and then Ekind (Item_Id) = E_Abstract_State
                 and then Has_Visible_Refinement (Item_Id);
          end if;
       end Is_Refined_State;
@@ -8097,6 +8092,34 @@
       end if;
    end Has_Tagged_Component;
 
+   ----------------------------
+   -- Has_Volatile_Component --
+   ----------------------------
+
+   function Has_Volatile_Component (Typ : Entity_Id) return Boolean is
+      Comp : Entity_Id;
+
+   begin
+      if Has_Volatile_Components (Typ) then
+         return True;
+
+      elsif Is_Array_Type (Typ) then
+         return Is_Volatile (Component_Type (Typ));
+
+      elsif Is_Record_Type (Typ) then
+         Comp := First_Component (Typ);
+         while Present (Comp) loop
+            if Is_Volatile_Object (Comp) then
+               return True;
+            end if;
+
+            Comp := Next_Component (Comp);
+         end loop;
+      end if;
+
+      return False;
+   end Has_Volatile_Component;
+
    -------------------------
    -- Implementation_Kind --
    -------------------------
@@ -10827,6 +10850,37 @@
       end if;
    end Is_SPARK_Object_Reference;
 
+   ------------------------------
+   -- Is_SPARK_Volatile_Object --
+   ------------------------------
+
+   function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
+   begin
+      if Nkind (N) = N_Defining_Identifier then
+         return Is_Volatile (N) or else Is_Volatile (Etype (N));
+
+      elsif Is_Entity_Name (N) then
+         return
+           Is_SPARK_Volatile_Object (Entity (N))
+             or else Is_Volatile (Etype (N));
+
+      elsif Nkind (N) = N_Expanded_Name then
+         return Is_SPARK_Volatile_Object (Entity (N));
+
+      elsif Nkind (N) = N_Indexed_Component then
+         return Is_SPARK_Volatile_Object (Prefix (N));
+
+      elsif Nkind (N) = N_Selected_Component then
+         return
+           Is_SPARK_Volatile_Object (Prefix (N))
+             or else
+           Is_SPARK_Volatile_Object (Selector_Name (N));
+
+      else
+         return False;
+      end if;
+   end Is_SPARK_Volatile_Object;
+
    ------------------
    -- Is_Statement --
    ------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads	(revision 207134)
+++ sem_util.ads	(working copy)
@@ -886,6 +886,10 @@
    --  component is present. This function is used to check if "=" has to be
    --  expanded into a bunch component comparisons.
 
+   function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
+   --  Given an arbitrary type, determine whether it contains at least one
+   --  volatile component.
+
    function Implementation_Kind (Subp : Entity_Id) return Name_Id;
    --  Subp is a subprogram marked with pragma Implemented. Return the specific
    --  implementation requirement which the pragma imposes. The return value is
@@ -1015,6 +1019,11 @@
    --  First determine whether type T is an interface and then check whether
    --  it is of protected, synchronized or task kind.
 
+   function Is_Delegate (T : Entity_Id) return Boolean;
+   --  Returns true if type T represents a delegate. A Delegate is the CIL
+   --  object used to represent access-to-subprogram types. This is only
+   --  relevant to CIL, will always return false for other targets.
+
    function Is_Dependent_Component_Of_Mutable_Object
      (Object : Node_Id) return Boolean;
    --  Returns True if Object is the name of a subcomponent that depends on
@@ -1165,6 +1174,13 @@
    function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
    --  Determines if the tree referenced by N represents an object in SPARK
 
+   function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
+   --  Determine whether an arbitrary node denotes a volatile object reference
+   --  according to the semantics of SPARK. To qualify as volatile, an object
+   --  must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
+   --  subject to the same attributes. Note that volatile components do not
+   --  render an object volatile.
+
    function Is_Statement (N : Node_Id) return Boolean;
    pragma Inline (Is_Statement);
    --  Check if the node N is a statement node. Note that this includes
@@ -1215,11 +1231,6 @@
    --  Determine whether an operator is one of the intrinsics defined
    --  in the DEC system extension.
 
-   function Is_Delegate (T : Entity_Id) return Boolean;
-   --  Returns true if type T represents a delegate. A Delegate is the CIL
-   --  object used to represent access-to-subprogram types. This is only
-   --  relevant to CIL, will always return false for other targets.
-
    function Is_Variable
      (N                 : Node_Id;
       Use_Original_Node : Boolean := True) return Boolean;
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 207120)
+++ sem_res.adb	(working copy)
@@ -4041,6 +4041,16 @@
                then
                   Apply_Discriminant_Check (A, F_Typ);
 
+                  --  For view conversions of a discriminated object, apply
+                  --  check to object itself, the conversion alreay has the
+                  --  proper type.
+
+                  if Nkind (A) = N_Type_Conversion
+                    and then Is_Constrained (Etype (Expression (A)))
+                  then
+                     Apply_Discriminant_Check (Expression (A), F_Typ);
+                  end if;
+
                elsif Is_Access_Type (F_Typ)
                  and then Is_Array_Type (Designated_Type (F_Typ))
                  and then Is_Constrained (Designated_Type (F_Typ))
@@ -4254,7 +4264,7 @@
             --  they are not standard Ada legality rule.
 
             if SPARK_Mode = On
-              and then Is_Volatile_Object (A)
+              and then Is_SPARK_Volatile_Object (A)
             then
                --  A volatile object may act as an actual parameter when the
                --  corresponding formal is of a non-scalar volatile type.
@@ -4273,7 +4283,7 @@
                else
                   Error_Msg_N
                     ("volatile object cannot act as actual in a call (SPARK "
-                     & "RM 7.1.3(8))", A);
+                     & "RM 7.1.3(12))", A);
                end if;
             end if;
 
@@ -6497,8 +6507,7 @@
       --  standard Ada legality rules.
 
       if SPARK_Mode = On
-        and then Ekind (E) = E_Variable
-        and then Is_Volatile_Object (E)
+        and then Is_SPARK_Volatile_Object (E)
         and then
           (Async_Writers_Enabled (E)
              or else Effective_Reads_Enabled (E))
@@ -6555,7 +6564,7 @@
          if not Usage_OK then
             Error_Msg_N
               ("volatile object cannot appear in this context (SPARK RM "
-               & "7.1.3(9))", N);
+               & "7.1.3(13))", N);
          end if;
       end if;
    end Resolve_Entity_Name;
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 207120)
+++ exp_ch6.adb	(working copy)
@@ -9477,7 +9477,7 @@
       --          <postconditions from body>
       --          <postconditions from spec>
       --          <inherited postconditions>
-      --          <contract cases>
+      --          <contract case consequences>
       --          <invariant check of function result (if applicable)>
       --          <invariant and predicate checks of parameters>
       --       end _Postconditions;
@@ -9486,6 +9486,7 @@
       --       <preconditions from spec>
       --       <preconditions from body>
       --       <refined preconditions from body>
+      --       <contract case conditions>
 
       --       <source declarations>
       --    begin
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 207120)
+++ sem_ch6.adb	(working copy)
@@ -11233,17 +11233,26 @@
             Null_Exclusion_Static_Checks (Param_Spec);
          end if;
 
-         --  A function cannot have a volatile formal parameter. The following
-         --  check is relevant when SPARK_Mode is on as it is not a standard
-         --  Ada legality rule.
+         --  The following checks are relevant when SPARK_Mode is on as these
+         --  are not standard Ada legality rules.
 
          if SPARK_Mode = On
-           and then Is_Volatile_Object (Formal)
            and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
          then
-            Error_Msg_N
-              ("function cannot have a volatile formal parameter (SPARK RM "
-               & "7.1.3(6))", Formal);
+            --  A function cannot have a parameter of mode IN OUT or OUT
+
+            if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+               Error_Msg_N
+                 ("function cannot have parameter of mode `OUT` or `IN OUT` "
+                  & "(SPARK RM 6.1)", Formal);
+
+            --  A function cannot have a volatile formal parameter
+
+            elsif Is_SPARK_Volatile_Object (Formal) then
+               Error_Msg_N
+                 ("function cannot have a volatile formal parameter (SPARK RM "
+                  & "7.1.3(10))", Formal);
+            end if;
          end if;
 
       <<Continue>>
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 207120)
+++ snames.ads-tmpl	(working copy)
@@ -724,7 +724,6 @@
    Name_In_Out                         : constant Name_Id := N + $;
    Name_Increases                      : constant Name_Id := N + $;
    Name_Info                           : constant Name_Id := N + $;
-   Name_Input_Only                     : constant Name_Id := N + $;
    Name_Internal                       : constant Name_Id := N + $;
    Name_Link_Name                      : constant Name_Id := N + $;
    Name_Lowercase                      : constant Name_Id := N + $;
@@ -761,7 +760,6 @@
    Name_Non_Volatile                   : constant Name_Id := N + $;
    Name_On                             : constant Name_Id := N + $;
    Name_Optional                       : constant Name_Id := N + $;
-   Name_Output_Only                    : constant Name_Id := N + $;
    Name_Policy                         : constant Name_Id := N + $;
    Name_Parameter_Types                : constant Name_Id := N + $;
    Name_Part_Of                        : constant Name_Id := N + $;


More information about the Gcc-patches mailing list