aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/libgnat
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2020-07-07 11:19:47 +0200
committerPierre-Marie de Rodat <derodat@adacore.com>2020-10-19 05:53:37 -0400
commita6272b85b5f624c5633af243bdf191b8089c892e (patch)
tree195c7d070395688472e5aa657b5c0458d3007c0b /gcc/ada/libgnat
parentb7fd8264143908dbc43bf9a7df7b930306eabbb8 (diff)
downloadgcc-a6272b85b5f624c5633af243bdf191b8089c892e.zip
gcc-a6272b85b5f624c5633af243bdf191b8089c892e.tar.gz
gcc-a6272b85b5f624c5633af243bdf191b8089c892e.tar.bz2
[Ada] Clarify protection offered by preconditions on Ada.Text_IO units
gcc/ada/ * libgnat/a-textio.ads: Update top-level comment.
Diffstat (limited to 'gcc/ada/libgnat')
-rw-r--r--gcc/ada/libgnat/a-textio.ads5
1 files changed, 3 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index 6e5e392..36a4b65 100644
--- 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);