2015-10-20 Hristian Kirtchev <kirtchev@adacore.com>

	* aspects.adb Add aspect Volatile_Function to table
	Canonical_Aspect.
	* aspect.ads Add aspect Volatile_Function to tables
	Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names
	and Implementation_Defined_Aspect.  Aspects Async_Readers,
	Async_Writers, Effective_Reads and Effective_Writes are no
	longer Boolean.
	* einfo.adb (Get_Pragma): Add an entry for pragma
	Volatile_Function.
	* par-prag.adb (Prag): Pragma Volatile_Function does not need
	special processing by the parser.
	* rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in
	table RTU_Id. Add an entry for Suspension_Object in table RE_Id.
	* sem_ch3.adb Fix SPARK RM references.
	(Analyze_Object_Contract): Update the error guard.
	* sem_ch5.adb Fix SPARK RM references.
	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure
	that a non-volatile function does not contain an effectively
	volatile parameter.
	(Analyze_Subprogram_Contract): Ensure
	that a non-volatile function does not contain an effectively
	volatile parameter.
	* sem_ch12.adb (Instantiate_Object): Remove the reference to
	the SPARK RM from the error message.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add
	processing for aspects Async_Readers, Async_Writers,
	Effective_Reads, Effective_Writes and Volatile_Function.
	(Check_Aspect_At_Freeze_Point): Aspects Async_Readers,
	Async_Writers, Effective_Reads, Effective_Writes and
	Volatile_Function do not need special processing at the freeze
	point.
	* sem_prag.adb Add an entry for pragma Volatile_Function in
	table Sig_Flags.
	(Analyze_External_Property_In_Decl_Part):
	Reimplemented as Async_Readers, Async_Writers, Effective_Reads
	and Effective_Writes are no longer Boolean pragmas.
	(Analyze_Global_Item): An external state or effectively
	volatile object cannot appear as an item in pragma
	[Refined_]Global.
	(Analyze_Pragma): Change the implementation
	of Async_Readers, Async_Writers, Effective_Reads and
	Effective_Writes as these are no longer Boolean pragmas.
	Use routine Check_Static_Boolean_Expression to verify the
	optional Boolean expression of Async_Readers, Async_Writers,
	Constant_After_Elaboration, Effective_Reads, Effective_Writes,
	Extensions_Visible and Volatile_Function.  Add processing for
	pragma Volatile_Function.
	(Check_Static_Boolean_Expression): New routine.
	(Find_Related_Context): Update the comment on usage.
	(Is_Enabled_Pragma): New routine.
	* sem_prag.ads (Is_Enabled_Pragma): New routine.
	* sem_res.adb Fix SPARK RM references.
	(Is_OK_Volatile_Context): Add detection for return statements.
	(Resolve_Actuals): Remove the check concerning an effectively volatile
	OUT actual parameter as this is now done by the SPARK flow analyzer.
	(Resolve_Entity_Name): Remove the check concerning an effectively
	volatile OUT formal parameter as this is now done by the SPARK
	flow analyzer.	(Within_Volatile_Function): New routine.
	* sem_util.adb (Add_Contract_Item): Add processing for pragma
	Volatile_Function.
	(Check_Nonvolatile_Function_Profile): New routine.
	(Is_Descendant_Of_Suspension_Object): New routine.
	(Is_Effectively_Volatile): Protected types and descendants of
	Suspension_Object are now treated as effectively volatile.
	(Is_Enabled): The optional Boolean expression of pragmas
	Async_Readers, Async_Writers, Effective_Reads and Effective_Writes
	now appears as the first argument.
	(Is_Volatile_Function): New routine.
	* sem_util.ads Add SPARK RM references.
	(Add_Contract_Item): Update the comment on usage.
	(Check_Nonvolatile_Function_Profile): New routine.
	(Is_Effectively_Volatile): Update the comment on usage.
	(Is_Volatile_Function): New routine.
	* snames.ads-tmpl Add a predefined name and pragma id for
	Volatile_Function.

From-SVN: r229047

17 files changed, 717 insertions, 243 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index db9d215..1278c0a 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,81 @@
+2015-10-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb Add aspect Volatile_Function to table
+	Canonical_Aspect.
+	* aspect.ads Add aspect Volatile_Function to tables
+	Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names
+	and Implementation_Defined_Aspect.  Aspects Async_Readers,
+	Async_Writers, Effective_Reads and Effective_Writes are no
+	longer Boolean.
+	* einfo.adb (Get_Pragma): Add an entry for pragma
+	Volatile_Function.
+	* par-prag.adb (Prag): Pragma Volatile_Function does not need
+	special processing by the parser.
+	* rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in
+	table RTU_Id. Add an entry for Suspension_Object in table RE_Id.
+	* sem_ch3.adb Fix SPARK RM references.
+	(Analyze_Object_Contract): Update the error guard.
+	* sem_ch5.adb Fix SPARK RM references.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure
+	that a non-volatile function does not contain an effectively
+	volatile parameter.
+	(Analyze_Subprogram_Contract): Ensure
+	that a non-volatile function does not contain an effectively
+	volatile parameter.
+	* sem_ch12.adb (Instantiate_Object): Remove the reference to
+	the SPARK RM from the error message.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add
+	processing for aspects Async_Readers, Async_Writers,
+	Effective_Reads, Effective_Writes and Volatile_Function.
+	(Check_Aspect_At_Freeze_Point): Aspects Async_Readers,
+	Async_Writers, Effective_Reads, Effective_Writes and
+	Volatile_Function do not need special processing at the freeze
+	point.
+	* sem_prag.adb Add an entry for pragma Volatile_Function in
+	table Sig_Flags.
+	(Analyze_External_Property_In_Decl_Part):
+	Reimplemented as Async_Readers, Async_Writers, Effective_Reads
+	and Effective_Writes are no longer Boolean pragmas.
+	(Analyze_Global_Item): An external state or effectively
+	volatile object cannot appear as an item in pragma
+	[Refined_]Global.
+	(Analyze_Pragma): Change the implementation
+	of Async_Readers, Async_Writers, Effective_Reads and
+	Effective_Writes as these are no longer Boolean pragmas.
+	Use routine Check_Static_Boolean_Expression to verify the
+	optional Boolean expression of Async_Readers, Async_Writers,
+	Constant_After_Elaboration, Effective_Reads, Effective_Writes,
+	Extensions_Visible and Volatile_Function.  Add processing for
+	pragma Volatile_Function.
+	(Check_Static_Boolean_Expression): New routine.
+	(Find_Related_Context): Update the comment on usage.
+	(Is_Enabled_Pragma): New routine.
+	* sem_prag.ads (Is_Enabled_Pragma): New routine.
+	* sem_res.adb Fix SPARK RM references.
+	(Is_OK_Volatile_Context): Add detection for return statements.
+	(Resolve_Actuals): Remove the check concerning an effectively volatile
+	OUT actual parameter as this is now done by the SPARK flow analyzer.
+	(Resolve_Entity_Name): Remove the check concerning an effectively
+	volatile OUT formal parameter as this is now done by the SPARK
+	flow analyzer.	(Within_Volatile_Function): New routine.
+	* sem_util.adb (Add_Contract_Item): Add processing for pragma
+	Volatile_Function.
+	(Check_Nonvolatile_Function_Profile): New routine.
+	(Is_Descendant_Of_Suspension_Object): New routine.
+	(Is_Effectively_Volatile): Protected types and descendants of
+	Suspension_Object are now treated as effectively volatile.
+	(Is_Enabled): The optional Boolean expression of pragmas
+	Async_Readers, Async_Writers, Effective_Reads and Effective_Writes
+	now appears as the first argument.
+	(Is_Volatile_Function): New routine.
+	* sem_util.ads Add SPARK RM references.
+	(Add_Contract_Item): Update the comment on usage.
+	(Check_Nonvolatile_Function_Profile): New routine.
+	(Is_Effectively_Volatile): Update the comment on usage.
+	(Is_Volatile_Function): New routine.
+	* snames.ads-tmpl Add a predefined name and pragma id for
+	Volatile_Function.
+
 2015-10-20  Arnaud Charlet  <charlet@adacore.com>
 
 	* gnat_ugn.texi, gnat_rm.texi: Regenerate.
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index b945a8b..3fc2049 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -610,6 +610,7 @@ package body Aspects is
     Aspect_Volatile                     => Aspect_Volatile,
     Aspect_Volatile_Components          => Aspect_Volatile_Components,
     Aspect_Volatile_Full_Access         => Aspect_Volatile_Full_Access,
