[multiple changes]

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

	* par-ch4.adb (P_Name): issue a syntax error in SPARK mode on character
	literal or operator symbol which is prefixed
	* sem_attr.adb (Analyze_Access_Attribute): issue an error in formal
	mode on access attributes.
	* sem_ch4.adb (Analyze_Concatenation_Operand): new procedure to check
	that concatenation operands are properly restricted in formal mode
	(Analyze_Concatenation, Analyze_Concatenation_Rest): call new procedure
	Analyze_Concatenation_Operand. Issue an error in formal mode if the
	result of the concatenation has a type different from String.
	(Analyze_Conditional_Expression, Analyze_Explicit_Dereference,
	Analyze_Quantified_Expression, Analyze_Slice,
	Analyze_Null): issue an error in formal mode on unsupported constructs
	* sem_ch5.adb
	(Analyze_Block_Statement): only issue error on source block statement
	* sem_util.ads, sem_util.adb (Last_Source_Node_In_Sequence): new
	function which returns the last node in a list of nodes for which
	Comes_From_Source returns True, if any
	* sem_ch6.adb (Check_Missing_Return): minor refactoring to use
	Last_Source_Node_In_Sequence
	* sem_ch8.adb (Analyze_Exception_Renaming, Analyze_Generic_Renaming,
	Analyze_Object_Renaming, Analyze_Use_Package): issue an error in formal
	mode on unsupported constructs
	* sem_ch9.adb Do not return after issuing error in formal mode, as the
	rest of the actions may be needed later on since the error is marked as
	not serious.
	* sinfo.ads: Typos in comments.

2011-08-01  Pascal Obry  <obry@adacore.com>

	* projects.texi: Minor editing.

From-SVN: r177057

gcc/ada/ChangeLog

 2011-08-01  Yannick Moy  <moy@adacore.com>
 
+	* par-ch4.adb (P_Name): issue a syntax error in SPARK mode on character
+	literal or operator symbol which is prefixed
+	* sem_attr.adb (Analyze_Access_Attribute): issue an error in formal
+	mode on access attributes.
+	* sem_ch4.adb (Analyze_Concatenation_Operand): new procedure to check
+	that concatenation operands are properly restricted in formal mode
+	(Analyze_Concatenation, Analyze_Concatenation_Rest): call new procedure
+	Analyze_Concatenation_Operand. Issue an error in formal mode if the
+	result of the concatenation has a type different from String.
+	(Analyze_Conditional_Expression, Analyze_Explicit_Dereference,
+	Analyze_Quantified_Expression, Analyze_Slice,
+	Analyze_Null): issue an error in formal mode on unsupported constructs
+	* sem_ch5.adb
+	(Analyze_Block_Statement): only issue error on source block statement
+	* sem_util.ads, sem_util.adb (Last_Source_Node_In_Sequence): new
+	function which returns the last node in a list of nodes for which
+	Comes_From_Source returns True, if any
+	* sem_ch6.adb (Check_Missing_Return): minor refactoring to use
+	Last_Source_Node_In_Sequence
+	* sem_ch8.adb (Analyze_Exception_Renaming, Analyze_Generic_Renaming,
+	Analyze_Object_Renaming, Analyze_Use_Package): issue an error in formal
+	mode on unsupported constructs
+	* sem_ch9.adb Do not return after issuing error in formal mode, as the
+	rest of the actions may be needed later on since the error is marked as
+	not serious.
+	* sinfo.ads: Typos in comments.
+
+2011-08-01  Pascal Obry  <obry@adacore.com>
+
+	* projects.texi: Minor editing.
+
+2011-08-01  Yannick Moy  <moy@adacore.com>
+
 	* err_vars.ads (Error_Msg_Lang, Error_Msg_Langlen): new variables for
 	insertion character ~~
 	* errout.ads, errout.adb (Formal_Error_Msg_...): remove procedures

gcc/ada/par-ch4.adb

@@ -209,8 +209,21 @@ package body Ch4 is
          --  designator.
 
          if Token not in Token_Class_Desig then
+
+            --  Selector name cannot be a character literal in SPARK
+
+            if SPARK_Mode and then Token = Tok_Char_Literal then
+               Error_Msg_SC ("|~~character literal cannot be prefixed");
+            end if;
+
             goto Scan_Name_Extension_Dot;
          else
+            --  Selector name cannot be an operator symbol in SPARK
+
+            if SPARK_Mode and then Token = Tok_Operator_Symbol then
+               Error_Msg_SC ("|~~operator symbol cannot be prefixed");
+            end if;
+
             Prefix_Node := Name_Node;
             Name_Node := New_Node (N_Selected_Component, Prev_Token_Ptr);
             Set_Prefix (Name_Node, Prefix_Node);

