diff options
| -rw-r--r-- | gcc/ada/freeze.adb | 27 | ||||
| -rw-r--r-- | 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); |