+    Aspect_Volatile_Function            => Aspect_Volatile_Function,
     Aspect_Warnings                     => Aspect_Warnings,
     Aspect_Write                        => Aspect_Write);
 
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 2d71394..8b7fca8 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -78,6 +78,8 @@ package Aspects is
       Aspect_Address,
       Aspect_Alignment,
       Aspect_Annotate,                      -- GNAT
+      Aspect_Async_Readers,                 -- GNAT
+      Aspect_Async_Writers,                 -- GNAT
       Aspect_Attach_Handler,
       Aspect_Bit_Order,
       Aspect_Component_Size,
@@ -96,6 +98,8 @@ package Aspects is
       Aspect_Dimension_System,              -- GNAT
       Aspect_Dispatching_Domain,
       Aspect_Dynamic_Predicate,
+      Aspect_Effective_Reads,               -- GNAT
+      Aspect_Effective_Writes,              -- GNAT
       Aspect_Extensions_Visible,            -- GNAT
       Aspect_External_Name,
       Aspect_External_Tag,
@@ -145,6 +149,7 @@ package Aspects is
       Aspect_Unsuppress,
       Aspect_Value_Size,                    -- GNAT
       Aspect_Variable_Indexing,
+      Aspect_Volatile_Function,             -- GNAT
       Aspect_Warnings,                      -- GNAT
       Aspect_Write,
 
@@ -167,15 +172,11 @@ package Aspects is
       --  the aspect value is inherited from the parent, in which case, we do
       --  not allow False if we inherit a True value from the parent.
 
-      Aspect_Async_Readers,                 -- GNAT
-      Aspect_Async_Writers,                 -- GNAT
       Aspect_Asynchronous,
       Aspect_Atomic,
       Aspect_Atomic_Components,
       Aspect_Disable_Controlled,            -- GNAT
       Aspect_Discard_Names,
-      Aspect_Effective_Reads,               -- GNAT
-      Aspect_Effective_Writes,              -- GNAT
       Aspect_Export,
       Aspect_Favor_Top_Level,               -- GNAT
       Aspect_Independent,
@@ -264,6 +265,7 @@ package Aspects is
       Aspect_Unreferenced               => True,
       Aspect_Unreferenced_Objects       => True,
       Aspect_Value_Size                 => True,
+      Aspect_Volatile_Function          => True,
       Aspect_Warnings                   => True,
       others                            => False);
 
@@ -291,7 +293,7 @@ package Aspects is
    --  aspect is enabled. If it is False, the aspect is disabled.
 
    subtype Boolean_Aspects is
-     Aspect_Id range Aspect_Async_Readers .. Aspect_Id'Last;
+     Aspect_Id range Aspect_Asynchronous .. Aspect_Id'Last;
 
    subtype Pre_Post_Aspects is
      Aspect_Id range Aspect_Post .. Aspect_Precondition;
@@ -312,6 +314,8 @@ package Aspects is
       Aspect_Address                    => Expression,
       Aspect_Alignment                  => Expression,
       Aspect_Annotate                   => Expression,
+      Aspect_Async_Readers              => Optional_Expression,
+      Aspect_Async_Writers              => Optional_Expression,
       Aspect_Attach_Handler             => Expression,
       Aspect_Bit_Order                  => Expression,
       Aspect_Component_Size             => Expression,
@@ -330,6 +334,8 @@ package Aspects is
       Aspect_Dimension_System           => Expression,
       Aspect_Dispatching_Domain         => Expression,
       Aspect_Dynamic_Predicate          => Expression,
+      Aspect_Effective_Reads            => Optional_Expression,
+      Aspect_Effective_Writes           => Optional_Expression,
       Aspect_Extensions_Visible         => Optional_Expression,
       Aspect_External_Name              => Expression,
       Aspect_External_Tag               => Expression,
@@ -379,6 +385,7 @@ package Aspects is
       Aspect_Unsuppress                 => Name,
       Aspect_Value_Size                 => Expression,
       Aspect_Variable_Indexing          => Name,
+      Aspect_Volatile_Function          => Optional_Expression,
       Aspect_Warnings                   => Name,
       Aspect_Write                      => Name,
 
@@ -511,6 +518,7 @@ package Aspects is
       Aspect_Volatile                     => Name_Volatile,
       Aspect_Volatile_Components          => Name_Volatile_Components,
       Aspect_Volatile_Full_Access         => Name_Volatile_Full_Access,
+      Aspect_Volatile_Function            => Name_Volatile_Function,
       Aspect_Warnings                     => Name_Warnings,
       Aspect_Write                        => Name_Write);
 
@@ -731,6 +739,7 @@ package Aspects is
       Aspect_Synchronization              => Never_Delay,
       Aspect_Test_Case                    => Never_Delay,
       Aspect_Unimplemented                => Never_Delay,
+      Aspect_Volatile_Function            => Never_Delay,
       Aspect_Warnings                     => Never_Delay,
 
       Aspect_Alignment                    => Rep_Aspect,
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 4e5d083..5adc28f 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -7000,7 +7000,8 @@ package body Einfo is
                  Id = Pragma_Part_Of                    or else
                  Id = Pragma_Refined_Depends            or else
                  Id = Pragma_Refined_Global             or else
-                 Id = Pragma_Refined_State;
+                 Id = Pragma_Refined_State              or else
+                 Id = Pragma_Volatile_Function;
 
       --  Contract / test case pragmas
 
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index bcb8add..a3ed732 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1486,6 +1486,7 @@ begin
            Pragma_Volatile                       |
            Pragma_Volatile_Components            |
            Pragma_Volatile_Full_Access           |
+           Pragma_Volatile_Function              |
            Pragma_Warning_As_Error               |
            Pragma_Weak_External                  |
            Pragma_Validity_Checks                =>
diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads
index af2b675..22f9390 100644
--- a/gcc/ada/rtsfind.ads
+++ b/gcc/ada/rtsfind.ads
@@ -23,15 +23,15 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Types; use Types;
-
-package Rtsfind is
-
 --  This package contains the routine that is used to obtain runtime library
 --  entities, loading in the required runtime library packages on demand. It
 --  is also used for such purposes as finding System.Address when System has
 --  not been explicitly With'ed.
 
+with Types; use Types;
+
+package Rtsfind is
+
    ------------------------
    -- Runtime Unit Table --
    ------------------------
@@ -131,6 +131,7 @@ package Rtsfind is
       Ada_Real_Time,
       Ada_Streams,
       Ada_Strings,
+      Ada_Synchronous_Task_Control,
       Ada_Tags,
       Ada_Task_Identification,
       Ada_Task_Termination,
@@ -606,6 +607,8 @@ package Rtsfind is
 
      RE_Unbounded_String,                -- Ada.Strings.Unbounded
 
+     RE_Suspension_Object,               -- Ada.Synchronous_Task_Control
+
      RE_Access_Level,                    -- Ada.Tags
      RE_Alignment,                       -- Ada.Tags
      RE_Address_Array,                   -- Ada.Tags
@@ -1837,6 +1840,8 @@ package Rtsfind is
 
      RE_Unbounded_String                 => Ada_Strings_Unbounded,
 
+     RE_Suspension_Object                => Ada_Synchronous_Task_Control,
+
      RE_Access_Level                     => Ada_Tags,
      RE_Alignment                        => Ada_Tags,
      RE_Address_Array                    => Ada_Tags,
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index ba0daa9..beb6757 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -5318,28 +5318,24 @@ package body Sem_Ch12 is
             if Need_Subprogram_Instance_Body (N, Act_Decl_Id) then
                Check_Forward_Instantiation (Gen_Decl);
 
-               --  The wrapper package is always delayed, because it does not
-               --  constitute a freeze point, but to insure that the freeze
-               --  node is placed properly, it is created directly when
-               --  instantiating the body (otherwise the freeze node might
-               --  appear to early for nested instantiations).
+            --  The wrapper package is always delayed, because it does not
+            --  constitute a freeze point, but to insure that the freeze node
+            --  is placed properly, it is created directly when instantiating
+            --  the body (otherwise the freeze node might appear to early for
+            --  nested instantiations). For ASIS purposes, indicate that the
+            --  wrapper package has replaced the instantiation node.
 
             elsif Nkind (Parent (N)) = N_Compilation_Unit then
