These preconditions are used in particular for analysis by SPARK tools.
It is thus important that they precisely convey which errors they allow
detecting, in callers of Ada.Text_IO. Here, Layout_Error cannot be
detected in a number of cases.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-textio.ads: Update top-level comment.diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
--- a/gcc/ada/libgnat/a-textio.ads
+++ b/gcc/ada/libgnat/a-textio.ads
@@ -36,8 +36,9 @@
-- Preconditions in this unit are meant for analysis only, not for run-time
-- checking, so that the expected exceptions are raised. This is enforced by
-- setting the corresponding assertion policy to Ignore. These preconditions
--- are partial and protect against Status_Error, Mode_Error, and Layout_Error,
--- but not against other types of errors.
+-- are partial. They protect fully against Status_Error and Mode_Error,
+-- partially against Layout_Error (see SPARK User's Guide for details), and
+-- not against other types of errors.
pragma Assertion_Policy (Pre => Ignore);
