[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 785a11a..a8264d6 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+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.

diff --git a/gcc/ada/a-comlin.ads b/gcc/ada/a-comlin.ads
index 42ca589..18695e9 100644 (file)
--- a/gcc/ada/a-comlin.ads
+++ b/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

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 4e03381..0138648 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/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