[multiple changes]

2014-01-27  Thomas Quinot  <quinot@adacore.com>

	* exp_smem.adb (Expand_Shared_Passive_Variable): For a reference
	to a shared variable as an OUT formal in a call to an init proc,
	the 'Read call must be emitted after, not before, the call.

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

	* gnat_rm.texi: Remove mention of AUTO mode for SPARK_Mode pragma.

From-SVN: r207139

gcc/ada/ChangeLog

+2014-01-27  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_smem.adb (Expand_Shared_Passive_Variable): For a reference
+	to a shared variable as an OUT formal in a call to an init proc,
+	the 'Read call must be emitted after, not before, the call.
+
+2014-01-27  Robert Dewar  <dewar@adacore.com>
+
+	* gnat_rm.texi: Remove mention of AUTO mode for SPARK_Mode pragma.
+
 2014-01-27  Robert Dewar  <dewar@adacore.com>
 
 	* a-wichha.adb (Character_Set_Version): Change to output proper

gcc/ada/exp_smem.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1998-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1998-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -26,6 +26,7 @@
 with Atree;    use Atree;
 with Einfo;    use Einfo;
 with Exp_Ch9;  use Exp_Ch9;
+with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
 with Nmake;    use Nmake;
 with Namet;    use Namet;
@@ -49,36 +50,38 @@ package body Exp_Smem is
    -- Local Subprograms --
    -----------------------
 
-   procedure Add_Read_Before (N : Node_Id);
-   --  Insert a Shared_Var_ROpen call for variable before node N
+   procedure Add_Read (N : Node_Id; Call : Node_Id := Empty);
+   --  Insert a Shared_Var_ROpen call for variable before node N, unless
+   --  Call is a call to an init-proc, in which case the call is inserted
+   --  after Call.
 
    procedure Add_Write_After (N : Node_Id);
-   --  Insert a Shared_Var_WOpen call for variable after the node
-   --  Insert_Node, as recorded by On_Lhs_Of_Assignment (where it points
-   --  to the assignment statement) or Is_Out_Actual (where it points to
-   --  the procedure call statement).
+   --  Insert a Shared_Var_WOpen call for variable after the node Insert_Node,
+   --  as recorded by On_Lhs_Of_Assignment (where it points to the assignment
+   --  statement) or Is_Out_Actual (where it points to the procedure call
+   --  statement).
 
    procedure Build_Full_Name (E : Entity_Id; N : out String_Id);
    --  Build the fully qualified string name of a shared variable
 
    function On_Lhs_Of_Assignment (N : Node_Id) return Boolean;
-   --  Determines if N is on the left hand of the assignment. This means
-   --  that either it is a simple variable, or it is a record or array
-   --  variable with a corresponding selected or indexed component on
-   --  the left side of an assignment. If the result is True, then
-   --  Insert_Node is set to point to the assignment
+   --  Determines if N is on the left hand of the assignment. This means that
+   --  either it is a simple variable, or it is a record or array variable with
+   --  a corresponding selected or indexed component on the left side of an
+   --  assignment. If the result is True, then Insert_Node is set to point
+   --  to the assignment
 
    function Is_Out_Actual (N : Node_Id) return Boolean;
-   --  In a similar manner, this function determines if N appears as an
-   --  OUT or IN OUT parameter to a procedure call. If the result is
-   --  True, then Insert_Node is set to point to the call.
+   --  In a similar manner, this function determines if N appears as an OUT
+   --  or IN OUT parameter to a procedure call. If the result is True, then
+   --  Insert_Node is set to point to the call.
 
    function Build_Shared_Var_Proc_Call
      (Loc : Source_Ptr;
       E   : Node_Id;
       N   : Name_Id) return Node_Id;
-   --  Build a call to support procedure N for shared object E (provided by
-   --  the instance of System.Shared_Storage.Shared_Var_Procs associated to E).
+   --  Build a call to support procedure N for shared object E (provided by the
+   --  instance of System.Shared_Storage.Shared_Var_Procs associated to E).
 
    --------------------------------
    -- Build_Shared_Var_Proc_Call --
@@ -87,7 +90,8 @@ package body Exp_Smem is
    function Build_Shared_Var_Proc_Call
      (Loc : Source_Ptr;
       E   : Entity_Id;
-      N   : Name_Id) return Node_Id is
+      N   : Name_Id) return Node_Id
+   is
    begin
       return Make_Procedure_Call_Statement (Loc,
         Name => Make_Selected_Component (Loc,
@@ -96,18 +100,26 @@ package body Exp_Smem is
           Selector_Name => Make_Identifier (Loc, N)));
    end Build_Shared_Var_Proc_Call;
 
