[multiple changes]

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

	* exp_ch7.adb: Minor reformatting.

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

	* opt.adb (SPARK_Mode): Default for library units is None rather
	than Off.
	* opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is
	no longer ordered.
	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO
	possibility.
	* snames.ads-tmpl (Name_Auto): Removed, no longer used.

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

	* par-ch5.adb (P_Sequence_Of_Statements): Make entry in
	Suspicious_Labels table if we have identifier; followed by loop
	or block.
	* par-endh.adb (Evaluate_End_Entry): Search Suspicious_Labels table.
	* par.adb (Suspicious_Labels): New table.

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

	* exp_aggr.adb (Check_Bounds): Reason is range check, not
	length check.

2014-01-27  Yannick Moy  <moy@adacore.com>

	* get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for
	reference.
	* lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless
	function now.
	(Add_SPARK_Xrefs): Include references to constants.
	* spark_xrefs.ads Document new character 'c' for references to
	constants.

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

	* exp_smem.adb (Add_Write_After): For a function call, insert write as
	an after action in a transient scope.

From-SVN: r207140

gcc/ada/ChangeLog

 2014-01-27  Thomas Quinot  <quinot@adacore.com>
 
+	* exp_ch7.adb: Minor reformatting.
+
+2014-01-27  Robert Dewar  <dewar@adacore.com>
+
+	* opt.adb (SPARK_Mode): Default for library units is None rather
+	than Off.
+	* opt.ads: Remove AUTO from SPARK_Mode_Type SPARK_Mode_Type is
+	no longer ordered.
+	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Remove AUTO
+	possibility.
+	* snames.ads-tmpl (Name_Auto): Removed, no longer used.
+
+2014-01-27  Robert Dewar  <dewar@adacore.com>
+
+	* par-ch5.adb (P_Sequence_Of_Statements): Make entry in
+	Suspicious_Labels table if we have identifier; followed by loop
+	or block.
+	* par-endh.adb (Evaluate_End_Entry): Search Suspicious_Labels table.
+	* par.adb (Suspicious_Labels): New table.
+
+2014-01-27  Robert Dewar  <dewar@adacore.com>
+
+	* exp_aggr.adb (Check_Bounds): Reason is range check, not
+	length check.
+
+2014-01-27  Yannick Moy  <moy@adacore.com>
+
+	* get_spark_xrefs.adb (Get_SPARK_Xrefs): Accept new type 'c' for
+	reference.
+	* lib-xref-spark_specific.adb (Is_Global_Constant): Remove useless
+	function now.
+	(Add_SPARK_Xrefs): Include references to constants.
+	* spark_xrefs.ads Document new character 'c' for references to
+	constants.
+
+2014-01-27  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_smem.adb (Add_Write_After): For a function call, insert write as
+	an after action in a transient scope.
+
+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.

gcc/ada/exp_aggr.adb

@@ -4141,7 +4141,7 @@ package body Exp_Aggr is
             Insert_Action (N,
               Make_Raise_Constraint_Error (Loc,
                 Condition => Cond,
-                Reason    => CE_Length_Check_Failed));
+                Reason    => CE_Range_Check_Failed));
          end if;
       end Check_Bounds;
 

gcc/ada/exp_ch7.adb

@@ -3612,7 +3612,7 @@ package body Exp_Ch7 is
    --  This procedure is called each time a transient block has to be inserted
    --  that is to say for each call to a function with unconstrained or tagged
    --  result. It creates a new scope on the stack scope in order to enclose
-   --  all transient variables generated
+   --  all transient variables generated.
 
    procedure Establish_Transient_Scope (N : Node_Id; Sec_Stack : Boolean) is
       Loc       : constant Source_Ptr := Sloc (N);

gcc/ada/exp_smem.adb

@@ -25,6 +25,7 @@
 
 with Atree;    use Atree;
 with Einfo;    use Einfo;
+with Exp_Ch7;  use Exp_Ch7;
 with Exp_Ch9;  use Exp_Ch9;
 with Exp_Tss;  use Exp_Tss;
 with Exp_Util; use Exp_Util;
@@ -58,8 +59,10 @@ package body Exp_Smem is
    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).
