diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2023-04-19 11:37:59 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:43 +0200 |
| commit | 431180997887296965f00328ec45c3d1f68ad4e9 (patch) | |
| tree | dec8a56ca862e98ddce57cad60694748c2d6d8fd | |
| parent | 0e511e29883e6959ce0e6c775bb62b8f8b48c7fb (diff) | |
| download | gcc-431180997887296965f00328ec45c3d1f68ad4e9.zip gcc-431180997887296965f00328ec45c3d1f68ad4e9.tar.gz gcc-431180997887296965f00328ec45c3d1f68ad4e9.tar.bz2 | |
ada: Remove wrong comment about expansion of exceptions for GNATprove
Code cleanup related to handling exceptions in GNATprove.
gcc/ada/
* exp_ch11.adb (Expand_N_Raise_Statement): Expansion of raise statements
never happens in GNATprove mode.
| -rw-r--r-- | gcc/ada/exp_ch11.adb | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/gcc/ada/exp_ch11.adb b/gcc/ada/exp_ch11.adb index db85c7e..53f0753 100644 --- a/gcc/ada/exp_ch11.adb +++ b/gcc/ada/exp_ch11.adb @@ -1592,10 +1592,8 @@ package body Exp_Ch11 is else -- Bypass expansion to a run-time call when back-end exception - -- handling is active, unless the target is CodePeer or GNATprove. - -- In CodePeer, raising an exception is treated as an error, while in - -- GNATprove all code with exceptions falls outside the subset of - -- code which can be formally analyzed. + -- handling is active, unless the target is CodePeer, where + -- raising an exception is treated as an error. if not CodePeer_Mode then return; @@ -1604,7 +1602,7 @@ package body Exp_Ch11 is -- Find innermost enclosing exception handler (there must be one, -- since the semantics has already verified that this raise statement -- is valid, and a raise with no arguments is only permitted in the - -- context of an exception handler. + -- context of an exception handler). Ehand := Parent (N); while Nkind (Ehand) /= N_Exception_Handler loop |