diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-06 12:18:12 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2017-09-06 12:18:12 +0200 |
| commit | 62bb542316bd5917977eda6ea89fcaadb09be287 (patch) | |
| tree | 0b160117718ff84865c6fff0c05b51698f6e9898 /gcc/ada | |
| parent | 95edbf5e5fb2c57ceda70cdf277d9b7655c1796e (diff) | |
| download | gcc-62bb542316bd5917977eda6ea89fcaadb09be287.zip gcc-62bb542316bd5917977eda6ea89fcaadb09be287.tar.gz gcc-62bb542316bd5917977eda6ea89fcaadb09be287.tar.bz2 | |
[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
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | gcc/ada/a-comlin.ads | 9 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 4 |
3 files changed, 18 insertions, 3 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 785a11a..a8264d6 100644 --- 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 --- 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 --- 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 |