The runtime checks for overlaping actual parameters, which gets enabled
by the -gnateA switch, were introduced to combine proof and test for the
antialiasing rules of SPARK.
The original implementation of these checks contained few mistakes which
resulted in spurious compilation errors. These are now fixed, but the
current implementation no longer matches the aliasing rules from the
SPARK RM 6.4.2; instead, it is based on the Ada RM 6.2(12/3).
This patch documents the current behaviour in the GNAT User's Guide.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* doc/gnat_ugn/building_executable_programs_with_gnat.rst
(gnateA): This switch no longer looks at the formal parameter
type being composite (as originally mandated by SPARK), but in
the parameter passing mechanism being not specified (as
currently mandated by Ada).
* gnat_ugn.texi: Regenerate.diff --git a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
--- a/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
+++ b/gcc/ada/doc/gnat_ugn/building_executable_programs_with_gnat.rst
@@ -1497,9 +1497,10 @@ Alphabetical List of All Switches
:switch:`-gnateA`
Check that the actual parameters of a subprogram call are not aliases of one
- another. To qualify as aliasing, the actuals must denote objects of a composite
- type, their memory locations must be identical or overlapping, and at least one
- of the corresponding formal parameters must be of mode OUT or IN OUT.
+ another. To qualify as aliasing, their memory locations must be identical or
+ overlapping, at least one of the corresponding formal parameters must be of
+ mode OUT or IN OUT, and at least one of the corresponding formal parameters
+ must have its parameter passing mechanism not specified.
.. code-block:: ada
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -8933,9 +8933,10 @@ also suppresses generation of cross-reference information
@item @code{-gnateA}
Check that the actual parameters of a subprogram call are not aliases of one
-another. To qualify as aliasing, the actuals must denote objects of a composite
-type, their memory locations must be identical or overlapping, and at least one
-of the corresponding formal parameters must be of mode OUT or IN OUT.
+another. To qualify as aliasing, their memory locations must be identical or
+overlapping, at least one of the corresponding formal parameters must be of
+mode OUT or IN OUT, and at least one of the corresponding formal parameters
+must have its parameter passing mechanism not specified.
@example
type Rec_Typ is record