+   --  statement) or Is_Out_Actual (where it points to the subprogram call).
+   --  When Insert_Node is a function call, establish a transient scope around
+   --  the expression, and insert the write as an after-action of the transient
+   --  scope.
 
    procedure Build_Full_Name (E : Entity_Id; N : out String_Id);
    --  Build the fully qualified string name of a shared variable
@@ -191,12 +194,18 @@ package body Exp_Smem is
 
    procedure Add_Write_After (N : Node_Id) is
       Loc : constant Source_Ptr := Sloc (N);
-      Ent : constant Node_Id    := Entity (N);
-
+      Ent : constant Entity_Id  := Entity (N);
+      Par : constant Node_Id := Insert_Node;
    begin
       if Present (Shared_Var_Procs_Instance (Ent)) then
-         Insert_After_And_Analyze (Insert_Node,
-           Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write));
+         if Nkind (Insert_Node) = N_Function_Call then
+            Establish_Transient_Scope (Insert_Node, Sec_Stack => False);
+            Store_After_Actions_In_Scope (New_List (
+              Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write)));
+         else
+            Insert_After_And_Analyze (Par,
+              Build_Shared_Var_Proc_Call (Loc, Ent, Name_Write));
+         end if;
       end if;
    end Add_Write_After;
 

gcc/ada/get_spark_xrefs.adb

@@ -455,6 +455,7 @@ begin
 
                            pragma Assert
                              (Rtype = 'r' or else
+                              Rtype = 'c' or else
                               Rtype = 'm' or else
                               Rtype = 's');
 

gcc/ada/lib-xref-spark_specific.adb

@@ -334,10 +334,6 @@ package body SPARK_Specific is
          S : Scope_Index) return Boolean;
       --  Check whether entity E is in SPARK_Scope_Table at index S or higher
 
-      function Is_Global_Constant (E : Entity_Id) return Boolean;
-      --  Return True if E is a global constant for which we should ignore
-      --  reads in SPARK.
-
       function Lt (Op1 : Natural; Op2 : Natural) return Boolean;
       --  Comparison function for Sort call
 
@@ -440,14 +436,6 @@ package body SPARK_Specific is
          if Ekind (E) in Overloadable_Kind then
             return Typ = 's';
 
-         --  References to constant objects are not considered in SPARK
-         --  section, as these will be translated as constants in the
-         --  intermediate language for formal verification, and should
-         --  therefore never appear in frame conditions.
-
-         elsif Is_Constant_Object (E) then
-            return False;
-
          --  Objects of Task type or protected type are not SPARK references
 
          elsif Present (Etype (E))
@@ -526,16 +514,6 @@ package body SPARK_Specific is
          return False;
       end Is_Future_Scope_Entity;
 
-      ------------------------
-      -- Is_Global_Constant --
-      ------------------------
-
-      function Is_Global_Constant (E : Entity_Id) return Boolean is
-      begin
-         return Ekind (E) = E_Constant
-           and then Ekind_In (Scope (E), E_Package, E_Package_Body);
-      end Is_Global_Constant;
-
       --------
       -- Lt --
       --------
@@ -726,7 +704,6 @@ package body SPARK_Specific is
               and then SPARK_References (Ref.Typ)
               and then Is_SPARK_Scope (Ref.Ent_Scope)
               and then Is_SPARK_Scope (Ref.Ref_Scope)
-              and then not Is_Global_Constant (Ref.Ent)
               and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
 
               --  Discard references from unknown scopes, e.g. generic scopes
@@ -805,6 +782,7 @@ package body SPARK_Specific is
          declare
             Ref_Entry : Xref_Entry renames Xrefs.Table (Rnums (Refno));
             Ref       : Xref_Key   renames Ref_Entry.Key;
+            Typ       : Character;
 
          begin
             --  If this assertion fails, the scope which we are looking for is
@@ -844,6 +822,17 @@ package body SPARK_Specific is
                Col  := Int (Get_Column_Number (Ref_Entry.Def));
             end if;
 
