diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2022-04-13 21:39:38 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-19 14:05:30 +0000 |
| commit | eff70bcc1f1e808e3cc253a8452b7849329d549a (patch) | |
| tree | 293ecd0157368c3bd67bf391caa4bdd1ee1d42a9 | |
| parent | 55a11c7e345dd06d6975fe8f4dc0e11ecbb581ff (diff) | |
| download | gcc-eff70bcc1f1e808e3cc253a8452b7849329d549a.tar.gz | |
[Ada] Ignore Predicate_Failure in GNATprove mode
In GNATprove mode we are don't want predicate failure to pollute the
predicate expression extracted from the predicate function.
gcc/ada/
* sem_ch13.adb (Build_Predicate_Function): Ignore predicate
failure in GNATprove mode.
| -rw-r--r-- | gcc/ada/sem_ch13.adb | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 54f32a2fc49..c12253cf26a 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -10487,7 +10487,13 @@ package body Sem_Ch13 is Second_Formal : constant Entity_Id := Next_Entity (Object_Entity); begin - if Present (PF_Expr) then + -- In GNATprove mode we are only interested in the predicate + -- expression itself and don't want a raise expression that + -- comes from the Predicate_Failure. + + if Present (PF_Expr) + and then not GNATprove_Mode + then pragma Assert (Present (Second_Formal)); -- This is an ugly hack to cope with an ugly situation. |