[multiple changes]

2011-08-01  Yannick Moy  <moy@adacore.com>

	* sem_util.ads, sem_util.adb, par.adb, par_util.adb
	(Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
	procedures out of these packages.
	* errout.ads, errout.adb 
	(Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
	procedures in of this package
	(Formal_Error_Msg_NE): new procedure for wrapper on Error_Msg_NE
	* par-ch5.adb (Parse_Decls_Begin_End): issue syntax error in SPARK mode
	on misplaced later vs initial declarations, like in Ada 83
	* sem_attr.adb (Processing for Analyze_Attribute): issue error in
	formal mode on attribute of private type whose full type declaration
	is not visible
	* sem_ch3.adb (Analyze_Declarations): issue error in formal mode on a
	package declaration inside a package specification
	(Analyze_Full_Type_Declaration): issue error in formal mode on
	controlled type or discriminant type
	* sem_ch6.adb (Analyze_Subprogram_Specification): only issue error on
	user-defined operator means that it should come from the source
	(New_Overloaded_Entity): issue error in formal mode on overloaded
	entity.
	* sem_ch6.ads, sem_ch13.ads: typos in comments.

2011-08-01  Thomas Quinot  <quinot@adacore.com>

	* atree.adb: Minor reformatting.
	* checks.adb: Minor reformatting.

From-SVN: r177052

gcc/ada/ChangeLog

+2011-08-01  Yannick Moy  <moy@adacore.com>
+
+	* sem_util.ads, sem_util.adb, par.adb, par_util.adb
+	(Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
+	procedures out of these packages.
+	* errout.ads, errout.adb 
+	(Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move
+	procedures in of this package
+	(Formal_Error_Msg_NE): new procedure for wrapper on Error_Msg_NE
+	* par-ch5.adb (Parse_Decls_Begin_End): issue syntax error in SPARK mode
+	on misplaced later vs initial declarations, like in Ada 83
+	* sem_attr.adb (Processing for Analyze_Attribute): issue error in
+	formal mode on attribute of private type whose full type declaration
+	is not visible
+	* sem_ch3.adb (Analyze_Declarations): issue error in formal mode on a
+	package declaration inside a package specification
+	(Analyze_Full_Type_Declaration): issue error in formal mode on
+	controlled type or discriminant type
+	* sem_ch6.adb (Analyze_Subprogram_Specification): only issue error on
+	user-defined operator means that it should come from the source
+	(New_Overloaded_Entity): issue error in formal mode on overloaded
+	entity.
+	* sem_ch6.ads, sem_ch13.ads: typos in comments.
+
+2011-08-01  Thomas Quinot  <quinot@adacore.com>
+
+	* atree.adb: Minor reformatting.
+	* checks.adb: Minor reformatting.
+
 2011-08-01  Vincent Celier  <celier@adacore.com>
 
 	* s-parame-vms-ia64.ads: Fix typo in comment

gcc/ada/atree.adb

@@ -1196,14 +1196,14 @@ package body Atree is
          Nodes.Table (New_Id).Link := Empty_List_Or_Node;
          Nodes.Table (New_Id).In_List := False;
 
-         --  If the original is marked as a rewrite insertion, then unmark
-         --  the copy, since we inserted the original, not the copy.
+         --  If the original is marked as a rewrite insertion, then unmark the
+         --  copy, since we inserted the original, not the copy.
 
          Nodes.Table (New_Id).Rewrite_Ins := False;
          pragma Debug (New_Node_Debugging_Output (New_Id));
 
          --  Clear Is_Overloaded since we cannot have semantic interpretations
-         --  of this new node
+         --  of this new node.
 
          if Nkind (Source) in N_Subexpr then
             Set_Is_Overloaded (New_Id, False);

gcc/ada/checks.adb

@@ -4560,6 +4560,10 @@ package body Checks is
       function Entity_Of_Prefix return Entity_Id;
       --  Returns the entity of the prefix of N (or Empty if not found)
 
+      ----------------------
+      -- Entity_Of_Prefix --
+      ----------------------
+
       function Entity_Of_Prefix return Entity_Id is
          P : Node_Id := Prefix (N);
       begin
@@ -4583,6 +4587,8 @@ package body Checks is
       A_Ent : constant Entity_Id  := Entity_Of_Prefix;
       Sub   : Node_Id;
 
+   --  Start of processing for Generate_Index_Checks
+
    begin
       --  Ignore call if the prefix is not an array since we have a serious
       --  error in the sources. Ignore it also if index checks are suppressed
@@ -4599,7 +4605,7 @@ package body Checks is
       --  Generate a raise of constraint error with the appropriate reason and
       --  a condition of the form:
 
-      --    Base_Type(Sub) not in array'range (subscript)
+      --    Base_Type (Sub) not in Array'Range (Subscript)
 
       --  Note that the reason we generate the conversion to the base type here
       --  is that we definitely want the range check to take place, even if it
@@ -4627,7 +4633,7 @@ package body Checks is
                           Duplicate_Subexpr_Move_Checks (Sub)),
                       Right_Opnd =>
                         Make_Attribute_Reference (Loc,
-                          Prefix => New_Reference_To (Etype (A), Loc),
+                          Prefix         => New_Reference_To (Etype (A), Loc),
                           Attribute_Name => Name_Range)),
                  Reason => CE_Index_Check_Failed));
          end if;
