diff options
Diffstat (limited to 'gcc/ada/exp_prag.adb')
| -rw-r--r-- | gcc/ada/exp_prag.adb | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index 22e9bb0..5c3d2ca 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -321,6 +321,15 @@ package body Exp_Prag is -- be an explicit conditional in the source, not an implicit if, so we -- do not call Make_Implicit_If_Statement. + -- In formal verification mode, we keep the pragma check in the code, + -- and its enclosed expression is not expanded. This requires that no + -- transient scope is introduced for pragma check in this mode in + -- Exp_Ch7.Establish_Transient_Scope. + + if ALFA_Mode then + return; + end if; + -- Case where we generate a direct raise if ((Debug_Flag_Dot_G |