[multiple changes]

2014-01-23  Tristan Gingold  <gingold@adacore.com>

	* gnat_rm.texi: Minor editing.

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

	* opt.adb (Set_Opt_Config_Switches): Reset SPARK mode for
	with'ed internal units.
	* sem.adb (Semantics): Save and restore SPARK_Mode[_Pragma].

2014-01-23  Javier Miranda  <miranda@adacore.com>

	* lib-xref.adb (Generate_Reference): As part of processing the
	"end-of-spec" reference generate an extra reference to the first
	private entity of the package.
	* xr_tabls.adb (Add_Reference): No action needed for the extra
	'E' reference associated; similar to the processing of the
	'e' reference.

2014-01-23  Bob Duff  <duff@adacore.com>

	* gnat_ugn.texi: Change "--&pp off" to "--!pp off".

2014-01-23  Ed Schonberg  <schonberg@adacore.com>

	* sem_util.ads, sem_util.adb (Is_Potentially_Unevaluated): new
	predicate to implement rule given in 6.1.1 (20/3).
	* sem_attr.adb (Analyze_Attribute, case 'Old): Reject prefix of
	'Old in a postcondition, if it is potentially unevaluated and
	it is not an entity name.

From-SVN: r206990

gcc/ada/ChangeLog

+2014-01-23  Tristan Gingold  <gingold@adacore.com>
+
+	* gnat_rm.texi: Minor editing.
+
+2014-01-23  Robert Dewar  <dewar@adacore.com>
+
+	* opt.adb (Set_Opt_Config_Switches): Reset SPARK mode for
+	with'ed internal units.
+	* sem.adb (Semantics): Save and restore SPARK_Mode[_Pragma].
+
+2014-01-23  Javier Miranda  <miranda@adacore.com>
+
+	* lib-xref.adb (Generate_Reference): As part of processing the
+	"end-of-spec" reference generate an extra reference to the first
+	private entity of the package.
+	* xr_tabls.adb (Add_Reference): No action needed for the extra
+	'E' reference associated; similar to the processing of the
+	'e' reference.
+
+2014-01-23  Bob Duff  <duff@adacore.com>
+
+	* gnat_ugn.texi: Change "--&pp off" to "--!pp off".
+
+2014-01-23  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_util.ads, sem_util.adb (Is_Potentially_Unevaluated): new
+	predicate to implement rule given in 6.1.1 (20/3).
+	* sem_attr.adb (Analyze_Attribute, case 'Old): Reject prefix of
+	'Old in a postcondition, if it is potentially unevaluated and
+	it is not an entity name.
+
 2014-01-23  Bob Duff  <duff@adacore.com>
 
 	* gnat_ugn.texi: Document the new "--&pp off" feature of gnatpp.

gcc/ada/gnat_rm.texi

@@ -4249,7 +4249,7 @@ pragma Linker_Section (
 @end smallexample
 
 @noindent
-@var{LOCAL_NAME} must refer to an object or a subprogram that is
+@var{LOCAL_NAME} must refer to an object that is
 declared at the library level. This pragma specifies the name of the
 linker section for the given entity. It is equivalent to
 @code{__attribute__((section))} in GNU C and causes @var{LOCAL_NAME} to

gcc/ada/gnat_ugn.texi

@@ -14504,12 +14504,12 @@ Display usage, then exit disregarding all other options.
 @item --pp-off=@var{xxx}
 @cindex @option{--pp-off} @command{gnatpp}
 Use @code{--xxx} as the command to turn off pretty printing, instead
-of the default @code{--&pp off}.
+of the default @code{--!pp off}.
 
 @item --pp-on=@var{xxx}
 @cindex @option{--pp-on} @command{gnatpp}
 Use @code{--xxx} as the command to turn pretty printing back on, instead
-of the default @code{--&pp on}.
+of the default @code{--!pp on}.
 
 @item --pp-old
 @cindex @option{--pp-old} @command{gnatpp}
@@ -14559,22 +14559,36 @@ They provide the detailed descriptions of the switches shown above.
 Pretty printing is highly heuristic in nature, and sometimes doesn't
 do exactly what you want. If you wish to format a certain region of
 code by hand, you can turn off pretty printing in that region by
-surrounding it with the special comments @code{--&pp off} and
-@code{--&pp on}. The text in that region will then be reproduced
+surrounding it with special comments that start with @code{--!pp off}
+and @code{--!pp on}. The text in that region will then be reproduced
 verbatim in the output with no formatting.
 
-To disable pretty printing for the whole file, put @code{--&pp off} at
-the top, with no following @code{--&pp on}.
+To disable pretty printing for the whole file, put @code{--!pp off} at
+the top, with no following @code{--!pp on}.
 
 The comments must appear on a line by themselves, with nothing
-preceding except spaces, and they must appear exactly as shown (case
-sensitive). For example, @code{--&pp off -- Turn off pp because ...}
-will not be recognized as a valid @code{--&pp off} command.
+preceding except spaces. The initial text of the comment must be
+exactly @code{--!pp off} or @code{--!pp on} (case sensitive), but may
+be followed by arbitrary additional text. For example:
+
+@smallexample @c ada
+@cartouche
+package Interrupts is
+   --!pp off -- turn off pretty printing so "Interrupt_Kind" lines up
+   type Interrupt_Kind is
+     (Asynchronous_Interrupt_Kind,
+       Synchronous_Interrupt_Kind,
+             Green_Interrupt_Kind);
+   --!pp on -- reenable pretty printing
+
+   ...
+@end cartouche
+@end smallexample
 
 You can specify different comment strings using the gnatpp
 @code{--pp-off} and @code{--pp-on} switches. For example, if you say
 @code{gnatpp --pp-off=' pp-' *.ad?} then gnatpp will recognize
-comments of the form @code{-- pp-}, instead of @code{--&pp off} for
+comments of the form @code{-- pp-} instead of @code{--!pp off} for
 disabling pretty printing. Note that the leading @code{--} of the
 comment is not included in the argument to these switches.
 

gcc/ada/lib-xref.adb

@@ -1069,6 +1069,27 @@ package body Lib.Xref is
                 Ref_Scope => Empty,
                 Ent_Scope => Empty),
                Ent_Scope_File => No_Unit);
+
+            --  Generate reference to the first private entity
+
+            if Typ = 'e'
+              and then Comes_From_Source (E)
+              and then Nkind (Ent) = N_Defining_Identifier
+              and then (Is_Package_Or_Generic_Package (Ent)
+                         or else Is_Concurrent_Type (Ent))
+              and then Present (First_Private_Entity (E))
+              and then In_Extended_Main_Source_Unit (N)
+            then
+               Add_Entry
+                 ((Ent       => Ent,
+                   Loc       => Sloc (First_Private_Entity (E)),
+                   Typ       => 'E',
+                   Eun       => Get_Source_Unit (Def),
+                   Lun       => Get_Source_Unit (Ref),
+                   Ref_Scope => Empty,
+                   Ent_Scope => Empty),
+                  Ent_Scope_File => No_Unit);
+            end if;
          end if;
       end if;
    end Generate_Reference;

gcc/ada/lib-xref.ads

@@ -175,6 +175,7 @@ package Lib.Xref is
    --              d = discriminant of type
    --              D = object definition
    --              e = end of spec
+   --              E = first private entity
    --              H = abstract type
    --              i = implicit reference
    --              k = implicit reference to parent unit in child unit

gcc/ada/opt.adb

@@ -167,20 +167,24 @@ package body Opt is
          Persistent_BSS_Mode         := False;
          Use_VADS_Size               := False;
          Optimize_Alignment_Local    := True;
-         SPARK_Mode                  := Auto;
 
          --  For an internal unit, assertions/debug pragmas are off unless this
          --  is the main unit and they were explicitly enabled. We also make
-         --  sure we do not assume that values are necessarily valid.
+         --  sure we do not assume that values are necessarily valid and that
+         --  SPARK_Mode is set to its configuration value.
 
          if Main_Unit then
             Assertions_Enabled       := Assertions_Enabled_Config;
             Assume_No_Invalid_Values := Assume_No_Invalid_Values_Config;
             Check_Policy_List        := Check_Policy_List_Config;
+            SPARK_Mode               := SPARK_Mode_Config;
+            SPARK_Mode_Pragma        := SPARK_Mode_Pragma_Config;
          else
             Assertions_Enabled       := False;
             Assume_No_Invalid_Values := False;
             Check_Policy_List        := Empty;
+            SPARK_Mode               := Off;
+            SPARK_Mode_Pragma        := Empty;
          end if;
 
       --  Case of non-internal unit
@@ -203,6 +207,7 @@ package body Opt is
          Optimize_Alignment_Local    := False;
          Persistent_BSS_Mode         := Persistent_BSS_Mode_Config;
          SPARK_Mode                  := SPARK_Mode_Config;
+         SPARK_Mode_Pragma           := SPARK_Mode_Pragma_Config;
          Use_VADS_Size               := Use_VADS_Size_Config;
 
          --  Update consistently the value of Init_Or_Norm_Scalars. The value

gcc/ada/sem.adb

@@ -1311,6 +1311,8 @@ package body Sem is
       S_Inside_A_Generic  : constant Boolean          := Inside_A_Generic;
       S_Outer_Gen_Scope   : constant Entity_Id        := Outer_Generic_Scope;
       S_Style_Check       : constant Boolean          := Style_Check;
+      S_SPARK_Mode        : constant SPARK_Mode_Type  := SPARK_Mode;
+      S_SPARK_Mode_Pragma : constant Node_Id          := SPARK_Mode_Pragma;
 
       Generic_Main : constant Boolean :=
                        Nkind (Unit (Cunit (Main_Unit)))
@@ -1418,7 +1420,6 @@ package body Sem is
       Inside_A_Generic   := False;
       In_Assertion_Expr  := 0;
       In_Spec_Expression := False;
-
       Set_Comes_From_Source_Default (False);
 
       --  Save current config switches and reset then appropriately
@@ -1511,6 +1512,8 @@ package body Sem is
       Inside_A_Generic     := S_Inside_A_Generic;
       Outer_Generic_Scope  := S_Outer_Gen_Scope;
       Style_Check          := S_Style_Check;
+      SPARK_Mode           := S_SPARK_Mode;
+      SPARK_Mode_Pragma    := S_SPARK_Mode_Pragma;
 
       Restore_Opt_Config_Switches (Save_Config_Switches);
 

gcc/ada/sem_attr.adb

@@ -4337,6 +4337,8 @@ package body Sem_Attr is
          --  During pre-analysis, Prag is the enclosing pragma node if any
 
       begin
+         Prag := Empty;
+
          --  Find enclosing scopes, excluding loops
 
          CS := Current_Scope;
@@ -4515,6 +4517,18 @@ package body Sem_Attr is
               ("??attribute Old applied to constant has no effect", P);
          end if;
 
+         --  Check that the prefix of 'Old is an entity, when it appears in
+         --  a postcondition and may be potentially unevaluated (6.1.1 (27/3)).
+
+         if Present (Prag)
+           and then Get_Pragma_Id (Prag) = Pragma_Postcondition
+           and then Is_Potentially_Unevaluated (N)
+           and then not Is_Entity_Name (P)
+         then
+            Error_Msg_N ("prefix that is potentially unevaluated must "
+               & "denote an entity", N);
+         end if;
+
          --  The attribute appears within a pre/postcondition, but refers to
          --  an entity in the enclosing subprogram. If it is a component of
          --  a formal its expansion might generate actual subtypes that may

gcc/ada/sem_util.adb

@@ -10249,6 +10249,48 @@ package body Sem_Util is
       end if;
    end Is_Partially_Initialized_Type;
 
+   --------------------------------
+   -- Is_Potentially_Unevaluated --
+   --------------------------------
+
+   function Is_Potentially_Unevaluated (N : Node_Id) return Boolean is
+      Par  : Node_Id;
+      Expr : Node_Id;
+
+   begin
+      Expr := N;
+      Par  := Parent (N);
+      while not Nkind_In (Par, N_If_Expression,
+                                N_Case_Expression,
+                                N_And_Then,
+                                N_Or_Else,
+                                N_In,
+                                N_Not_In)
+      loop
+         Expr := Par;
+         Par  := Parent (Par);
+         if Nkind (Par) not in N_Subexpr then
+            return False;
+         end if;
+      end loop;
+
+      if Nkind (Par) = N_If_Expression then
+         return Is_Elsif (Par) or else Expr /= First (Expressions (Par));
+
+      elsif Nkind (Par) = N_Case_Expression then
+         return Expr /= Expression (Par);
+
+      elsif Nkind_In (Par, N_And_Then, N_Or_Else) then
+         return Expr = Right_Opnd (Par);
+
+      elsif Nkind_In (Par, N_In, N_Not_In) then
+         return Expr /= Left_Opnd (Par);
+
+      else
+         return False;
+      end if;
+   end Is_Potentially_Unevaluated;
+
    ------------------------------------
    -- Is_Potentially_Persistent_Type --
    ------------------------------------

gcc/ada/sem_util.ads

@@ -1116,6 +1116,9 @@ package Sem_Util is
    --  if Include_Implicit is False, these cases do not count as making the
    --  type be partially initialized.
 
+   function Is_Potentially_Unevaluated (N : Node_Id) return Boolean;
+   --  Predicate to implement definition given in RM 6.1.1 (20/3)
+
    function Is_Potentially_Persistent_Type (T : Entity_Id) return Boolean;
    --  Determines if type T is a potentially persistent type. A potentially
    --  persistent type is defined (recursively) as a scalar type, a non-tagged

gcc/ada/xr_tabls.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1998-2012, 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- --
@@ -431,7 +431,7 @@ package body Xr_Tabls is
                  Decl_Type    => ' ',
                  Is_Parameter => True);
 
-         when 'e' | 'z' | 't' | 'p' | 'P' | 'k' | 'd' =>
+         when 'e' | 'E' | 'z' | 't' | 'p' | 'P' | 'k' | 'd' =>
             return;
 
          when others    =>