In GNATprove mode, all subprograms are candidates for front-end inlining, to simplify proofs. This patch extends this transformation to subprogam bodies that do not have a previous subprogram declaration. In this case the compiler builds a declaration, transfers aspects, if any, from body to declaration, and attempts to create a body_to_inline, as if the Inline_Always pragma was present on every such body.
Tested on x86_64-pc-linux-gnu, committed on trunk 2014-07-30 Ed Schonberg <schonb...@adacore.com> * sem_ch6.adb (Hanalyze_Subprogram_Body_Helper): In GNATprove mode, subprogram bodies without a previous declaration are also candidates for front-end inlining.
Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 213240) +++ sem_ch6.adb (working copy) @@ -2952,6 +2952,42 @@ Spec_Id := Disambiguate_Spec; else Spec_Id := Find_Corresponding_Spec (N); + + -- In GNATprove mode, if the body has no previous spec, create + -- one so that the inlining machinery can operate properly. + -- Transfer aspects, if any, to the new spec, so that they + -- are legal and can be processed ahead of the body. + -- We make two copies of the given spec, one for the new + -- declaration, and one for the body. + + -- This cannot be done for a compilation unit, which is not + -- in a context where we can insert a new spec. + + if No (Spec_Id) + and then GNATprove_Mode + and then Debug_Flag_QQ + and then Full_Analysis + and then Comes_From_Source (Body_Id) + and then Is_List_Member (N) + then + declare + Body_Spec : constant Node_Id := + Copy_Separate_Tree (Specification (N)); + New_Decl : constant Node_Id := + Make_Subprogram_Declaration + (Loc, Copy_Separate_Tree (Specification (N))); + + begin + Insert_Before (N, New_Decl); + Move_Aspects (From => N, To => New_Decl); + Analyze (New_Decl); + Spec_Id := Defining_Entity (New_Decl); + + Set_Specification (N, Body_Spec); + Body_Id := Analyze_Subprogram_Specification (Body_Spec); + Set_Corresponding_Spec (N, Spec_Id); + end; + end if; end if; -- If this is a duplicate body, no point in analyzing it