@@ -4680,7 +4686,8 @@ package body Checks is
                   then
                      Range_N :=
                        Make_Attribute_Reference (Loc,
-                         Prefix => New_Reference_To (Etype (A_Idx), Loc),
+                         Prefix         =>
+                           New_Reference_To (Etype (A_Idx), Loc),
                          Attribute_Name => Name_Range);
 
                   --  For arrays with non-constant bounds we cannot generate

gcc/ada/errout.adb

@@ -1402,6 +1402,49 @@ package body Errout is
       return S;
    end First_Sloc;
 
+   ----------------------
+   -- Formal_Error_Msg --
+   ----------------------
+
+   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is
+   begin
+      pragma Assert (Formal_Verification_Mode);
+      Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location);
+   end Formal_Error_Msg;
+
+   ------------------------
+   -- Formal_Error_Msg_N --
+   ------------------------
+
+   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is
+   begin
+      pragma Assert (Formal_Verification_Mode);
+      Error_Msg_N ("(" & Formal_Language & ") " & Msg, N);
+   end Formal_Error_Msg_N;
+
+   -------------------------
+   -- Formal_Error_Msg_NE --
+   -------------------------
+
+   procedure Formal_Error_Msg_NE
+     (Msg : String;
+      N   : Node_Or_Entity_Id;
+      E   : Node_Or_Entity_Id) is
+   begin
+      pragma Assert (Formal_Verification_Mode);
+      Error_Msg_NE ("(" & Formal_Language & ") " & Msg, N, E);
+   end Formal_Error_Msg_NE;
+
+   -------------------------
+   -- Formal_Error_Msg_SP --
+   -------------------------
+
+   procedure Formal_Error_Msg_SP (Msg : String) is
+   begin
+      pragma Assert (Formal_Verification_Mode);
+      Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
+   end Formal_Error_Msg_SP;
+
    ----------------
    -- Initialize --
    ----------------

gcc/ada/errout.ads

@@ -735,6 +735,25 @@ package Errout is
    --  where the expression is parenthesized, an attempt is made to include
    --  the parentheses (i.e. to return the location of the initial paren).
 