-
-               --  For ASIS purposes, indicate that the wrapper package has
-               --  replaced the instantiation node.
-
                Rewrite (N, Unit (Parent (N)));
                Set_Unit (Parent (N), N);
             end if;
 
-         elsif Nkind (Parent (N)) = N_Compilation_Unit then
+         --  Replace instance node for library-level instantiations of
+         --  intrinsic subprograms, for ASIS use.
 
-               --  Replace instance node for library-level instantiations of
-               --  intrinsic subprograms, for ASIS use.
-
-               Rewrite (N, Unit (Parent (N)));
-               Set_Unit (Parent (N), N);
+         elsif Nkind (Parent (N)) = N_Compilation_Unit then
+            Rewrite (N, Unit (Parent (N)));
+            Set_Unit (Parent (N), N);
          end if;
 
          if Parent_Installed then
@@ -5359,7 +5355,6 @@ package body Sem_Ch12 is
          if SPARK_Mode = On then
             Dynamic_Elaboration_Checks := False;
          end if;
-
       end if;
 
    <<Leave>>
@@ -10663,17 +10658,18 @@ package body Sem_Ch12 is
            ("actual must exclude null to match generic formal#", Actual);
       end if;
 
-      --  An effectively volatile object cannot be used as an actual in
-      --  a generic instance. The following check is only relevant when
-      --  SPARK_Mode is on as it is not a standard Ada legality rule.
+      --  An effectively volatile object cannot be used as an actual in a
+      --  generic instantiation (SPARK RM 7.1.3(7)). The following check is
+      --  relevant only when SPARK_Mode is on as it is not a standard Ada
+      --  legality rule.
 
       if SPARK_Mode = On
         and then Present (Actual)
         and then Is_Effectively_Volatile_Object (Actual)
       then
          Error_Msg_N
-           ("volatile object cannot act as actual in generic instantiation "
-            & "(SPARK RM 7.1.3(8))", Actual);
+           ("volatile object cannot act as actual in generic instantiation",
+            Actual);
       end if;
 
       return List;
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 95624e6..820a2d1 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -2284,6 +2284,36 @@ package body Sem_Ch13 is
                   goto Continue;
                end Abstract_State;
 
+               --  Aspect Async_Readers is never delayed because it is
+               --  equivalent to a source pragma which appears after the
+               --  related object declaration.
+
+               when Aspect_Async_Readers =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Async_Readers);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
+               --  Aspect Async_Writers is never delayed because it is
+               --  equivalent to a source pragma which appears after the
+               --  related object declaration.
+
+               when Aspect_Async_Writers =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Async_Writers);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  Aspect Constant_After_Elaboration is never delayed because
                --  it is equivalent to a source pragma which appears after the
                --  related object declaration.
@@ -2354,6 +2384,36 @@ package body Sem_Ch13 is
                   Insert_Pragma (Aitem);
                   goto Continue;
 
+               --  Aspect Effecitve_Reads is never delayed because it is
+               --  equivalent to a source pragma which appears after the
+               --  related object declaration.
+
+               when Aspect_Effective_Reads =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Effective_Reads);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
+               --  Aspect Effective_Writes is never delayed because it is
+               --  equivalent to a source pragma which appears after the
+               --  related object declaration.
+
+               when Aspect_Effective_Writes =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Effective_Writes);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  Aspect Extensions_Visible is never delayed because it is
                --  equivalent to a source pragma which appears after the
                --  related subprogram.
@@ -2779,6 +2839,21 @@ package body Sem_Ch13 is
                      end;
                   end if;
 
+               --  Aspect Volatile_Function is never delayed because it is
+               --  equivalent to a source pragma which appears after the
+               --  related subprogram.
+
+               when Aspect_Volatile_Function =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Volatile_Function);
+
+                  Decorate (Aspect, Aitem);
+                  Insert_Pragma (Aitem);
+                  goto Continue;
+
                --  Case 2e: Annotate aspect
 
                when Aspect_Annotate =>
@@ -3234,47 +3309,10 @@ package body Sem_Ch13 is
                      goto Continue;
                   end if;
 
-                  --  External property aspects are Boolean by nature, but
-                  --  their pragmas must contain two arguments, the second
-                  --  being the optional Boolean expression.
-
-                  if A_Id = Aspect_Async_Readers   or else
-                     A_Id = Aspect_Async_Writers   or else
-                     A_Id = Aspect_Effective_Reads or else
-                     A_Id = Aspect_Effective_Writes
-                  then
-                     declare
-                        Args : List_Id;
-
-                     begin
-                        --  The first argument of the external property pragma
-                        --  is the related object.
-
-                        Args :=
-                          New_List (
-                            Make_Pragma_Argument_Association (Sloc (Ent),
-                              Expression => Ent));
-
-                        --  The second argument is the optional Boolean
-                        --  expression which must be propagated even if it
-                        --  evaluates to False as this has special semantic
-                        --  meaning.
-
-                        if Present (Expr) then
-                           Append_To (Args,
-                             Make_Pragma_Argument_Association (Loc,
-                               Expression => Relocate_Node (Expr)));
-                        end if;
-
-                        Make_Aitem_Pragma
-                          (Pragma_Argument_Associations => Args,
-                           Pragma_Name                  => Nam);
-                     end;
-
                   --  Cases where we do not delay, includes all cases where the
                   --  expression is missing other than the above cases.
 
-                  elsif not Delay_Required or else No (Expr) then
+                  if not Delay_Required or else No (Expr) then
                      Make_Aitem_Pragma
                        (Pragma_Argument_Associations => New_List (
                           Make_Pragma_Argument_Association (Sloc (Ent),
@@ -9285,12 +9323,16 @@ package body Sem_Ch13 is
 
          when Aspect_Abstract_State             |
               Aspect_Annotate                   |
+              Aspect_Async_Readers              |
+              Aspect_Async_Writers              |
               Aspect_Constant_After_Elaboration |
               Aspect_Contract_Cases             |
               Aspect_Default_Initial_Condition  |
               Aspect_Depends                    |
               Aspect_Dimension                  |
               Aspect_Dimension_System           |
+              Aspect_Effective_Reads            |
+              Aspect_Effective_Writes           |
               Aspect_Extensions_Visible         |
               Aspect_Ghost                      |
               Aspect_Global                     |
@@ -9309,7 +9351,8 @@ package body Sem_Ch13 is
               Aspect_Refined_State              |
               Aspect_SPARK_Mode                 |
               Aspect_Test_Case                  |
-              Aspect_Unimplemented              =>
+              Aspect_Unimplemented              |
+              Aspect_Volatile_Function          =>
             raise Program_Error;
 
       end case;
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index b8f901d..555c361 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3313,19 +3313,16 @@ package body Sem_Ch3 is
 
       if Ekind (Obj_Id) = E_Constant then
 
-         --  A constant cannot be effectively volatile. This check is only
-         --  relevant with SPARK_Mode on as it is not a standard Ada legality
-         --  rule. Do not flag internally-generated constants that map generic
-         --  formals to actuals in instantiations (SPARK RM 7.1.3(6)).
+         --  A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
+         --  This check is relevant only when SPARK_Mode is on as it is not a
+         --  standard Ada legality rule. Internally-generated constants that
+         --  map generic formals to actuals in instantiations are allowed to
+         --  be volatile.
 
          if SPARK_Mode = On
+           and then Comes_From_Source (Obj_Id)
            and then Is_Effectively_Volatile (Obj_Id)
            and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
-
-           --  Don't give this for internally generated entities (such as the
-           --  FIRST and LAST temporaries generated for bounds).
-
-           and then Comes_From_Source (Obj_Id)
          then
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
          end if;
@@ -3334,7 +3331,7 @@ package body Sem_Ch3 is
 
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
-         --  The following checks are only relevant when SPARK_Mode is on as
+         --  The following checks are relevant only when SPARK_Mode is on as
          --  they are not standard Ada legality rules. Internally generated
          --  temporaries are ignored.
 
@@ -3342,7 +3339,7 @@ package body Sem_Ch3 is
             if Is_Effectively_Volatile (Obj_Id) then
 
                --  The declaration of an effectively volatile object must
-               --  appear at the library level (SPARK RM 7.1.3(7), C.6(6)).
+               --  appear at the library level (SPARK RM 7.1.3(3), C.6(6)).
 
                if not Is_Library_Level_Entity (Obj_Id) then
                   Error_Msg_N
@@ -3367,7 +3364,7 @@ package body Sem_Ch3 is
 
             else
                --  A non-effectively volatile object cannot have effectively
-               --  volatile components (SPARK RM 7.1.3(7)).
+               --  volatile components (SPARK RM 7.1.3(6)).
 
                if not Is_Effectively_Volatile (Obj_Id)
                  and then Has_Volatile_Component (Obj_Typ)
@@ -19282,9 +19279,9 @@ package body Sem_Ch3 is
             end if;
          end if;
 
-         --  A discriminant cannot be effectively volatile. This check is only
-         --  relevant when SPARK_Mode is on as it is not standard Ada legality
-         --  rule (SPARK RM 7.1.3(6)).
+         --  A discriminant cannot be effectively volatile (SPARK RM 7.1.3(6)).
+         --  This check is relevant only when SPARK_Mode is on as it is not a
+         --  standard Ada legality rule.
 
          if SPARK_Mode = On
            and then Is_Effectively_Volatile (Defining_Identifier (Discr))
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 234317c..3e2e26b 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -2279,9 +2279,9 @@ package body Sem_Ch5 is
          end if;
       end if;
 
-      --  A loop parameter cannot be effectively volatile. This check is
-      --  peformed only when SPARK_Mode is on as it is not a standard Ada
-      --  legality check (SPARK RM 7.1.3(6)).
+      --  A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)).
+      --  This check is relevant only when SPARK_Mode is on as it is not a
+      --  standard Ada legality check.
 
       --  Not clear whether this applies to element iterators, where the
       --  cursor is not an explicit entity ???
