From 0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 16 Jul 2021 16:35:19 +0200 Subject: [Ada] More precise analysis of function renamings in GNATprove gcc/ada/ * freeze.adb (Build_Renamed_Body): Special case for GNATprove. * sem_ch6.adb (Analyze_Expression_Function): Remove useless test for a node to come from source, which becomes harmful otherwise. --- gcc/ada/freeze.adb | 27 ++++++++++++++++++++------- gcc/ada/sem_ch6.adb | 6 ------ 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 3f57bc5..5167141 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -636,13 +636,26 @@ package body Freeze is Next (Param_Spec); end loop; - Body_Node := - Make_Subprogram_Body (Loc, - Specification => Spec, - Declarations => New_List, - Handled_Statement_Sequence => - Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List (Call_Node))); + -- In GNATprove, prefer to generate an expression function whenever + -- possible, to benefit from the more precise analysis in that case + -- (as if an implicit postcondition had been generated). + + if GNATprove_Mode + and then Nkind (Call_Node) = N_Simple_Return_Statement + then + Body_Node := + Make_Expression_Function (Loc, + Specification => Spec, + Expression => Expression (Call_Node)); + else + Body_Node := + Make_Subprogram_Body (Loc, + Specification => Spec, + Declarations => New_List, + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => New_List (Call_Node))); + end if; if Nkind (Decl) /= N_Subprogram_Declaration then Rewrite (N, diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index ea6ecf9..0292834 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -385,15 +385,9 @@ package body Sem_Ch6 is Analyze (New_Body); Set_Is_Inlined (Prev); - -- If the expression function is a completion, the previous declaration - -- must come from source. We know already that it appears in the current - -- scope. The entity itself may be internally created if within a body - -- to be inlined. - elsif Present (Prev) and then Is_Overloadable (Prev) and then not Is_Formal_Subprogram (Prev) - and then Comes_From_Source (Parent (Prev)) then Set_Has_Completion (Prev, False); Set_Is_Inlined (Prev); -- cgit v1.1