gcc/ada/projects.texi

@@ -736,9 +736,10 @@ Notice the three steps described earlier:
 The default output of GPRbuild's execution is kept reasonably simple and easy
 to understand. In particular, some of the less frequently used commands are not
 shown, and some parameters are abbreviated. So it is not possible to rerun the
-effect of the gprbuild command by cut-and-pasting its output. GPRbuild's option
-@code{-v} provides a much more verbose output which includes, among other
-information, more complete compilation, post-compilation and link commands.
+effect of the @command{gprbuild} command by cut-and-pasting its output.
+GPRbuild's option @code{-v} provides a much more verbose output which includes,
+among other information, more complete compilation, post-compilation and link
+commands.
 
 @c ---------------------------------------------
 @node Executable File Names
@@ -1112,6 +1113,7 @@ the search stops:
 @itemize @bullet
 @item First, the file is searched relative to the directory that contains the
   current project file.
+
 @item
 @cindex @code{ADA_PROJECT_PATH}
 @cindex @code{GPR_PROJECT_PATH}
@@ -1119,12 +1121,22 @@ the search stops:
   ^environment variables^logical names^ @b{GPR_PROJECT_PATH} and
   @b{ADA_PROJECT_PATH} (in that order) if they exist. The former is
   recommended, the latter is kept for backward compatibility.
+
 @item Finally, it is searched relative to the default project directories.
-  Such directories depends on the tool used. For @command{gnatmake}, there is
-  one default project directory: @file{<prefix>/lib/gnat/}. In our example,
-  @file{gtkada.gpr} is found in the predefined directory if it was installed at
-  the same root as GNAT.
+  Such directories depends on the tool used. The different locations searched
+  in the specified order are:
+
+  @itemize @bullet
+  @item @file{<prefix>/<target>/lib/gnat}
+  (for @command{gprbuild} only and if option @option{--target} is specified)
+  @item @file{<prefix>/share/gpr/}
+  (for @command{gnatmake} and @command{gprbuild})
+  @item @file{<prefix>/lib/gnat/}
+  (for @command{gnatmake} and @command{gprbuild})
+  @end itemize
 
+  In our example, @file{gtkada.gpr} is found in the predefined directory if
+  it was installed at the same root as GNAT.
 @end itemize
 
 @noindent

gcc/ada/sem_attr.adb

@@ -565,6 +565,14 @@ package body Sem_Attr is
       --  Start of processing for Analyze_Access_Attribute
 
       begin
+         --  Access attribute is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode and then Comes_From_Source (N) then
+            Error_Attr_P ("|~~% attribute is not allowed");
+         end if;
+
+         --  Proceed with analysis
+
          Check_E0;
 
          if Nkind (P) = N_Character_Literal then

gcc/ada/sem_ch4.adb

@@ -67,6 +67,11 @@ package body Sem_Ch4 is
    -- Local Subprograms --
    -----------------------
 
+   procedure Analyze_Concatenation_Operand (N : Node_Id);
+   --  Checks that concatenation operands are properly restricted in SPARK or
+   --  ALFA: each operand must be either a string literal, a static character
+   --  expression, or another concatenation.
+
    procedure Analyze_Concatenation_Rest (N : Node_Id);
    --  Does the "rest" of the work of Analyze_Concatenation, after the left
    --  operand has been analyzed. See Analyze_Concatenation for details.
@@ -369,6 +374,14 @@ package body Sem_Ch4 is
       C        : Node_Id;
 
    begin
+      --  Allocator is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~allocator is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       --  Deal with allocator restrictions
 
       --  In accordance with H.4(7), the No_Allocators restriction only applies
@@ -1344,6 +1357,7 @@ package body Sem_Ch4 is
       --  First analyze L ...
 
       Analyze_Expression (L);
+      Analyze_Concatenation_Operand (L);
 
       --  ... then walk NN back up until we reach N (where we started), calling
       --  Analyze_Concatenation_Rest along the way.
@@ -1353,8 +1367,45 @@ package body Sem_Ch4 is
          exit when NN = N;
          NN := Parent (NN);
       end loop;
+
+      if Formal_Verification_Mode
+        and then Etype (N) /= Standard_String
+      then
+         Error_Msg_F ("|~~result of concatenation should have type String", N);
+      end if;
    end Analyze_Concatenation;
 
