[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 --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 3f57bc50fea875a53a3c37fc8aceca53212dad32..51671419b4439a8451fca02f268bf8fd16e34abb 100644 (file)
--- 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 ea6ecf9b145cf2472011fadf77c6ca7344238363..02928342744a625da4191af2423c6b4c8d2e34ce 100644 (file)
--- 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);