@@ -3037,9 +3037,9 @@ package body Sem_Ch5 is
          end;
       end if;
 
-      --  A loop parameter cannot be effectively volatile. This check is
-      --  peformed only when SPARK_Mode is on as it is not a standard Ada
-      --  legality check (SPARK RM 7.1.3(6)).
+      --  A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)).
+      --  This check is relevant only when SPARK_Mode is on as it is not a
+      --  standard Ada legality check.
 
       if SPARK_Mode = On and then Is_Effectively_Volatile (Id) then
          Error_Msg_N ("loop parameter cannot be volatile", Id);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 0d61181..5e1ddf5 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -2228,6 +2228,19 @@ package body Sem_Ch6 is
 
       Check_Result_And_Post_State (Body_Id);
 
+      --  A stand alone non-volatile function body cannot have an effectively
+      --  volatile formal parameter or return type (SPARK RM 7.1.3(9)). This
+      --  check is relevant only when SPARK_Mode is on as it is not a standard
+      --  legality rule. The check is performed here because Volatile_Function
+      --  is processed after the analysis of the related subprogram body.
+
+      if SPARK_Mode = On
+        and then Ekind_In (Body_Id, E_Function, E_Generic_Function)
+        and then not Is_Volatile_Function (Body_Id)
+      then
+         Check_Nonvolatile_Function_Profile (Body_Id);
+      end if;
+
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
@@ -4086,6 +4099,19 @@ package body Sem_Ch6 is
          Check_Result_And_Post_State (Subp_Id);
       end if;
 
+      --  A non-volatile function cannot have an effectively volatile formal
+      --  parameter or return type (SPARK RM 7.1.3(9)). This check is relevant
+      --  only when SPARK_Mode is on as it is not a standard legality rule. The
+      --  check is performed here because pragma Volatile_Function is processed
+      --  after the analysis of the related subprogram declaration.
+
+      if SPARK_Mode = On
+        and then Ekind_In (Subp_Id, E_Function, E_Generic_Function)
+        and then not Is_Volatile_Function (Subp_Id)
+      then
+         Check_Nonvolatile_Function_Profile (Subp_Id);
+      end if;
+
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
@@ -4451,9 +4477,9 @@ package body Sem_Ch6 is
          --  the check is applied later (see Analyze_Subprogram_Declaration).
 
          if not Nkind_In (Original_Node (Parent (N)),
-                          N_Subprogram_Renaming_Declaration,
                           N_Abstract_Subprogram_Declaration,
-                          N_Formal_Abstract_Subprogram_Declaration)
+                          N_Formal_Abstract_Subprogram_Declaration,
+                          N_Subprogram_Renaming_Declaration)
          then
             if Is_Abstract_Type (Etype (Designator))
               and then not Is_Interface (Etype (Designator))
@@ -4464,14 +4490,15 @@ package body Sem_Ch6 is
             --  Ada 2012 (AI-0073): Extend this test to subprograms with an
             --  access result whose designated type is abstract.
 
-            elsif Nkind (Result_Definition (N)) = N_Access_Definition
+            elsif Ada_Version >= Ada_2012
+              and then Nkind (Result_Definition (N)) = N_Access_Definition
               and then
                 not Is_Class_Wide_Type (Designated_Type (Etype (Designator)))
               and then Is_Abstract_Type (Designated_Type (Etype (Designator)))
-              and then Ada_Version >= Ada_2012
             then
-               Error_Msg_N ("function whose access result designates "
-                            & "abstract type must be abstract", N);
+               Error_Msg_N
+                 ("function whose access result designates abstract type "
+                  & "must be abstract", N);
             end if;
          end if;
       end if;
@@ -9933,17 +9960,6 @@ package body Sem_Ch6 is
      (T           : List_Id;
       Related_Nod : Node_Id)
    is
-      Context     : constant Node_Id := Parent (Parent (T));
-      Param_Spec  : Node_Id;
-      Formal      : Entity_Id;
-      Formal_Type : Entity_Id;
-      Default     : Node_Id;
-      Ptype       : Entity_Id;
-
-      Num_Out_Params  : Nat       := 0;
-      First_Out_Param : Entity_Id := Empty;
-      --  Used for setting Is_Only_Out_Parameter
-
       function Designates_From_Limited_With (Typ : Entity_Id) return Boolean;
       --  Determine whether an access type designates a type coming from a
       --  limited view.
@@ -9986,6 +10002,19 @@ package body Sem_Ch6 is
                      and then Is_Class_Wide_Type (Etype (Prefix (D))));
       end Is_Class_Wide_Default;
 
+      --  Local variables
+
+      Context     : constant Node_Id := Parent (Parent (T));
+      Default     : Node_Id;
+      Formal      : Entity_Id;
+      Formal_Type : Entity_Id;
+      Param_Spec  : Node_Id;
+      Ptype       : Entity_Id;
+
+      Num_Out_Params  : Nat       := 0;
+      First_Out_Param : Entity_Id := Empty;
+      --  Used for setting Is_Only_Out_Parameter
+
    --  Start of processing for Process_Formals
 
    begin
@@ -10269,8 +10298,8 @@ package body Sem_Ch6 is
             Null_Exclusion_Static_Checks (Param_Spec);
          end if;
 
-         --  The following checks are relevant when SPARK_Mode is on as these
-         --  are not standard Ada legality rules.
+         --  The following checks are relevant only when SPARK_Mode is on as
+         --  these are not standard Ada legality rules.
 
          if SPARK_Mode = On then
             if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
@@ -10282,14 +10311,6 @@ package body Sem_Ch6 is
                   Error_Msg_N
                     ("function cannot have parameter of mode `OUT` or "
                      & "`IN OUT`", Formal);
-
-               --  A function cannot have an effectively volatile formal
-               --  parameter (SPARK RM 7.1.3(10)).
-
-               elsif Is_Effectively_Volatile (Formal) then
-                  Error_Msg_N
-                    ("function cannot have a volatile formal parameter",
-                     Formal);
                end if;
 
             --  A procedure cannot have an effectively volatile formal
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index dabacf5..2733dc3 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -206,7 +206,8 @@ package body Sem_Prag is
    function Find_Related_Context
      (Prag      : Node_Id;
       Do_Checks : Boolean := False) return Node_Id;
