OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Fix casing from GNATProve to GNATprove

Browse Source 
2020-06-17  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* doc/gnat_rm/implementation_defined_pragmas.rst, lib-writ.ads,
	par-prag.adb, sem_ch12.adb, sem_ch8.adb, sem_prag.adb: Fix
	casing of GNATprove.
	* gnat_rm.texi: Regenerate.
This commit is contained in:
Piotr Trojanek 2020-04-10 19:33:44 +02:00 committed by Pierre-Marie de Rodat
parent 4ffefb704a
commit 137adce390
7 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
gcc/ada/doc/gnat_rm/implementation_defined_pragmas.rst
View File

@ -7421,7 +7421,7 @@ Syntax:
DETAILS ::= static_string_EXPRESSION
DETAILS ::= On | Off, static_string_EXPRESSION
TOOL_NAME ::= GNAT | GNATProve
TOOL_NAME ::= GNAT | GNATprove
REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}

4
gcc/ada/gnat_rm.texi
View File

@ -21,7 +21,7 @@
@copying
@quotation
GNAT Reference Manual , May 05, 2020
GNAT Reference Manual , May 13, 2020
AdaCore
@ -8902,7 +8902,7 @@ DETAILS ::= On | Off, local_NAME
DETAILS ::= static_string_EXPRESSION
DETAILS ::= On | Off, static_string_EXPRESSION
TOOL_NAME ::= GNAT | GNATProve
TOOL_NAME ::= GNAT | GNATprove
REASON ::= Reason => STRING_LITERAL @{& STRING_LITERAL@}
@end example

2
gcc/ada/lib-writ.ads
View File

@ -1051,7 +1051,7 @@ package Lib.Writ is
procedure Write_ALI (Object : Boolean);
-- This procedure writes the library information for the current main unit
-- The Object parameter is true if an object file is created, and false
-- otherwise. Note that the pseudo-object file generated in GNATProve mode
-- otherwise. Note that the pseudo-object file generated in GNATprove mode
-- does count as an object file from this point of view.
--
-- Note: in the case where we are not generating code (-gnatc mode), this

2
gcc/ada/par-prag.adb
View File

@ -1109,7 +1109,7 @@ begin
-- DETAILS ::= static_string_EXPRESSION
-- DETAILS ::= On | Off, static_string_EXPRESSION
-- TOOL_NAME ::= GNAT | GNATProve
-- TOOL_NAME ::= GNAT | GNATprove
-- REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}

4
gcc/ada/sem_ch12.adb
View File

@ -1718,7 +1718,7 @@ package body Sem_Ch12 is
Assoc_List);
-- For a defaulted in_parameter, create an entry in the
-- the list of defaulted actuals, for GNATProve use. Do
-- the list of defaulted actuals, for GNATprove use. Do
-- not included these defaults for an instance nested
-- within a generic, because the defaults are also used
-- in the analysis of the enclosing generic, and only
@ -1928,7 +1928,7 @@ package body Sem_Ch12 is
end if;
-- If this is a nested generic, preserve default for later
-- instantiations. We do this as well for GNATProve use,
-- instantiations. We do this as well for GNATprove use,
-- so that the list of generic associations is complete.
if No (Match) and then Box_Present (Formal) then

4
gcc/ada/sem_ch8.adb
View File

@ -7162,10 +7162,10 @@ package body Sem_Ch8 is
-- is an array type we may already have a usable subtype for it, so we
-- can use it rather than generating a new one, because the bounds
-- will be the values of the discriminants and not discriminant refs.
-- This simplifies value tracing in GNATProve. For consistency, both
-- This simplifies value tracing in GNATprove. For consistency, both
-- the entity name and the subtype come from the constrained component.
-- This is only used in GNATProve mode: when generating code it may be
-- This is only used in GNATprove mode: when generating code it may be
-- necessary to create an itype in the scope of use of the selected
-- component, e.g. in the context of a expanded record equality.

2
gcc/ada/sem_prag.adb
View File

@ -25258,7 +25258,7 @@ package body Sem_Prag is
-- DETAILS ::= static_string_EXPRESSION
-- DETAILS ::= On | Off, static_string_EXPRESSION
-- TOOL_NAME ::= GNAT | GNATProve
-- TOOL_NAME ::= GNAT | GNATprove
-- REASON ::= Reason => STRING_LITERAL {& STRING_LITERAL}