From 62bb542316bd5917977eda6ea89fcaadb09be287 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 6 Sep 2017 12:18:12 +0200 Subject: [PATCH] [multiple changes] 2017-09-06 Gary Dismukes * sem_util.adb: Minor reformatting. 2017-09-06 Yannick Moy * a-comlin.ads (Argument): Add precondition for analysis. From-SVN: r251770 --- gcc/ada/ChangeLog | 8 ++++++++ gcc/ada/a-comlin.ads | 9 ++++++++- gcc/ada/sem_util.adb | 4 ++-- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 785a11a8a1f..a8264d616d9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2017-09-06 Gary Dismukes + + * sem_util.adb: Minor reformatting. + +2017-09-06 Yannick Moy + + * a-comlin.ads (Argument): Add precondition for analysis. + 2017-09-06 Yannick Moy * 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 42ca589da47..18695e91c30 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 4e03381463c..0138648c39a 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 -- 2.30.2