-   --  Subsidiaty to the analysis of pragmas Constant_After_Elaboration and
+   --  Subsidiaty to the analysis of pragmas Async_Readers, Async_Writers,
+   --  Constant_After_Elaboration, Effective_Reads, Effective_Writers and
    --  Part_Of. Find the first source declaration or statement found while
    --  traversing the previous node chain starting from pragma Prag. If flag
    --  Do_Checks is set, the routine reports duplicate pragmas. The routine
@@ -1720,19 +1721,12 @@ package body Sem_Prag is
      (N        : Node_Id;
       Expr_Val : out Boolean)
    is
-      Arg1   : constant Node_Id   := First (Pragma_Argument_Associations (N));
-      Expr   : constant Node_Id   := Get_Pragma_Arg (Next (Arg1));
-      Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1));
-
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+      Arg1     : constant Node_Id := First (Pragma_Argument_Associations (N));
+      Obj_Decl : constant Node_Id := Find_Related_Context (N);
+      Obj_Id   : constant Entity_Id := Defining_Entity (Obj_Decl);
+      Expr     : Node_Id;
 
    begin
-      --  Set the Ghost mode in effect from the pragma. Due to the delayed
-      --  analysis of the pragma, the Ghost mode at point of declaration and
-      --  point of analysis may not necessarely be the same. Use the mode in
-      --  effect at the point of declaration.
-
-      Set_Ghost_Mode (N);
       Error_Msg_Name_1 := Pragma_Name (N);
 
       --  An external property pragma must apply to an effectively volatile
@@ -1754,17 +1748,13 @@ package body Sem_Prag is
 
       Expr_Val := True;
 
-      if Present (Expr) then
-         Analyze_And_Resolve (Expr, Standard_Boolean);
+      if Present (Arg1) then
+         Expr := Get_Pragma_Arg (Arg1);
 
          if Is_OK_Static_Expression (Expr) then
             Expr_Val := Is_True (Expr_Value (Expr));
-         else
-            SPARK_Msg_N ("expression of % must be static", Expr);
          end if;
       end if;
-
-      Ghost_Mode := Save_Ghost_Mode;
    end Analyze_External_Property_In_Decl_Part;
 
    ---------------------------------
@@ -1924,6 +1914,18 @@ package body Sem_Prag is
                      SPARK_Msg_N ("\use its constituents instead", Item);
                      return;
 
+                  --  An external state cannot appear as a global item of a
+                  --  nonvolatile function (SPARK RM 7.1.3(8)).
+
+                  elsif Is_External_State (Item_Id)
+                    and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                    and then not Is_Volatile_Function (Spec_Id)
+                  then
+                     SPARK_Msg_NE
+                       ("external state & cannot act as global item of "
+                        & "nonvolatile function", Item, Item_Id);
+                     return;
+
                   --  If the reference to the abstract state appears in an
                   --  enclosing package body that will eventually refine the
                   --  state, record the reference for future checks.
@@ -1956,9 +1958,11 @@ package body Sem_Prag is
                  and then Is_Effectively_Volatile (Item_Id)
                then
                   --  An effectively volatile object cannot appear as a global
-                  --  item of a function (SPARK RM 7.1.3(9)).
+                  --  item of a nonvolatile function (SPARK RM 7.1.3(8)).
 
-                  if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
+                  if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                    and then not Is_Volatile_Function (Spec_Id)
+                  then
                      Error_Msg_NE
                        ("volatile object & cannot act as global item of a "
                         & "function", Item, Item_Id);
@@ -2936,6 +2940,13 @@ package body Sem_Prag is
       --  In this version of the procedure, the identifier name is given as
       --  a string with lower case letters.
 
+      procedure Check_Static_Boolean_Expression (Expr : Node_Id);
+      --  Subsidiary to the analysis of pragmas Async_Readers, Async_Writers,
+      --  Constant_After_Elaboration, Effective_Reads, Effective_Writes,
+      --  Extensions_Visible and Volatile_Function. Ensure that expression Expr
+      --  is an OK static boolean expression. Emit an error if this is not the
+      --  case.
+
       procedure Check_Static_Constraint (Constr : Node_Id);
       --  Constr is a constraint from an N_Subtype_Indication node from a
       --  component constraint in an Unchecked_Union type. This routine checks
@@ -5070,6 +5081,22 @@ package body Sem_Prag is
          Check_Optional_Identifier (Arg, Name_Find);
       end Check_Optional_Identifier;
 
+      -------------------------------------
+      -- Check_Static_Boolean_Expression --
+      -------------------------------------
+
+      procedure Check_Static_Boolean_Expression (Expr : Node_Id) is
+      begin
+         if Present (Expr) then
+            Analyze_And_Resolve (Expr, Standard_Boolean);
+
+            if not Is_OK_Static_Expression (Expr) then
+               Error_Pragma_Arg
+                 ("expression of pragma % must be static", Expr);
+            end if;
+         end if;
+      end Check_Static_Boolean_Expression;
+
       -----------------------------
       -- Check_Static_Constraint --
       -----------------------------
@@ -11079,43 +11106,45 @@ package body Sem_Prag is
          -- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes --
          ------------------------------------------------------------------
 
-         --  pragma Asynch_Readers   ( object_LOCAL_NAME [, FLAG] );
-         --  pragma Asynch_Writers   ( object_LOCAL_NAME [, FLAG] );
-         --  pragma Effective_Reads  ( object_LOCAL_NAME [, FLAG] );
-         --  pragma Effective_Writes ( object_LOCAL_NAME [, FLAG] );
-
-         --  FLAG ::= boolean_EXPRESSION
+         --  pragma Asynch_Readers   [ (boolean_EXPRESSION) ];
+         --  pragma Asynch_Writers   [ (boolean_EXPRESSION) ];
+         --  pragma Effective_Reads  [ (boolean_EXPRESSION) ];
+         --  pragma Effective_Writes [ (boolean_EXPRESSION) ];
 
          when Pragma_Async_Readers    |
               Pragma_Async_Writers    |
               Pragma_Effective_Reads  |
               Pragma_Effective_Writes =>
          Async_Effective : declare
-            Duplic : Node_Id;
-            Expr   : Node_Id;
-            Obj    : Node_Id;
-            Obj_Id : Entity_Id;
+            Obj_Decl : Node_Id;
+            Obj_Id   : Entity_Id;
 
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
-            Check_At_Least_N_Arguments (1);
-            Check_At_Most_N_Arguments  (2);
-            Check_Arg_Is_Local_Name (Arg1);
-            Error_Msg_Name_1 := Pname;
+            Check_At_Most_N_Arguments  (1);
 
-            Obj  := Get_Pragma_Arg (Arg1);
-            Expr := Get_Pragma_Arg (Arg2);
+            Obj_Decl := Find_Related_Context (N, Do_Checks => True);
+
+            --  Object declaration
+
+            if Nkind (Obj_Decl) = N_Object_Declaration then
+               null;
+
+            --  Otherwise the pragma is associated with an illegal construact
+
+            else
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Obj_Id := Defining_Entity (Obj_Decl);
 
             --  Perform minimal verification to ensure that the argument is at
             --  least a variable. Subsequent finer grained checks will be done
             --  at the end of the declarative region the contains the pragma.
 
-            if Is_Entity_Name (Obj)
-              and then Present (Entity (Obj))
-              and then Ekind (Entity (Obj)) = E_Variable
-            then
-               Obj_Id := Entity (Obj);
+            if Ekind (Obj_Id) = E_Variable then
 
                --  A pragma that applies to a Ghost entity becomes Ghost for
                --  the purposes of legality checks and removal of ignored Ghost
@@ -11123,30 +11152,19 @@ package body Sem_Prag is
 
                Mark_Pragma_As_Ghost (N, Obj_Id);
 
-               --  Detect a duplicate pragma. Note that it is not efficient to
-               --  examine preceding statements as Boolean aspects may appear
-               --  anywhere between the related object declaration and its
-               --  freeze point. As an alternative, inspect the contents of the
-               --  variable contract.
-
-               Duplic := Get_Pragma (Obj_Id, Prag_Id);
+               --  Analyze the Boolean expression (if any)
 