+   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr);
+   --  Wrapper on Error_Msg which adds a prefix to Msg giving the name of
+   --  the formal language analyzed (spark or alfa)
+
+   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id);
+   --  Wrapper on Error_Msg_N which adds a prefix to Msg giving the name of
+   --  the formal language analyzed (spark or alfa)
+
+   procedure Formal_Error_Msg_NE
+     (Msg : String;
+      N   : Node_Or_Entity_Id;
+      E   : Node_Or_Entity_Id);
+   --  Wrapper on Error_Msg_NE which adds a prefix to Msg giving the name of
+   --  the formal language analyzed (spark or alfa)
+
+   procedure Formal_Error_Msg_SP (Msg : String);
+   --  Wrapper on Error_Msg_SP which adds a prefix to Msg giving the name of
+   --  the formal language analyzed (spark or alfa)
+
    procedure Purge_Messages (From : Source_Ptr; To : Source_Ptr)
      renames Erroutc.Purge_Messages;
    --  All error messages whose location is in the range From .. To (not

gcc/ada/par-ch5.adb

@@ -2110,9 +2110,12 @@ package body Ch5 is
    begin
       Decls := P_Declarative_Part;
 
-      --  Check for misplacement of later vs basic declarations in Ada 83
+      --  Check for misplacement of later vs basic declarations in Ada 83.
+      --  The same is true for the SPARK mode: although SPARK 95 removes
+      --  the distinction between initial and later declarative items,
+      --  the distinction remains in the Examiner. (JB01-005)
 
-      if Ada_Version = Ada_83 then
+      if Ada_Version = Ada_83 or else SPARK_Mode then
          Decl := First (Decls);
 
          --  Loop through sequence of basic declarative items
@@ -2139,6 +2142,11 @@ package body Ch5 is
                         Error_Msg_Sloc := Body_Sloc;
                         Error_Msg_N
                           ("(Ada 83) decl cannot appear after body#", Decl);
+                     else
+                        pragma Assert (SPARK_Mode);
+                        Error_Msg_Sloc := Body_Sloc;
+                        Formal_Error_Msg_N
+                          ("decl cannot appear after body#", Decl);
                      end if;
                   end if;
 

gcc/ada/par-util.adb

@@ -377,16 +377,6 @@ package body Util is
       null;
    end Discard_Junk_Node;
 
-   -------------------------
-   -- Formal_Error_Msg_SP --
-   -------------------------
-
-   procedure Formal_Error_Msg_SP (Msg : String) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg_SP ("(" & Formal_Language & ") " & Msg);
-   end Formal_Error_Msg_SP;
-
    ------------
    -- Ignore --
    ------------

gcc/ada/par.adb

@@ -1158,10 +1158,6 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is
       --  the argument. A typical use is to skip by some junk that is not
       --  expected in the current context.
 
-      procedure Formal_Error_Msg_SP (Msg : String);
-      --  Wrapper on Errout.Error_Msg_SP which adds a prefix to Msg giving
-      --  the name of the formal language analyzed (spark or alfa)
-
       procedure Ignore (T : Token_Type);
       --  If current token matches T, then give an error message and skip
       --  past it, otherwise the call has no effect at all. T may be any

gcc/ada/sem_attr.adb

@@ -2055,6 +2055,20 @@ package body Sem_Attr is
          end if;
       end if;
 
+      --  In SPARK or ALFA, attributes of private types are only allowed if
+      --  the full type declaration is visible
+
+      if Formal_Verification_Mode
+        and then Is_Entity_Name (P)
+        and then Is_Type (Entity (P))
+        and then Is_Private_Type (P_Type)
+        and then not In_Open_Scopes (Scope (P_Type))
+        and then not In_Spec_Expression
+      then
+         Formal_Error_Msg_NE
+           ("invisible attribute of}", N, First_Subtype (P_Type));
+      end if;
+
       --  Remaining processing depends on attribute
 
       case Attr_Id is

gcc/ada/sem_ch13.ads

@@ -40,9 +40,9 @@ package Sem_Ch13 is
      (N : Node_Id;
       E : Entity_Id;
       L : List_Id);
-   --  This procedure is called to analyze aspect specifications for node N. E
-   --  is the corresponding entity declared by the declaration node N, and L is
-   --  the list of aspect specifications for this node. If L is No_List, the
+   --  This procedure is called to analyze aspect specifications for node N.
+   --  E is the corresponding entity declared by the declaration node N, and L
+   --  is the list of aspect specifications for this node. If L is No_List, the
    --  call is ignored. Note that we can't use a simpler interface of just
    --  passing the node N, since the analysis of the node may cause it to be
    --  rewritten to a node not permitting aspect specifications.

gcc/ada/sem_ch3.adb

@@ -2027,6 +2027,17 @@ package body Sem_Ch3 is
       D := First (L);
       while Present (D) loop
 
+         --  Package specification cannot contain a package declaration in
+         --  SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Nkind (D) = N_Package_Declaration
+           and then Nkind (Parent (L)) = N_Package_Specification
+         then
+            Formal_Error_Msg_N ("package specification cannot contain "
+                                & "a package declaration", D);
+         end if;
+
          --  Complete analysis of declaration
 
          Analyze (D);
@@ -2347,6 +2358,21 @@ package body Sem_Ch3 is
          return;
       end if;
 
+      if Formal_Verification_Mode then
+
+         --  Controlled type is not allowed in SPARK and ALFA
+
+         if Is_Visibly_Controlled (T) then
+            Formal_Error_Msg_N ("controlled type is not allowed", N);
+         end if;
+
+         --  Discriminant type is not allowed in SPARK and ALFA
+
+         if Present (Discriminant_Specifications (N)) then
+            Formal_Error_Msg_N ("discriminant type is not allowed", N);
+         end if;
+      end if;
+
       --  Some common processing for all types
 
       Set_Depends_On_Private (T, Has_Private_Component (T));

gcc/ada/sem_ch6.adb

@@ -3072,6 +3072,7 @@ package body Sem_Ch6 is
       --  User-defined operator is not allowed in SPARK or ALFA
 
       if Formal_Verification_Mode
+        and then Comes_From_Source (N)
         and then Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
       then
          Formal_Error_Msg_N ("user-defined operator is not allowed", N);
@@ -8493,6 +8494,15 @@ package body Sem_Ch6 is
          Check_Overriding_Indicator
            (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
 
+         --  Overloading is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Comes_From_Source (S)
+         then
+            Error_Msg_Sloc := Sloc (Homonym (S));
+            Formal_Error_Msg_N ("overloading not allowed with entity#", S);
+         end if;
+
          --  If S is a derived operation for an untagged type then by
          --  definition it's not a dispatching operation (even if the parent
          --  operation was dispatching), so we don't call

gcc/ada/sem_ch6.ads

@@ -205,7 +205,7 @@ package Sem_Ch6 is
    --  Process new overloaded entity. Overloaded entities are created by
    --  enumeration type declarations, subprogram specifications, entry
    --  declarations, and (implicitly) by type derivations. Derived_Type non-
-   --  Empty indicates that this is subprogram derived for that type.
+   --  Empty indicates that this is a subprogram derived for that type.
 
    procedure Process_Formals (T : List_Id; Related_Nod : Node_Id);
    --  Enter the formals in the scope of the subprogram or entry, and

gcc/ada/sem_util.adb

@@ -9,7 +9,7 @@
 --          Copyright (C) 1992-2011, 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- --
+-- terms of the  GNU Genconflieral Public License as published  by the Free Soft- --
 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
@@ -3644,26 +3644,6 @@ package body Sem_Util is
       end if;
    end First_Actual;
 
-   ----------------------
-   -- Formal_Error_Msg --
-   ----------------------
-
-   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location);
-   end Formal_Error_Msg;
-
-   ------------------------
-   -- Formal_Error_Msg_N --
-   ------------------------
-
-   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is
-   begin
-      pragma Assert (Formal_Verification_Mode);
-      Error_Msg_N ("(" & Formal_Language & ") " & Msg, N);
-   end Formal_Error_Msg_N;
-
    -----------------------
    -- Gather_Components --
    -----------------------

gcc/ada/sem_util.ads

@@ -407,14 +407,6 @@ package Sem_Util is
    --  is always the expression (not the N_Parameter_Association nodes,
    --  even if named association is used).
 
-   procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr);
-   --  Wrapper on Errout.Error_Msg which adds a prefix to Msg giving
-   --  the name of the formal language analyzed (spark or alfa)
-
-   procedure Formal_Error_Msg_N (Msg : String; N : Node_Id);
-   --  Wrapper on Errout.Error_Msg_N which adds a prefix to Msg giving
-   --  the name of the formal language analyzed (spark or alfa)
-
    procedure Gather_Components
      (Typ           : Entity_Id;
       Comp_List     : Node_Id;