diff --git a/gcc/ada/doc/gnat_rm/security_hardening_features.rst b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
index d7c02b9..ad165cd 100644
--- a/gcc/ada/doc/gnat_rm/security_hardening_features.rst
+++ b/gcc/ada/doc/gnat_rm/security_hardening_features.rst
@@ -383,11 +383,127 @@
 least one of its predecessors, and at least one of its successors, are
 also marked as visited.
 
-Verification is performed just before returning.  Subprogram
-executions that complete by raising or propagating an exception bypass
-verification-and-return points.  A subprogram that can only complete
-by raising or propagating an exception may have instrumentation
-disabled altogether.
+Verification is performed just before a subprogram returns.  The
+following fragment:
+
+.. code-block:: ada
+
+   if X then
+     Y := F (Z);
+     return;
+   end if;
+
+
+gets turned into:
+
+.. code-block:: ada
+
+   type Visited_Bitmap is array (1..N) of Boolean with Pack;
+   Visited : aliased Visited_Bitmap := (others => False);
+   --  Bitmap of visited blocks.  N is the basic block count.
+   [...]
+   --  Basic block #I
+   Visited(I) := True;
+   if X then
+     --  Basic block #J
+     Visited(J) := True;
+     Y := F (Z);
+     CFR.Check (N, Visited'Access, CFG'Access);
+     --  CFR is a hypothetical package whose Check procedure calls
+     --  libgcc's __hardcfr_check, that traps if the Visited bitmap
+     --  does not hold a valid path in CFG, the run-time
+     --  representation of the control flow graph in the enclosing
+     --  subprogram.
+     return;
+   end if;
+   --  Basic block #K
+   Visited(K) := True;
+
+
+Verification would also be performed before tail calls, if any
+front-ends marked them as mandatory or desirable, but none do.
+Regular calls are optimized into tail calls too late for this
+transformation to act on it.
+
+In order to avoid adding verification after potential tail calls,
+which would prevent tail-call optimization, we recognize returning
+calls, i.e., calls whose result, if any, is returned by the calling
+subprogram to its caller immediately after the call returns.
+Verification is performed before such calls, whether or not they are
+ultimately optimized to tail calls.  This behavior is enabled by
+default whenever sibcall optimization is enabled (see
+:switch:`-foptimize-sibling-calls`); it may be disabled with
+:switch:`-fno-hardcfr-check-returning-calls`, or enabled with
+:switch:`-fhardcfr-check-returning-calls`, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     P (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return;
+
+or:
+
+.. code-block:: ada
+
+     --  CFR.Check here, with -fhardcfr-check-returning-calls.
+     R := F (X);
+     --  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+     return R;
+
+
+Any subprogram from which an exception may escape, i.e., that may
+raise or propagate an exception that isn't handled internally, is
+conceptually enclosed by a cleanup handler that performs verification,
+unless this is disabled with :switch:`-fno-hardcfr-check-exceptions`.
+With this feature enabled, a subprogram body containing:
+
+.. code-block:: ada
+
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+
+
+gets modified as follows:
+
+.. code-block:: ada
+
+   begin
+     --  ...
+       Y := F (X);  -- May raise exceptions.
+     --  ...
+       raise E;  -- Not handled internally.
+     --  ...
+   exception
+     when others =>
+       CFR.Check (N, Visited'Access, CFG'Access);
+       raise;
+   end;
+
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+:switch:`-fhardcfr-check-noreturn-calls=nothrow`, or all of them, with
+:switch:`-fhardcfr-check-noreturn-calls=always`.  The default is
+:switch:`-fhardcfr-check-noreturn-calls=never` for this feature, that
+disables checking before No_Return calls.
+
+When a No_Return call returns control to its caller through an
+exception, verification may have already been performed before the
+call, if :switch:`-fhardcfr-check-noreturn-calls=always` is in effect.
+The compiler arranges for already-checked No_Return calls without a
+preexisting handler to bypass the implicitly-added cleanup handler and
+thus the redundant check, but a local exception or cleanup handler, if
+present, will modify the set of visited blocks, and checking will take
+place again when the caller reaches the next verification point,
+whether it is a return or reraise statement after the exception is
+otherwise handled, or even another No_Return call.
 
 The instrumentation for hardening with control flow redundancy can be
 observed in dump files generated by the command-line option
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index fbd8bb8..83458cb 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -19,7 +19,7 @@
 
 @copying
 @quotation
-GNAT Reference Manual , Oct 27, 2022
+GNAT Reference Manual , Nov 14, 2022
 
 AdaCore
 
@@ -29037,11 +29037,122 @@
 least one of its predecessors, and at least one of its successors, are
 also marked as visited.
 
-Verification is performed just before returning.  Subprogram
-executions that complete by raising or propagating an exception bypass
-verification-and-return points.  A subprogram that can only complete
-by raising or propagating an exception may have instrumentation
-disabled altogether.
+Verification is performed just before a subprogram returns.  The
+following fragment:
+
+@example
+if X then
+  Y := F (Z);
+  return;
+end if;
+@end example
+
+gets turned into:
+
+@example
+type Visited_Bitmap is array (1..N) of Boolean with Pack;
+Visited : aliased Visited_Bitmap := (others => False);
+--  Bitmap of visited blocks.  N is the basic block count.
+[...]
+--  Basic block #I
+Visited(I) := True;
+if X then
+  --  Basic block #J
+  Visited(J) := True;
+  Y := F (Z);
+  CFR.Check (N, Visited'Access, CFG'Access);
+  --  CFR is a hypothetical package whose Check procedure calls
+  --  libgcc's __hardcfr_check, that traps if the Visited bitmap
+  --  does not hold a valid path in CFG, the run-time
+  --  representation of the control flow graph in the enclosing
+  --  subprogram.
+  return;
+end if;
+--  Basic block #K
+Visited(K) := True;
+@end example
+
+Verification would also be performed before tail calls, if any
+front-ends marked them as mandatory or desirable, but none do.
+Regular calls are optimized into tail calls too late for this
+transformation to act on it.
+
+In order to avoid adding verification after potential tail calls,
+which would prevent tail-call optimization, we recognize returning
+calls, i.e., calls whose result, if any, is returned by the calling
+subprogram to its caller immediately after the call returns.
+Verification is performed before such calls, whether or not they are
+ultimately optimized to tail calls.  This behavior is enabled by
+default whenever sibcall optimization is enabled (see
+@code{-foptimize-sibling-calls}); it may be disabled with
+@code{-fno-hardcfr-check-returning-calls}, or enabled with
+@code{-fhardcfr-check-returning-calls}, regardless of the
+optimization, but the lack of other optimizations may prevent calls
+from being recognized as returning calls:
+
+@example
+--  CFR.Check here, with -fhardcfr-check-returning-calls.
+P (X);
+--  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+return;
+@end example
+
+or:
+
+@example
+--  CFR.Check here, with -fhardcfr-check-returning-calls.
+R := F (X);
+--  CFR.Check here, with -fno-hardcfr-check-returning-calls.
+return R;
+@end example
+
+Any subprogram from which an exception may escape, i.e., that may
+raise or propagate an exception that isn’t handled internally, is
+conceptually enclosed by a cleanup handler that performs verification,
+unless this is disabled with @code{-fno-hardcfr-check-exceptions}.
+With this feature enabled, a subprogram body containing:
+
+@example
+--  ...
+  Y := F (X);  -- May raise exceptions.
+--  ...
+  raise E;  -- Not handled internally.
+--  ...
+@end example
+
+gets modified as follows:
+
+@example
+begin
+  --  ...
+    Y := F (X);  -- May raise exceptions.
+  --  ...
+    raise E;  -- Not handled internally.
+  --  ...
+exception
+  when others =>
+    CFR.Check (N, Visited'Access, CFG'Access);
+    raise;
+end;
+@end example
+
+Verification may also be performed before No_Return calls, whether
+only nothrow ones, with
+@code{-fhardcfr-check-noreturn-calls=nothrow}, or all of them, with
+@code{-fhardcfr-check-noreturn-calls=always}.  The default is
+@code{-fhardcfr-check-noreturn-calls=never} for this feature, that
+disables checking before No_Return calls.
+
+When a No_Return call returns control to its caller through an
+exception, verification may have already been performed before the
+call, if @code{-fhardcfr-check-noreturn-calls=always} is in effect.
+The compiler arranges for already-checked No_Return calls without a
+preexisting handler to bypass the implicitly-added cleanup handler and
+thus the redundant check, but a local exception or cleanup handler, if
+present, will modify the set of visited blocks, and checking will take
+place again when the caller reaches the next verification point,
+whether it is a return or reraise statement after the exception is
+otherwise handled, or even another No_Return call.
 
 The instrumentation for hardening with control flow redundancy can be
 observed in dump files generated by the command-line option
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 7b1aaeb..2f43b4f 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -19,7 +19,7 @@
 
 @copying
 @quotation
-GNAT User's Guide for Native Platforms , Oct 27, 2022
+GNAT User's Guide for Native Platforms , Nov 14, 2022
 
 AdaCore
 
@@ -17993,7 +17993,6 @@
 
 
 
-
 @c -- Example: A |withing| unit has a |with| clause, it |withs| a |withed| unit
 
 @node GNAT and Program Execution,Platform-Specific Information,GNAT Utility Programs,Top
@@ -29382,8 +29381,8 @@
 
 @printindex ge
 
-@anchor{cf}@w{                              }
 @anchor{gnat_ugn/gnat_utility_programs switches-related-to-project-files}@w{                              }
+@anchor{cf}@w{                              }
 
 @c %**end of body
 @bye