-               if Present (Duplic) then
-                  Error_Msg_Sloc := Sloc (Duplic);
-                  Error_Msg_N ("pragma % duplicates pragma declared #", N);
+               if Present (Arg1) then
+                  Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
+               end if;
 
-               --  No duplicate detected
+               --  Chain the pragma on the contract for further processing by
+               --  Analyze_External_Property_In_Decl_Part.
 
-               else
-                  if Present (Expr) then
-                     Preanalyze_And_Resolve (Expr, Standard_Boolean);
-                  end if;
+               Add_Contract_Item (N, Obj_Id);
 
-                  --  Chain the pragma on the contract for further processing
-                  --  by Analyze_External_Property_In_Decl_Part.
+            --  Otherwise the external property applies to a constant
 
-                  Add_Contract_Item (N, Obj_Id);
-               end if;
             else
                Error_Pragma ("pragma % must apply to a volatile object");
             end if;
@@ -12150,7 +12168,6 @@ package body Sem_Prag is
 
          when Pragma_Constant_After_Elaboration => Constant_After_Elaboration :
          declare
-            Expr     : Node_Id;
             Obj_Decl : Node_Id;
             Obj_Id   : Entity_Id;
 
@@ -12208,15 +12225,7 @@ package body Sem_Prag is
             --  Analyze the Boolean expression (if any)
 
             if Present (Arg1) then
-               Expr := Get_Pragma_Arg (Arg1);
-
-               Analyze_And_Resolve (Expr, Standard_Boolean);
-
-               if not Is_OK_Static_Expression (Expr) then
-                  Error_Pragma_Arg
-                    ("expression of pragma % must be static", Expr);
-                  return;
-               end if;
+               Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
             end if;
 
             --  Chain the pragma on the contract for completeness
@@ -13950,7 +13959,6 @@ package body Sem_Prag is
          --    the annotation must instantiate itself.
 
          when Pragma_Extensions_Visible => Extensions_Visible : declare
-            Expr          : Node_Id;
             Formal        : Entity_Id;
             Has_OK_Formal : Boolean := False;
             Spec_Id       : Entity_Id;
@@ -14043,15 +14051,8 @@ package body Sem_Prag is
             --  Analyze the Boolean expression (if any)
 
             if Present (Arg1) then
-               Expr := Expression (Get_Argument (N, Spec_Id));
-
-               Analyze_And_Resolve (Expr, Standard_Boolean);
-
-               if not Is_OK_Static_Expression (Expr) then
-                  Error_Pragma_Arg
-                    ("expression of pragma % must be static", Expr);
-                  return;
-               end if;
+               Check_Static_Boolean_Expression
+                 (Expression (Get_Argument (N, Spec_Id)));
             end if;
 
             --  Chain the pragma on the contract for completeness
@@ -21486,6 +21487,14 @@ package body Sem_Prag is
          when Pragma_Volatile =>
             Process_Atomic_Independent_Shared_Volatile;
 
+         -------------------------
+         -- Volatile_Components --
+         -------------------------
+
+         --  pragma Volatile_Components (array_LOCAL_NAME);
+
+         --  Volatile is handled by the same circuit as Atomic_Components
+
          --------------------------
          -- Volatile_Full_Access --
          --------------------------
@@ -21496,13 +21505,97 @@ package body Sem_Prag is
             GNAT_Pragma;
             Process_Atomic_Independent_Shared_Volatile;
 
-         -------------------------
-         -- Volatile_Components --
-         -------------------------
+         -----------------------
+         -- Volatile_Function --
+         -----------------------
 
-         --  pragma Volatile_Components (array_LOCAL_NAME);
+         --  pragma Volatile_Function [ (boolean_EXPRESSION) ];
 
-         --  Volatile is handled by the same circuit as Atomic_Components
+         when Pragma_Volatile_Function => Volatile_Function : declare
+            Over_Id   : Entity_Id;
+            Spec_Id   : Entity_Id;
+            Subp_Decl : Node_Id;
+
+         begin
+            GNAT_Pragma;
+            Check_No_Identifiers;
+            Check_At_Most_N_Arguments (1);
+
+            Subp_Decl :=
+              Find_Related_Subprogram_Or_Body (N, Do_Checks => True);
+
+            --  Function instantiation
+
+            if Nkind (Subp_Decl) = N_Function_Instantiation then
+               null;
+
+            --  Generic subprogram
+
+            elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then
+               null;
+
+            --  Body acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body
+              and then No (Corresponding_Spec (Subp_Decl))
+            then
+               null;
+
+            --  Body stub acts as spec
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+              and then No (Corresponding_Spec_Of_Stub (Subp_Decl))
+            then
+               null;
+
+            --  Subprogram
+
+            elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then
+               null;
+
+            else
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+            Over_Id := Overridden_Operation (Spec_Id);
+
+            --  A pragma that applies to a Ghost entity becomes Ghost for the
+            --  purposes of legality checks and removal of ignored Ghost code.
+
+            Mark_Pragma_As_Ghost (N, Spec_Id);
+
+            --  A volatile function cannot override a non-volatile function
+            --  (SPARK RM 7.1.2(15)). Overriding checks are usually performed
+            --  in New_Overloaded_Entity, however at that point the pragma has
+            --  not been processed yet.
+
+            if Present (Over_Id)
+              and then not Is_Volatile_Function (Over_Id)
+            then
+               Error_Msg_N
+                 ("incompatible volatile function values in effect", Spec_Id);
+
+               Error_Msg_Sloc := Sloc (Over_Id);
+               Error_Msg_N
+                 ("\& declared # with Volatile_Function value `False`",
+                  Spec_Id);
+
+               Error_Msg_Sloc := Sloc (Spec_Id);
+               Error_Msg_N
+                 ("\overridden # with Volatile_Function value `True`",
+                  Spec_Id);
+            end if;
+
+            --  Analyze the Boolean expression (if any)
+
+            if Present (Arg1) then
+               Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1));
+            end if;
+
+            Add_Contract_Item (N, Spec_Id);
+         end Volatile_Function;
 
          ----------------------
          -- Warning_As_Error --
@@ -26278,6 +26371,33 @@ package body Sem_Prag is
            and then Nkind (Parent (Parent (N))) = N_Package_Body;
    end Is_Elaboration_SPARK_Mode;
 
+   -----------------------
+   -- Is_Enabled_Pragma --
+   -----------------------
+
+   function Is_Enabled_Pragma (Prag : Node_Id) return Boolean is
+      Arg : Node_Id;
+
+   begin
+      if Present (Prag) then
+         Arg := First (Pragma_Argument_Associations (Prag));
+
+         if Present (Arg) then
+            return Is_True (Expr_Value (Get_Pragma_Arg (Arg)));
+
+         --  The lack of a Boolean argument automatically enables the pragma
+
+         else
+            return True;
+         end if;
+
+      --  The pragma is missing, therefore it is not enabled
+
+      else
+         return False;
+      end if;
+   end Is_Enabled_Pragma;
+
    -----------------------------------------
    -- Is_Non_Significant_Pragma_Reference --
    -----------------------------------------
@@ -26519,6 +26639,7 @@ package body Sem_Prag is
       Pragma_Volatile                       =>  0,
       Pragma_Volatile_Components            =>  0,
       Pragma_Volatile_Full_Access           =>  0,
+      Pragma_Volatile_Function              =>  0,
       Pragma_Warning_As_Error               =>  0,
       Pragma_Warnings                       =>  0,
       Pragma_Weak_External                  =>  0,
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 72881a0..cdd3657 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -364,6 +364,23 @@ package Sem_Prag is
    --  Determine whether pragma SPARK_Mode appears in the statement part of a
    --  package body.
 
+   function Is_Enabled_Pragma (Prag : Node_Id) return Boolean;
+   --  Determine whether a Boolean-like SPARK pragma Prag is enabled. To be
+   --  considered enabled, the pragma must either:
+   --    * Appear without its Boolean expression
+   --    * The Boolean expression evaluates to "True"
+   --
+   --  Boolean-like SPARK pragmas differ from pure Boolean Ada pragmas in that
+   --  their optional Boolean expression must be static and cannot benefit from
+   --  forward references. The following are Boolean-like SPARK pragmas:
+   --    Async_Readers
+   --    Async_Writers
+   --    Constant_After_Elaboration
+   --    Effective_Reads
+   --    Effective_Writes
+   --    Extensions_Visible
+   --    Volatile_Function
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 01b912f..5b62aed 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4105,22 +4105,11 @@ package body Sem_Res is
                --  actual to a nested call, since this constitutes a reading of
                --  the parameter, which is not allowed.
 