-   ---------------------
-   -- Add_Read_Before --
-   ---------------------
+   --------------
+   -- Add_Read --
+   --------------
 
-   procedure Add_Read_Before (N : Node_Id) is
+   procedure Add_Read (N : Node_Id; Call : Node_Id := Empty) is
       Loc : constant Source_Ptr := Sloc (N);
       Ent : constant Node_Id    := Entity (N);
+      SVC : Node_Id;
+
    begin
       if Present (Shared_Var_Procs_Instance (Ent)) then
-         Insert_Action (N, Build_Shared_Var_Proc_Call (Loc, Ent, Name_Read));
+         SVC := Build_Shared_Var_Proc_Call (Loc, Ent, Name_Read);
+
+         if Present (Call) and then Is_Init_Proc (Name (Call)) then
+            Insert_After_And_Analyze (Call, SVC);
+         else
+            Insert_Action (N, SVC);
+         end if;
       end if;
-   end Add_Read_Before;
+   end Add_Read;
 
    -------------------------------
    -- Add_Shared_Var_Lock_Procs --
@@ -121,10 +133,10 @@ package body Exp_Smem is
 
    begin
       --  We have to add Shared_Var_Lock and Shared_Var_Unlock calls around
-      --  the procedure or function call node. First we locate the right
-      --  place to do the insertion, which is the call itself in the
-      --  procedure call case, or else the nearest non subexpression
-      --  node that contains the function call.
+      --  the procedure or function call node. First we locate the right place
+      --  to do the insertion, which is the call itself in the procedure call
+      --  case, or else the nearest non subexpression node that contains the
+      --  function call.
 
       Inode := N;
       while Nkind (Inode) /= N_Procedure_Call_Statement
@@ -135,11 +147,11 @@ package body Exp_Smem is
 
       --  Now insert the Lock and Unlock calls and the read/write calls
 
-      --  Two concerns here. First we are not dealing with the exception
-      --  case, really we need some kind of cleanup routine to do the
-      --  Unlock. Second, these lock calls should be inside the protected
-      --  object processing, not outside, otherwise they can be done at
-      --  the wrong priority, resulting in dead lock situations ???
+      --  Two concerns here. First we are not dealing with the exception case,
+      --  really we need some kind of cleanup routine to do the Unlock. Second,
+      --  these lock calls should be inside the protected object processing,
+      --  not outside, otherwise they can be done at the wrong priority,
+      --  resulting in dead lock situations ???
 
       Build_Full_Name (Obj, Vnm);
 
@@ -171,7 +183,6 @@ package body Exp_Smem is
          Insert_After_And_Analyze (Inode,
            Build_Shared_Var_Proc_Call (Loc, Obj, Name_Write));
       end if;
-
    end Add_Shared_Var_Lock_Procs;
 
    ---------------------
@@ -235,23 +246,41 @@ package body Exp_Smem is
       if Is_Limited_Type (Typ) or else Is_Concurrent_Type (Typ) then
          return;
 
-      --  If we are on the left hand side of an assignment, then we add
-      --  the write call after the assignment.
+      --  If we are on the left hand side of an assignment, then we add the
+      --  write call after the assignment.
 
       elsif On_Lhs_Of_Assignment (N) then
          Add_Write_After (N);
 
-      --  If we are a parameter for an out or in out formal, then put
-      --  the read before and the write after.
+      --  If we are a parameter for an out or in out formal, then in general
+      --  we do:
+
+      --    read
+      --    call
+      --    write
+
+      --  but in the special case of a call to an init proc, we need to first
+      --  call the init proc (to set discriminants), then read (to possibly
+      --  set other components), then write (to record the updated components
+      --  to the backing store):
+
+      --    init-proc-call
+      --    read
+      --    write
 
       elsif Is_Out_Actual (N) then
-         Add_Read_Before (N);
+
+         --  Note: For an init proc call, Add_Read inserts just after the
+         --  call node, and we want to have first the read, then the write,
+         --  so we need to first Add_Write_After, then Add_Read.
+
          Add_Write_After (N);
+         Add_Read (N, Call => Insert_Node);
 
       --  All other cases are simple reads
 
       else
-         Add_Read_Before (N);
+         Add_Read (N);
       end if;
    end Expand_Shared_Passive_Variable;
 
@@ -297,8 +326,7 @@ package body Exp_Smem is
 
       SVP_Instance : constant Entity_Id := Make_Defining_Identifier (Loc,
                        Chars => New_External_Name (Chars (Ent), 'G'));