+            --  References to constant objects are considered specially in
+            --  SPARK section, because these will be translated as constants in
+            --  the intermediate language for formal verification, and should
+            --  therefore never appear in frame conditions.
+
+            if Is_Constant_Object (Ref.Ent) then
+               Typ := 'c';
+            else
+               Typ := Ref.Typ;
+            end if;
+
             SPARK_Xref_Table.Append (
               (Entity_Name => Ref_Name,
                Entity_Line => Line,
@@ -852,7 +841,7 @@ package body SPARK_Specific is
                File_Num    => Dependency_Num (Ref.Lun),
                Scope_Num   => Get_Scope_Num (Ref.Ref_Scope),
                Line        => Int (Get_Logical_Line_Number (Ref.Loc)),
-               Rtype       => Ref.Typ,
+               Rtype       => Typ,
                Col         => Int (Get_Column_Number (Ref.Loc))));
          end;
       end loop;

gcc/ada/opt.adb

@@ -186,7 +186,7 @@ package body Opt is
             Assertions_Enabled       := False;
             Assume_No_Invalid_Values := False;
             Check_Policy_List        := Empty;
-            SPARK_Mode               := Off;
+            SPARK_Mode               := None;
             SPARK_Mode_Pragma        := Empty;
          end if;
 

gcc/ada/opt.ads

@@ -1264,9 +1264,9 @@ package Opt is
    --  GNAT
    --  Set True if a pragma Short_Descriptors applies to the current unit.
 
-   type SPARK_Mode_Type is (None, Off, Auto, On);
-   pragma Ordered (SPARK_Mode_Type);
-   --  Possible legal modes that can be set by aspect/pragma SPARK_Mode
+   type SPARK_Mode_Type is (None, Off, On);
+   --  Possible legal modes that can be set by aspect/pragma SPARK_Mode, as
+   --  well as the value None, which indicates no such pragma/aspect applies.
 
    SPARK_Mode : SPARK_Mode_Type := None;
    --  GNAT

gcc/ada/par-ch5.adb

@@ -506,6 +506,24 @@ package body Ch5 is
                      Scan; -- past semicolon
                      Statement_Required := False;
 
+                     --  Here is the special test for a suspicious label, more
+                     --  accurately a suspicious name, which we think perhaps
+                     --  should have been a label. If next token is one of
+                     --  LOOP, FOR, WHILE, DECLARE, BEGIN, then make an entry
+                     --  in the suspicious label table.
+
+                     if Token = Tok_Loop    or else
+                        Token = Tok_For     or else
+                        Token = Tok_While   or else
+                        Token = Tok_Declare or else
+                        Token = Tok_Begin
+                     then
+                        Suspicious_Labels.Append
+                          ((Proc_Call     => Id_Node,
+                            Semicolon_Loc => Prev_Token_Ptr,
+                            Start_Token   => Token_Ptr));
+                     end if;
+
                   --  Check for case of "go to" in place of "goto"
 
                   elsif Token = Tok_Identifier

gcc/ada/par-endh.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-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- --
@@ -711,17 +711,67 @@ package body Endh is
    ------------------------
 
    procedure Evaluate_End_Entry (SS_Index : Nat) is
+      STE : Scope_Table_Entry renames Scope.Table (SS_Index);
+
    begin
-      Column_OK := (End_Column = Scope.Table (SS_Index).Ecol);
+      Column_OK := (End_Column = STE.Ecol);
 
-      Token_OK  := (End_Type = Scope.Table (SS_Index).Etyp or else
-                     (End_Type = E_Name and then
-                       Scope.Table (SS_Index).Etyp >= E_Name));
+      Token_OK  := (End_Type = STE.Etyp
+                     or else (End_Type = E_Name and then STE.Etyp >= E_Name));
 
       Label_OK := End_Labl_Present
