[gcc r12-3807] [Ada] More precise analysis of function renamings in GNATprove

[gcc r12-3807] [Ada] More precise analysis of function renamings in GNATprove

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098

commit r12-3807-g0b7ddfb9f13b3bfb7f4fc9ac23f6adf4f36e7098
Author: Yannick Moy <moy@adacore.com>
Date:   Fri Jul 16 16:35:19 2021 +0200

    [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.

Diff:
---
 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 3f57bc50fea..51671419b44 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 ea6ecf9b145..02928342744 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);