-      --  Instance of System.Shared_Storage.Shared_Var_Procs associated
-      --  with Ent.
+      --  Instance of Shared_Storage.Shared_Var_Procs associated with Ent
 
       Instantiation : Node_Id;
       --  Package instantiation node for SVP_Instance
@@ -308,9 +336,9 @@ package body Exp_Smem is
    begin
       Build_Full_Name (Ent, Vnm);
 
-      --  We turn off Shared_Passive during construction and analysis of
-      --  the generic package instantiation, to avoid improper attempts to
-      --  process the variable references within these instantiation.
+      --  We turn off Shared_Passive during construction and analysis of the
+      --  generic package instantiation, to avoid improper attempts to process
+      --  the variable references within these instantiation.
 
       Set_Is_Shared_Passive (Ent, False);
 
@@ -376,9 +404,7 @@ package body Exp_Smem is
             return False;
          end if;
 
-      elsif (Nkind (P) = N_Indexed_Component
-               or else
-             Nkind (P) = N_Selected_Component)
+      elsif Nkind_In (P, N_Indexed_Component, N_Selected_Component)
         and then N = Prefix (P)
       then
          return On_Lhs_Of_Assignment (P);

gcc/ada/gnat_rm.texi

@@ -6305,7 +6305,7 @@ is needed for error messages issued by all phases of the compiler.
 Syntax:
 
 @smallexample @c ada
-pragma SPARK_Mode [ (On | Off | Auto) ] ;
+pragma SPARK_Mode [(On | Off)] ;
 @end smallexample
 
 @noindent
@@ -6315,16 +6315,14 @@ language. The pragma is intended for use with formal verification tools
 and has no effect on the generated code.
 
 The SPARK_Mode pragma is used to specify the value of the SPARK_Mode aspect
-(a three-valued aspect having values of On, Off, or Auto) of an entity.
+(either Off or On) of an entity.
 More precisely, it is used to specify the aspect value of a ``section''
 of an entity (the term ``section'' is defined below).
 If a Spark_Mode pragma's (optional) argument is omitted,
 an implicit argument of On is assumed.
 
 A SPARK_Mode pragma may be used as a configuration pragma and then has the
-semantics described below. A SPARK_Mode pragma which is not used as a
-configuration pragma (or an equivalent SPARK_Mode aspect_specification)
-shall not have an argument of Auto.
+semantics described below.
 
 A SPARK_Mode pragma can be used as a local pragma only
 in the following contexts:
@@ -6374,8 +6372,7 @@ completion is defined to have 2 ``sections'': its declaration and its
 completion. Any other construct is defined to have 1 section.
 
 The SPARK_Mode aspect value of an arbitrary section of an arbitrary Ada entity
-or construct is then defined to be the following value (except if this yields
-a result of Auto for a non-package; see below):
+or construct is then defined to be the following value:
 
 @itemize
 
@@ -6392,7 +6389,7 @@ else for any of the visible part or body declarations of a library unit package
 or either section of a library unit subprogram, if there is an applicable
 SPARK_Mode configuration pragma then the value specified by the
 pragma; if no such configuration pragma applies, then an implicit
-specification of Auto is assumed;
+specification of Off is assumed;
 
 @item
 else for any subsequent (i.e., not the first) section of a library unit
@@ -6404,12 +6401,11 @@ or subprogram;
 
 @end itemize
 
-If the above computation yields a result of Auto for any construct other than
-one of the four sections of a package, then a result of On or Off is
-determined instead based on the legality (with respect to the rules of
-SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only
-if the construct is in SPARK 2014. [A SPARK_Mode of
-Auto is therefore only possible for sections of a package.]
+If the above computation does not specify a SPARK_Mode setting for any
+construct other than one of the four sections of a package, then a result of On
+or Off is determined instead based on the legality (with respect to the rules
+of SPARK 2014) of the construct. The construct's SPARK_Mode is On if and only
+if the construct is in SPARK 2014.
 
 If an earlier section of an entity has a Spark_Mode of Off, then the
 Spark_Mode aspect of any later section of that entity shall not be
@@ -12472,7 +12468,7 @@ See A.3.5(3).
 @end cartouche
 @noindent
 @code{Ada.Wide_Characters.Handling.Character_Set_Version} returns
-the string "Unicode 6.2", referring to version 6.2.x of the
+the string "Unicode 4.0", referring to version 4.0 of the
 Unicode specification.
 
 @sp 1