-                    and then
-                      (Same_Label (End_Labl, Scope.Table (SS_Index).Labl)
-                        or else Scope.Table (SS_Index).Labl = Error);
+                    and then (Same_Label (End_Labl, STE.Labl)
+                               or else STE.Labl = Error);
+
+      --  Special case to consider. Suppose we have the suspicious label case,
+      --  e.g. a situation like:
+
+      --    My_Label;
+      --    declare
+      --       ...
+      --    begin
+      --       ...
+      --    end My_Label;
+
+      --  This is the case where we want to use the entry in the suspicous
+      --  label table to flag the semicolon saying it should be a colon.
+
+      --  Label_OK will be false because the label does not match (we have
+      --  My_Label on the end line, and the generated name for the scope). Also
+      --  End_Labl_Present will be True.
+
+      if not Label_OK
+        and then End_Labl_Present
+        and then not Comes_From_Source (Scope.Table (SS_Index).Labl)
+      then
+         --  Here is where we will search the suspicious labels table
+
+         for J in 1 .. Suspicious_Labels.Last loop
+            declare
+               SLE : Suspicious_Label_Entry renames
+                       Suspicious_Labels.Table (J);
+            begin
+               --  See if character name of label matches
+
+               if Chars (Name (SLE.Proc_Call)) = Chars (End_Labl)
+
+                 --  And first token of loop/block identifies this entry
+
+                 and then SLE.Start_Token = STE.Sloc
+               then
+                  --  We have the special case, issue the error message
+
+                  Error_Msg -- CODEFIX
+                    (""";"" should be "":""", SLE.Semicolon_Loc);
+
+                  --  And indicate we consider the Label OK after all
+
+                  Label_OK := True;
+                  exit;
+               end if;
+            end;
+         end loop;
+      end if;
 
       --  Compute setting of Syntax_OK. We definitely have a syntax error
       --  if the Token does not match properly or if P_End_Scan detected

gcc/ada/par.adb

@@ -535,6 +535,66 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is
      Table_Increment      => 100,
      Table_Name           => "Scope");
 
+   ------------------------------------------
+   -- Table for Handling Suspicious Labels --
+   ------------------------------------------
+
+   --  This is a special data structure which is used to deal very spefifically
+   --  with the following error case
+
+   --     label;
+   --     loop
+   --       ...
+   --     end loop label;
+
+   --  Similar cases apply to FOR, WHILE, DECLARE, or BEGIN
+
+   --  In each case the opening line looks like a procedure call because of
+   --  the semicolon. And the end line looks illegal because of an unexpected
+   --  label. If we did nothing special, we would just diagnose the label on
+   --  the end as unexpected. But that does not help point to the real error
+   --  which is that the semicolon after label should be a colon.
+
+   --  To deal with this, we build an entry in the Suspicious_Labels table
+   --  whenever we encounter an identifier followed by a semicolon, followed
+   --  by one of LOOP, FOR, WHILE, DECLARE, BEGIN. Then this entry is used to
+   --  issue the right message when we hit the END that confirms that this was
+   --  a bad label.
+
+   type Suspicious_Label_Entry is record
+      Proc_Call : Node_Id;
+      --  Node for the procedure call statement built for the label; construct
+
+      Semicolon_Loc : Source_Ptr;
+      --  Location of the possibly wrong semicolon
+
+      Start_Token : Source_Ptr;
+      --  Source location of the LOOP, FOR, WHILE, DECLARE, BEGIN token
+   end record;
+
+   package Suspicious_Labels is new Table.Table (
+     Table_Component_Type => Suspicious_Label_Entry,
+     Table_Index_Type     => Int,
+     Table_Low_Bound      => 1,
+     Table_Initial        => 50,
+     Table_Increment      => 100,
+     Table_Name           => "Suspicious_Labels");
+
+   --  Now when we are about to issue a message complaining about an END label
+   --  that should not be there because it appears to end a construct that has
+   --  no label, we first search the suspicious labels table entry, using the
+   --  source location stored in the scope table as a key. If we find a match,
+   --  then we check that the label on the end matches the name in the call,
+   --  and if so, we issue a message saying the semicolon should be a colon.
+
+   --  Quite a bit of work, but really helpful in the case where it helps, and
+   --  the need for this is based on actual experience with tracking down this
+   --  kind of error (the eye often easily mistakes semicolon for colon!)
+
+   --  Note: we actually have enough information to patch up the tree, but
+   --  this may not be worth the effort! Also we could deal with the same
+   --  situation for EXIT with a label, but for now don't bother with that!
+
    ---------------------------------
    -- Parsing Routines by Chapter --
    ---------------------------------

gcc/ada/sem_prag.adb

@@ -18587,7 +18587,7 @@ package body Sem_Prag is
          -- SPARK_Mode --
          ----------------
 
