diff mbox series

[Ada] More precise analysis of function renamings in GNATprove

Message ID 20210922151550.GA1907911@adacore.com
State New
Headers show
Series [Ada] More precise analysis of function renamings in GNATprove | expand

Commit Message

Pierre-Marie de Rodat Sept. 22, 2021, 3:15 p.m. UTC 
When a function renaming has a contract, it is important for GNATprove
that it is not treated as a simple wrapper, otherwise the link between
the renamed function and its renaming is lost for proof. Instead, it
should be treated as an expression function.

There is no impact on compilation.

Tested on x86_64-pc-linux-gnu, committed on trunk

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 mbox series

Patch

diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
--- 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
--- 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);