From eff70bcc1f1e808e3cc253a8452b7849329d549a Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 13 Apr 2022 21:39:38 +0200 Subject: [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. --- gcc/ada/sem_ch13.adb | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 54f32a2..c12253c 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. -- cgit v1.1