-         --  pragma SPARK_Mode [(On | Off | Auto)];
+         --  pragma SPARK_Mode [(On | Off)];
 
          when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
             Body_Id : Entity_Id;
@@ -18609,9 +18609,6 @@ package body Sem_Prag is
             procedure Check_Library_Level_Entity (E : Entity_Id);
             --  Verify that pragma is applied to library-level entity E
 
-            function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
-            --  Convert a value of type SPARK_Mode_Type to corresponding name
-
             ------------------------------
             -- Check_Pragma_Conformance --
             ------------------------------
@@ -18623,15 +18620,13 @@ package body Sem_Prag is
 
                   --  New mode less restrictive than the established mode
 
-                  if Get_SPARK_Mode_From_Pragma (Old_Pragma) < Mode_Id then
-                     Error_Msg_Name_1 := Mode;
-                     Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1);
-
-                     Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode);
-                     Error_Msg_Sloc   := Sloc (SPARK_Mode_Pragma);
+                  if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off
+                    and then Mode_Id = On
+                  then
                      Error_Msg_N
-                       ("\mode is less restrictive than mode "
-                        & "% defined #", Arg1);
+                       ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1);
+                     Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+                     Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1);
                      raise Pragma_Exit;
                   end if;
                end if;
@@ -18665,28 +18660,6 @@ package body Sem_Prag is
                end if;
             end Check_Library_Level_Entity;
 
-            -------------------------
-            -- Get_SPARK_Mode_Name --
-            -------------------------
-
-            function Get_SPARK_Mode_Name
-              (Id : SPARK_Mode_Type) return Name_Id
-            is
-            begin
-               if Id = On then
-                  return Name_On;
-               elsif Id = Off then
-                  return Name_Off;
-               elsif Id = Auto then
-                  return Name_Auto;
-
-               --  Mode "None" should never be used in error message generation
-
-               else
-                  raise Program_Error;
-               end if;
-            end Get_SPARK_Mode_Name;
-
          --  Start of processing for Do_SPARK_Mode
 
          begin
@@ -18697,7 +18670,7 @@ package body Sem_Prag is
             --  Check the legality of the mode (no argument = ON)
 
             if Arg_Count = 1 then
-               Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
+               Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off);
                Mode := Chars (Get_Pragma_Arg (Arg1));
             else
                Mode := Name_On;
@@ -18732,14 +18705,6 @@ package body Sem_Prag is
             --  The pragma applies to a [library unit] subprogram or package
 
             else
-               --  Mode "Auto" can only be used in a configuration pragma
-
-               if Mode_Id = Auto then
-                  Error_Pragma_Arg
-                    ("mode `Auto` is only allowed when pragma % appears as "
-                     & "a configuration pragma", Arg1);
-               end if;
-
                --  Verify the placement of the pragma with respect to package
                --  or subprogram declarations and detect duplicates.
 
@@ -23513,8 +23478,6 @@ package body Sem_Prag is
          return On;
       elsif N = Name_Off then
          return Off;
-      elsif N = Name_Auto then
-         return Auto;
 
       --  Any other argument is erroneous
 

gcc/ada/snames.ads-tmpl

@@ -688,7 +688,6 @@ package Snames is
    Name_Assertion                      : constant Name_Id := N + $;
    Name_Assertions                     : constant Name_Id := N + $;
    Name_Attribute_Name                 : constant Name_Id := N + $;
-   Name_Auto                           : constant Name_Id := N + $;
    Name_Body_File_Name                 : constant Name_Id := N + $;
    Name_Boolean_Entry_Barriers         : constant Name_Id := N + $;
    Name_By_Any                         : constant Name_Id := N + $;

gcc/ada/spark_xrefs.ads

@@ -177,6 +177,7 @@ package SPARK_Xrefs is
 
    --        m = modification
    --        r = reference
+   --        c = reference to constant object
    --        s = subprogram reference in a static call
 
    --  Special entries for reads and writes to memory reference a special
@@ -229,6 +230,7 @@ package SPARK_Xrefs is
       Rtype : Character;
       --  Indicates type of reference, using code used in ALI file:
       --    r = reference
+      --    c = reference to constant object
       --    m = modification
       --    s = call