-               if Is_Entity_Name (A)
+               if Ada_Version = Ada_83
+                 and then Is_Entity_Name (A)
                  and then Ekind (Entity (A)) = E_Out_Parameter
                then
-                  if Ada_Version = Ada_83 then
-                     Error_Msg_N
-                       ("(Ada 83) illegal reading of out parameter", A);
-
-                  --  An effectively volatile OUT parameter cannot act as IN or
-                  --  IN OUT actual in a call (SPARK RM 7.1.3(11)).
-
-                  elsif SPARK_Mode = On
-                    and then Is_Effectively_Volatile (Entity (A))
-                  then
-                     Error_Msg_N
-                       ("illegal reading of volatile OUT parameter", A);
-                  end if;
+                  Error_Msg_N ("(Ada 83) illegal reading of out parameter", A);
                end if;
             end if;
 
@@ -4472,8 +4461,8 @@ package body Sem_Res is
             --  temporaries are ignored.
 
             if SPARK_Mode = On
-              and then Is_Effectively_Volatile_Object (A)
               and then Comes_From_Source (A)
+              and then Is_Effectively_Volatile_Object (A)
             then
                --  An effectively volatile object may act as an actual
                --  parameter when the corresponding formal is of a non-scalar
@@ -6792,7 +6781,7 @@ package body Sem_Res is
         (Context : Node_Id;
          Obj_Ref : Node_Id) return Boolean;
       --  Determine whether node Context denotes a "non-interfering context"
-      --  (as defined in SPARK RM 7.1.3(13)) where volatile reference Obj_Ref
+      --  (as defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref
       --  can safely reside.
 
       ----------------------------------------
@@ -6851,6 +6840,10 @@ package body Sem_Res is
          function Within_Procedure_Call (Nod : Node_Id) return Boolean;
          --  Determine whether an arbitrary node appears in a procedure call
 
+         function Within_Volatile_Function (Id : Entity_Id) return Boolean;
+         --  Determine whether an arbitrary entity appears in a volatile
+         --  function.
+
          ------------------
          -- Within_Check --
          ------------------
@@ -6905,6 +6898,32 @@ package body Sem_Res is
             return False;
          end Within_Procedure_Call;
 
+         ------------------------------
+         -- Within_Volatile_Function --
+         ------------------------------
+
+         function Within_Volatile_Function (Id : Entity_Id) return Boolean is
+            Func_Id : Entity_Id;
+
+         begin
+            --  Traverse the scope stack looking for a [generic] function
+
+            Func_Id := Id;
+            while Present (Func_Id) and then Func_Id /= Standard_Standard loop
+               if Ekind_In (Func_Id, E_Function, E_Generic_Function) then
+                  return Is_Volatile_Function (Func_Id);
+               end if;
+
+               Func_Id := Scope (Func_Id);
+            end loop;
+
+            return False;
+         end Within_Volatile_Function;
+
+         --  Local variables
+
+         Obj_Id : Entity_Id;
+
       --  Start of processing for Is_OK_Volatile_Context
 
       begin
@@ -6914,14 +6933,26 @@ package body Sem_Res is
             return True;
 
          --  The volatile object is part of the initialization expression of
-         --  another object. Ensure that the climb of the parent chain came
-         --  from the expression side and not from the name side.
+         --  another object.
 
          elsif Nkind (Context) = N_Object_Declaration
            and then Present (Expression (Context))
            and then Expression (Context) = Obj_Ref
          then
-            return True;
+            Obj_Id := Defining_Entity (Context);
+
+            --  The volatile object acts as the initialization expression of an
+            --  extended return statement. This is valid context as long as the
+            --  function is volatile.
+
+            if Is_Return_Object (Obj_Id) then
+               return Within_Volatile_Function (Obj_Id);
+
+            --  Otherwise this is a normal object initialization
+
+            else
+               return True;
+            end if;
 
          --  The volatile object appears as an actual parameter in a call to an
          --  instance of Unchecked_Conversion whose result is renamed.
@@ -6932,6 +6963,15 @@ package body Sem_Res is
          then
             return True;
 
+         --  The volatile object appears as the expression of a simple return
+         --  statement that applies to a volatile function.
+
+         elsif Nkind (Context) = N_Simple_Return_Statement
+           and then Expression (Context) = Obj_Ref
+         then
+            return
+              Within_Volatile_Function (Return_Statement_Entity (Context));
+
          --  The volatile object appears as the prefix of a name occurring
          --  in a non-interfering context.
 
@@ -7057,14 +7097,6 @@ package body Sem_Res is
       then
          if Ada_Version = Ada_83 then
             Error_Msg_N ("(Ada 83) illegal reading of out parameter", N);
-
-         --  An effectively volatile OUT parameter cannot be read
-         --  (SPARK RM 7.1.3(11)).
-
-         elsif SPARK_Mode = On
-           and then Is_Effectively_Volatile (E)
-         then
-            Error_Msg_N ("illegal reading of volatile OUT parameter", N);
          end if;
 
       --  In all other cases, just do the possible static evaluation
@@ -7117,7 +7149,7 @@ package body Sem_Res is
         and then Comes_From_Source (N)
       then
          --  The effectively volatile objects appears in a "non-interfering
-         --  context" as defined in SPARK RM 7.1.3(13).
+         --  context" as defined in SPARK RM 7.1.3(12).
 
          if Is_OK_Volatile_Context (Par, N) then
             null;
@@ -7128,7 +7160,7 @@ package body Sem_Res is
          else
             SPARK_Msg_N
               ("volatile object cannot appear in this context "
-               & "(SPARK RM 7.1.3(13))", N);
+               & "(SPARK RM 7.1.3(12))", N);
          end if;
       end if;
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index d7177b8..27b8f9e 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -375,6 +375,7 @@ package body Sem_Util is
       --    Postcondition
       --    Precondition
       --    Test_Case
+      --    Volatile_Function
 
       elsif Ekind_In (Id, E_Entry, E_Entry_Family)
         or else Is_Generic_Subprogram (Id)
@@ -392,6 +393,11 @@ package body Sem_Util is
          then
             Add_Classification;
 
+         elsif Prag_Nam = Name_Volatile_Function
+           and then Ekind_In (Id, E_Function, E_Generic_Function)
+         then
+            Add_Classification;
+
          --  The pragma is not a proper contract item
 
          else
@@ -3146,6 +3152,36 @@ package body Sem_Util is
       end if;
    end Check_No_Hidden_State;
 
+   ----------------------------------------
+   -- Check_Nonvolatile_Function_Profile --
+   ----------------------------------------
+
+   procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id) is
+      Formal : Entity_Id;
+
+   begin
+      --  Inspect all formal parameters
+
+      Formal := First_Formal (Func_Id);
+      while Present (Formal) loop
+         if Is_Effectively_Volatile (Etype (Formal)) then
+            Error_Msg_NE
+              ("nonvolatile function & cannot have a volatile parameter",
+               Formal, Func_Id);
+         end if;
+
+         Next_Formal (Formal);
+      end loop;
+
+      --  Inspect the return type
+
+      if Is_Effectively_Volatile (Etype (Func_Id)) then
+         Error_Msg_N
+           ("nonvolatile function & cannot have a volatile return type",
+            Func_Id);
+      end if;
+   end Check_Nonvolatile_Function_Profile;
+
    ------------------------------------------
    -- Check_Potentially_Blocking_Operation --
    ------------------------------------------
@@ -8577,18 +8613,18 @@ package body Sem_Util is
          ----------------
 
          function Is_Enabled (Prag : Node_Id) return Boolean is
-            Arg2 : Node_Id;
+            Arg1 : Node_Id;
 
          begin
             if Present (Prag) then
-               Arg2 := Next (First (Pragma_Argument_Associations (Prag)));
+               Arg1 := First (Pragma_Argument_Associations (Prag));
 
                --  The pragma has an optional Boolean expression, the related
                --  property is enabled only when the expression evaluates to
                --  True.
 
