[multiple changes]

2017-09-06  Gary Dismukes  <dismukes@adacore.com>

	* sem_util.adb: Minor reformatting.

2017-09-06  Yannick Moy  <moy@adacore.com>

	* a-comlin.ads (Argument): Add precondition for analysis.

From-SVN: r251770

gcc/ada/ChangeLog

+2017-09-06  Gary Dismukes  <dismukes@adacore.com>
+
+	* sem_util.adb: Minor reformatting.
+
+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* a-comlin.ads (Argument): Add precondition for analysis.
+
 2017-09-06  Yannick Moy  <moy@adacore.com>
 
 	* sem_res.adb (Resolve): Update message for function call as statement.

gcc/ada/a-comlin.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- This specification is derived from the Ada Reference Manual for use with --
 -- GNAT. The copyright notice above, and the license provisions that follow --
@@ -45,7 +45,14 @@ package Ada.Command_Line is
    --
    --  In GNAT: Corresponds to (argc - 1) in C.
 
+   pragma Assertion_Policy (Pre => Ignore);
+   --  We need to ignore the precondition of Argument, below, so that we don't
+   --  raise Assertion_Error. The body raises Constraint_Error. It would be
+   --  cleaner to add "or else raise Constraint_Error" to the precondition, but
+   --  SPARK does not yet support raise expressions.
+
    function Argument (Number : Positive) return String;
+   pragma Precondition (Number <= Argument_Count);
    --  If the external execution environment supports passing arguments to
    --  a program, then Argument returns an implementation-defined value
    --  corresponding to the argument at relative position Number. If Number

gcc/ada/sem_util.adb

@@ -17059,8 +17059,8 @@ package body Sem_Util is
       Formal : Entity_Id;
 
    begin
-      --  Ada 2005 or later, and formals present. The first formal must
-      --  be of  type that supports prefix notation: a controlling argument,
+      --  Ada 2005 or later, and formals present. The first formal must be
+      --  of a type that supports prefix notation: a controlling argument,
       --  a class-wide type, or an access to such.
 
       if Ada_Version >= Ada_2005