+   -----------------------------------
+   -- Analyze_Concatenation_Operand --
+   -----------------------------------
+
+   --  Concatenation is restricted in SPARK or ALFA: each operand must be
+   --  either a string literal, a static character expression, or another
+   --  concatenation. N cannot be a concatenation here as Analyze_Concatenation
+   --  and Analyze_Concatenation_Rest call Analyze_Concatenation_Operand
+   --  separately on each final operand, past concatenation operations.
+
+   procedure Analyze_Concatenation_Operand (N : Node_Id) is
+   begin
+      if Formal_Verification_Mode then
+         if Is_Character_Type (Etype (N)) then
+            if not Is_Static_Expression (N) then
+               Error_Msg_F ("|~~character operand for concatenation should be "
+                            & "static", N);
+            end if;
+         elsif Is_String_Type (Etype (N)) then
+            if Nkind (N) /= N_String_Literal then
+               Error_Msg_F ("|~~string operand for concatenation should be "
+                            & "a literal", N);
+            end if;
+
+         --  Do not issue error on an operand that is neither a character nor
+         --  a string, as the error is issued in Analyze_Concatenation_Rest.
+
+         end if;
+      end if;
+   end Analyze_Concatenation_Operand;
+
    --------------------------------
    -- Analyze_Concatenation_Rest --
    --------------------------------
@@ -1373,6 +1424,7 @@ package body Sem_Ch4 is
 
    begin
       Analyze_Expression (R);
+      Analyze_Concatenation_Operand (R);
 
       --  If the entity is present, the node appears in an instance, and
       --  denotes a predefined concatenation operation. The resulting type is
@@ -1467,6 +1519,14 @@ package body Sem_Ch4 is
          return;
       end if;
 
+      --  Conditional expression is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~conditional expression is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Else_Expr := Next (Then_Expr);
 
       if Comes_From_Source (N) then
@@ -1665,6 +1725,14 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Explicit_Dereference
 
    begin
+      --  Explicit dereference is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~explicit dereference is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Analyze (P);
       Set_Etype (N, Any_Type);
 
@@ -2542,6 +2610,14 @@ package body Sem_Ch4 is
 
    procedure Analyze_Null (N : Node_Id) is
    begin
+      --  Null is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~null is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Set_Etype (N, Any_Access);
    end Analyze_Null;
 
@@ -3226,6 +3302,14 @@ package body Sem_Ch4 is
       Iterator : Node_Id;
 
    begin
+      --  Quantified expression is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~quantified expression is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Set_Etype  (Ent,  Standard_Void_Type);
       Set_Parent (Ent, N);
 
@@ -4252,6 +4336,14 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Slice
 
    begin
+      --  Slice is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~slice is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Analyze (P);
       Analyze (D);
 

gcc/ada/sem_ch5.adb

@@ -808,7 +808,9 @@ package body Sem_Ch5 is
    begin
       --  Block statement is not allowed in SPARK or ALFA
 
-      if Formal_Verification_Mode then
+      if Formal_Verification_Mode
+        and then Comes_From_Source (N)
+      then
          Error_Msg_F ("|~~block statement is not allowed", N);
       end if;
 

gcc/ada/sem_ch6.adb

@@ -1851,25 +1851,17 @@ package body Sem_Ch6 is
 
             if Formal_Verification_Mode then
                declare
-                  Stat : Node_Id := Last (Statements (HSS));
+                  Stat : constant Node_Id :=
+                           Last_Source_Node_In_Sequence (Statements (HSS));
                begin
-                  while Present (Stat) loop
-                     if Comes_From_Source (Stat) then
-                        if not Nkind_In (Nkind (Stat),
-                                         N_Simple_Return_Statement,
-                                         N_Extended_Return_Statement)
-                        then
-                           Error_Msg_F ("|~~last statement in function "
-                                        & "should be RETURN", N);
-                        end if;
-                        exit;
-                     end if;
-
-                     --  Reach before the generated statements at the end of
-                     --  the function.
-
-                     Stat := Prev (Stat);
-                  end loop;
+                  if Present (Stat)
+                    and then not Nkind_In (Nkind (Stat),
+                                           N_Simple_Return_Statement,
+                                           N_Extended_Return_Statement)
+                  then
+                     Error_Msg_F ("|~~last statement in function should "
+                                  & "be RETURN", Stat);
+                  end if;
                end;
 
             elsif Return_Present (Id) then

gcc/ada/sem_ch8.adb

@@ -455,7 +455,7 @@ package body Sem_Ch8 is
    --  private with on E.
 
    procedure Find_Expanded_Name (N : Node_Id);
-   --  The input is a selected component is known to be expanded name. Verify
+   --  The input is a selected component known to be an expanded name. Verify
    --  legality of selector given the scope denoted by prefix, and change node
    --  N into a expanded name with a properly set Entity field.
 