-               if Present (Arg2) then
-                  return Is_True (Expr_Value (Get_Pragma_Arg (Arg2)));
+               if Present (Arg1) then
+                  return Is_True (Expr_Value (Get_Pragma_Arg (Arg1)));
 
                --  Otherwise the lack of expression enables the property by
                --  default.
@@ -11358,6 +11394,66 @@ package body Sem_Util is
    -----------------------------
 
    function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is
+      function Is_Descendant_Of_Suspension_Object
+        (Typ : Entity_Id) return Boolean;
+      --  Determine whether type Typ is a descendant of type Suspension_Object
+      --  defined in Ada.Synchronous_Task_Control. This routine is similar to
+      --  Sem_Util.Is_Descendent_Of, however this version does not load unit
+      --  Ada.Synchronous_Task_Control.
+
+      ----------------------------------------
+      -- Is_Descendant_Of_Suspension_Object --
+      ----------------------------------------
+
+      function Is_Descendant_Of_Suspension_Object
+        (Typ : Entity_Id) return Boolean
+      is
+         Cur_Typ : Entity_Id;
+         Par_Typ : Entity_Id;
+
+      begin
+         --  Do not attempt to load Ada.Synchronous_Task_Control in No_Run_Time
+         --  mode. The unit contains tagged types and those are not allowed in
+         --  this mode.
+
+         if No_Run_Time_Mode then
+            return False;
+
+         --  Unit Ada.Synchronous_Task_Control is not available, the type
+         --  cannot possibly be a descendant of Suspension_Object.
+
+         elsif not RTE_Available (RE_Suspension_Object) then
+            return False;
+         end if;
+
+         --  Climb the type derivation chain checking each parent type against
+         --  Suspension_Object.
+
+         Cur_Typ := Base_Type (Typ);
+         while Present (Cur_Typ) loop
+            Par_Typ := Etype (Cur_Typ);
+
+            --  The current type is a match
+
+            if Is_RTE (Cur_Typ, RE_Suspension_Object) then
+               return True;
+
+            --  Stop the traversal once the root of the derivation chain has
+            --  been reached. In that case the current type is its own base
+            --  type.
+
+            elsif Cur_Typ = Par_Typ then
+               exit;
+            end if;
+
+            Cur_Typ := Base_Type (Par_Typ);
+         end loop;
+
+         return False;
+      end Is_Descendant_Of_Suspension_Object;
+
+   --  Start of processing for Is_Effectively_Volatile
+
    begin
       if Is_Type (Id) then
 
@@ -11377,6 +11473,19 @@ package body Sem_Util is
                 or else
               Is_Effectively_Volatile (Component_Type (Base_Type (Id)));
 
+         --  A protected type is always volatile
+
+         elsif Is_Protected_Type (Id) then
+            return True;
+
+         --  A descendant of Ada.Synchronous_Task_Control.Suspension_Object is
+         --  automatically volatile.
+
+         elsif Is_Descendant_Of_Suspension_Object (Id) then
+            return True;
+
+         --  Otherwise the type is not effectively volatile
+
          else
             return False;
          end if;
@@ -13510,6 +13619,33 @@ package body Sem_Util is
         and then Scope (Scope (Scope (Root))) = Standard_Standard;
    end Is_Visibly_Controlled;
 
+   --------------------------
+   -- Is_Volatile_Function --
+   --------------------------
+
+   function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean is
+   begin
+      --  The caller must ensure that Func_Id denotes a function
+
+      pragma Assert (Ekind_In (Func_Id, E_Function, E_Generic_Function));
+
+      --  A protected function is automatically volatile
+
+      if Is_Primitive (Func_Id)
+        and then Present (First_Formal (Func_Id))
+        and then Is_Protected_Type (Etype (First_Formal (Func_Id)))
+      then
+         return True;
+
+      --  Otherwise the function is treated as volatile if it is subject to
+      --  enabled pragma Volatile_Function.
+
+      else
+         return
+           Is_Enabled_Pragma (Get_Pragma (Func_Id, Pragma_Volatile_Function));
+      end if;
+   end Is_Volatile_Function;
+
    ------------------------
    -- Is_Volatile_Object --
    ------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 543d31f..5583aa0 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -73,6 +73,7 @@ package Sem_Util is
    --    Refined_Post
    --    Refined_States
    --    Test_Case
+   --    Volatile_Function
 
    procedure Add_Global_Declaration (N : Node_Id);
    --  These procedures adds a declaration N at the library level, to be
@@ -313,6 +314,10 @@ package Sem_Util is
    --  Determine whether object or state Id introduces a hidden state. If this
    --  is the case, emit an error.
 
+   procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id);
+   --  Verify that the profile of nonvolatile function Func_Id does not contain
+   --  effectively volatile parameters or return type.
+
    procedure Check_Potentially_Blocking_Operation (N : Node_Id);
    --  N is one of the statement forms that is a potentially blocking
    --  operation. If it appears within a protected action, emit warning.
@@ -533,7 +538,7 @@ package Sem_Util is
 
    function Enclosing_Declaration (N : Node_Id) return Node_Id;
    --  Returns the declaration node enclosing N (including possibly N itself),
-   --  if any, or Empty otherwise
+   --  if any, or Empty otherwise.
 
    function Enclosing_Generic_Body
      (N : Node_Id) return Node_Id;
@@ -1285,13 +1290,17 @@ package Sem_Util is
    --  . machine_emin = 3 - machine_emax
 
    function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
-   --  The SPARK property "effectively volatile" applies to both types and
-   --  objects. To qualify as such, an entity must be either volatile or be
-   --  (of) an array type subject to aspect Volatile_Components.
+   --  Determine whether a type or object denoted by entity Id is effectively
+   --  volatile (SPARK RM 7.1.2). To qualify as such, the entity must be either
+   --    * Volatile
+   --    * An array type subject to aspect Volatile_Components
+   --    * An array type whose component type is effectively volatile
+   --    * A protected type
+   --    * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object
 
    function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean;
    --  Determine whether an arbitrary node denotes an effectively volatile
-   --  object.
+   --  object (SPARK RM 7.1.2).
 
    function Is_Expression_Function (Subp : Entity_Id) return Boolean;
    --  Predicate to determine whether a scope entity comes from a rewritten
@@ -1301,8 +1310,8 @@ package Sem_Util is
    function Is_EVF_Expression (N : Node_Id) return Boolean;
    --  Determine whether node N denotes a reference to a formal parameter of
    --  a specific tagged type whose related subprogram is subject to pragma
-   --  Extensions_Visible with value "False". Several other constructs fall
-   --  under this category:
+   --  Extensions_Visible with value "False" (SPARK RM 6.1.7). Several other
+   --  constructs fall under this category:
    --    1) A qualified expression whose operand is EVF
    --    2) A type conversion whose operand is EVF
    --    3) An if expression with at least one EVF dependent_expression
@@ -1550,6 +1559,11 @@ package Sem_Util is
    --  Initialize/Adjust/Finalize subprogram does not override the inherited
    --  one.
 
+   function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean;
+   --  Determine whether [generic] function Func_Id is subject to enabled
+   --  pragma Volatile_Function. Protected functions are treated as volatile
+   --  (SPARK RM 7.1.2).
+
    function Is_Volatile_Object (N : Node_Id) return Boolean;
    --  Determines if the given node denotes an volatile object in the sense of
    --  the legality checks described in RM C.6(12). Note that the test here is
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index 9484311..d5b06a8 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -632,6 +632,7 @@ package Snames is
    Name_Volatile                       : constant Name_Id := N + $;
    Name_Volatile_Components            : constant Name_Id := N + $;
    Name_Volatile_Full_Access           : constant Name_Id := N + $; -- GNAT
+   Name_Volatile_Function              : constant Name_Id := N + $; -- GNAT
    Name_Weak_External                  : constant Name_Id := N + $; -- GNAT
    Last_Pragma_Name                    : constant Name_Id := N + $;
 
@@ -1937,6 +1938,7 @@ package Snames is
       Pragma_Volatile,
       Pragma_Volatile_Components,
       Pragma_Volatile_Full_Access,
+      Pragma_Volatile_Function,
       Pragma_Weak_External,
 
       --  The following pragmas are on their own, out of order, because of the