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

[Ada] Add GNAT specific pragmas to the equivalent Assertion_Policy for -gnata

Browse Source 
All assertion pragmas are enabled by default when using -gnata. We need
to add the GNAT specific ones to the list.

gcc/ada/

	* doc/gnat_ugn/building_executable_programs_with_gnat.rst
	(Debugging and Assertion Control): Add GNAT specific assertion
	pragmas to the equivalent Assertion_Policy for the -gnata
	option.
	* gnat_ugn.texi: Regenerate.
This commit is contained in:
Claire Dross 2022-05-24 10:42:46 +02:00 committed by Pierre-Marie de Rodat
parent ddd8892527
commit 82b63eb0f3
2 changed files with 52 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
View File

@ -4331,15 +4331,31 @@ Debugging and Assertion Control
Which is a shorthand for::
pragma Assertion_Policy
(Assert => Check,
Static_Predicate => Check,
Dynamic_Predicate => Check,
Pre => Check,
Pre'Class => Check,
Post => Check,
Post'Class => Check,
Type_Invariant => Check,
Type_Invariant'Class => Check);
-- Ada RM assertion pragmas
(Assert => Check,
Static_Predicate => Check,
Dynamic_Predicate => Check,
Pre => Check,
Pre'Class => Check,
Post => Check,
Post'Class => Check,
Type_Invariant => Check,
Type_Invariant'Class => Check,
Default_Initial_Condition => Check,
-- GNAT specific assertion pragmas
Assert_And_Cut => Check,
Assume => Check,
Contract_Cases => Check,
Debug => Check,
Ghost => Check,
Initial_Condition => Check,
Loop_Invariant => Check,
Loop_Variant => Check,
Postcondition => Check,
Precondition => Check,
Predicate => Check,
Refined_Post => Check,
Subprogram_Variant => Check);
The pragmas ``Assert`` and ``Debug`` normally have no effect and
are ignored. This switch, where ``a`` stands for 'assert', causes

38
gcc/ada/gnat_ugn.texi
View File

@ -21,7 +21,7 @@
@copying
@quotation
GNAT User's Guide for Native Platforms , May 24, 2022
GNAT User's Guide for Native Platforms , Jun 24, 2022
AdaCore
@ -12853,15 +12853,31 @@ Which is a shorthand for:
@example
pragma Assertion_Policy
(Assert => Check,
Static_Predicate => Check,
Dynamic_Predicate => Check,
Pre => Check,
Pre'Class => Check,
Post => Check,
Post'Class => Check,
Type_Invariant => Check,
Type_Invariant'Class => Check);
-- Ada RM assertion pragmas
(Assert => Check,
Static_Predicate => Check,
Dynamic_Predicate => Check,
Pre => Check,
Pre'Class => Check,
Post => Check,
Post'Class => Check,
Type_Invariant => Check,
Type_Invariant'Class => Check,
Default_Initial_Condition => Check,
-- GNAT specific assertion pragmas
Assert_And_Cut => Check,
Assume => Check,
Contract_Cases => Check,
Debug => Check,
Ghost => Check,
Initial_Condition => Check,
Loop_Invariant => Check,
Loop_Variant => Check,
Postcondition => Check,
Precondition => Check,
Predicate => Check,
Refined_Post => Check,
Subprogram_Variant => Check);
@end example
The pragmas @code{Assert} and @code{Debug} normally have no effect and
@ -29249,8 +29265,8 @@ to permit their use in free software.
@printindex ge
@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{ }
@anchor{cf}@w{ }
@anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{ }
@c %**end of body
@bye