@@ -526,6 +526,14 @@ package body Sem_Ch8 is
       Nam : constant Node_Id := Name (N);
 
    begin
+      --  Exception renaming is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~exception renaming is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Enter_Name (Id);
       Analyze (Nam);
 
@@ -617,6 +625,14 @@ package body Sem_Ch8 is
       Inst  : Boolean   := False; -- prevent junk warning
 
    begin
+      --  Generic renaming is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~generic renaming is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       if Name (N) = Error then
          return;
       end if;
@@ -707,6 +723,14 @@ package body Sem_Ch8 is
    --  Start of processing for Analyze_Object_Renaming
 
    begin
+      --  Object renaming is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~object renaming is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       if Nam = Error then
          return;
       end if;
@@ -2540,6 +2564,15 @@ package body Sem_Ch8 is
    --  Start of processing for Analyze_Use_Package
 
    begin
+      --  Use package is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Error_Msg_F ("|~~use clause is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Set_Hidden_By_Use_Clause (N, No_Elist);
 
       --  Use clause is not allowed in a spec of a predefined package
@@ -5468,6 +5501,18 @@ package body Sem_Ch8 is
       elsif Is_Entity_Name (P) then
          P_Name := Entity (P);
 
+         --  Selector name is restricted in SPARK
+
+         if SPARK_Mode then
+            if Is_Subprogram (P_Name) then
+               Error_Msg_F
+                 ("|~~prefix of expanded name cannot be a subprogram", P);
+            elsif Ekind (P_Name) = E_Loop then
+               Error_Msg_F
+                 ("|~~prefix of expanded name cannot be a loop statement", P);
+            end if;
+         end if;
+
          --  The prefix may denote an enclosing type which is the completion
          --  of an incomplete type declaration.
 

gcc/ada/sem_ch9.adb

@@ -104,7 +104,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~abort statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -182,7 +181,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~accept statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -421,7 +419,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~select statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -475,7 +472,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~select statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -580,7 +576,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~delay statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -606,7 +601,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~delay statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -901,7 +895,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~entry call is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -1360,7 +1353,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~requeue statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -1642,7 +1634,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~select statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis
@@ -2179,7 +2170,6 @@ package body Sem_Ch9 is
 
       if Formal_Verification_Mode then
          Error_Msg_F ("|~~select statement is not allowed", N);
-         return;
       end if;
 
       --  Proceed with analysis

gcc/ada/sem_util.adb

@@ -7981,6 +7981,24 @@ package body Sem_Util is
       end case;
    end Known_To_Be_Assigned;
 
+   ----------------------------------
+   -- Last_Source_Node_In_Sequence --
+   ----------------------------------
+
+   function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id is
+      N : Node_Id := Last (List);
+   begin
+      while Present (N) loop
+         exit when Comes_From_Source (N);
+
+         --  Reach before the generated statements at the end of the function
+
+         N := Prev (N);
+      end loop;
+
+      return N;
+   end Last_Source_Node_In_Sequence;
+
    -------------------
    -- May_Be_Lvalue --
    -------------------

gcc/ada/sem_util.ads

@@ -927,6 +927,10 @@ package Sem_Util is
    --  direction. Cases which may possibly be assignments but are not known to
    --  be may return True from May_Be_Lvalue, but False from this function.
 
+   function Last_Source_Node_In_Sequence (List : List_Id) return Node_Id;
+   --  Returns the last node in List for which Comes_From_Source returns True,
+   --  if any, or Empty otherwise.
+
    function Make_Simple_Return_Statement
      (Sloc       : Source_Ptr;
       Expression : Node_Id := Empty) return Node_Id

gcc/ada/sinfo.ads

@@ -6939,7 +6939,7 @@ package Sinfo is
 
       --  This node is created by the analyzer/expander to handle some
       --  expansion cases, notably short circuit forms where there are
-      --  actions associated with the right hand operand.
+      --  actions associated with the right-hand side operand.
 
       --  The N_Expression_With_Actions node represents an expression with
       --  an associated set of actions (which are executable statements and
@@ -6953,8 +6953,8 @@ package Sinfo is
       --  executing all the actions.
 
       --  Note: if the actions contain declarations, then these declarations
-      --  maybe referenced with in the expression. It is thus appropriate for
-      --  the back end to create a scope that encompasses the construct (any
+      --  may be referenced within the expression. It is thus appropriate for
+      --  the back-end to create a scope that encompasses the construct (any
       --  declarations within the actions will definitely not be referenced
       --  once elaboration of the construct is completed).