diff options
author | Yannick Moy <moy@adacore.com> | 2021-07-16 16:35:19 +0200 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-09-22 15:01:46 +0000 |
commit | 0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098 (patch) | |
tree | 41b9ff3f97e4a0ff66d2fddd82bc6d6baeb4da31 | |
parent | 4b54d9393e2af43393cce9b76798617b3c3452f1 (diff) | |
download | gcc-0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098.zip gcc-0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098.tar.gz gcc-0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098.tar.bz2 |
[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.
-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); |