From: Arnaud Charlet Date: Fri, 23 Oct 2015 12:28:53 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2700b9c1ee96244be32ca50533692d14f4b18eef;p=gcc.git [multiple changes] 2015-10-23 Arnaud Charlet * gnat1drv.adb (Adjust_Global_Switches): Adjust. 2015-10-23 Hristian Kirtchev * exp_dbug.ads, exp_dbug.adb (Get_External_Name): The special prefix for ignored Ghost entities is now ___ghost_. 2015-10-23 Hristian Kirtchev * ghost.adb (Is_Subject_To_Ghost): Check the original node when searching for pragma Ghost to catch cases where a source construct has been rewritten into something else. 2015-10-23 Ed Schonberg * einfo.ads, einfo.adb (Rewritten_For_C): New flag on functions that return a constrained array type. When generating C these functions are rewritten as procedures with an out parameter, and calls to such functions are rewritten accordingly. * exp_ch6.adb (Expand_N_Subprogram_Declaration): When Modify_Tree_For_C is set and the function returns a constrained array type, generate a procedure declaration with an additional out parameter. Mark original function as Rewritten_For_C. The new declaration is inserted in tree immediately after current declaration. (Expand_Subprogram_Body): If entity is marked Rewritten_For_C, generate body of corresponding procedure using declarations and statements for function body. Replace return statements with assignments to the out parameter, followed by a simple return statement. (Rewrite_Function_Call_For_C): New procedure to replace a function call that returns an array by a procedure call. From-SVN: r229241 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 882fb8c5059..4851d5dbc41 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,38 @@ +2015-10-23 Arnaud Charlet + + * gnat1drv.adb (Adjust_Global_Switches): Adjust. + +2015-10-23 Hristian Kirtchev + + * exp_dbug.ads, exp_dbug.adb (Get_External_Name): The special prefix for + ignored Ghost entities is now ___ghost_. + +2015-10-23 Hristian Kirtchev + + * ghost.adb (Is_Subject_To_Ghost): Check the + original node when searching for pragma Ghost to catch cases + where a source construct has been rewritten into something else. + +2015-10-23 Ed Schonberg + + * einfo.ads, einfo.adb (Rewritten_For_C): New flag on functions + that return a constrained array type. When generating C these + functions are rewritten as procedures with an out parameter, + and calls to such functions are rewritten accordingly. + * exp_ch6.adb (Expand_N_Subprogram_Declaration): When + Modify_Tree_For_C is set and the function returns a constrained + array type, generate a procedure declaration with an additional + out parameter. Mark original function as Rewritten_For_C. + The new declaration is inserted in tree immediately after + current declaration. + (Expand_Subprogram_Body): If entity is marked Rewritten_For_C, + generate body of corresponding procedure using declarations + and statements for function body. Replace return statements + with assignments to the out parameter, followed by a simple + return statement. + (Rewrite_Function_Call_For_C): New procedure to replace a function + call that returns an array by a procedure call. + 2015-10-23 Hristian Kirtchev * sem_util.adb (Denotes_Iterator): New routine. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 1572a9a794e..5cca0fa11c7 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -597,8 +597,8 @@ package body Einfo is -- Is_Unimplemented Flag284 -- Is_Volatile_Full_Access Flag285 -- Needs_Typedef Flag286 + -- Rewritten_For_C Flag287 - -- (unused) Flag287 -- (unused) Flag288 -- (unused) Flag289 -- (unused) Flag300 @@ -3042,6 +3042,12 @@ package body Einfo is return Flag93 (Base_Type (Id)); end Reverse_Storage_Order; + function Rewritten_For_C (Id : E) return B is + begin + pragma Assert (Ekind (Id) = E_Function); + return Flag287 (Id); + end Rewritten_For_C; + function RM_Size (Id : E) return U is begin pragma Assert (Is_Type (Id)); @@ -6046,6 +6052,12 @@ package body Einfo is Set_Flag93 (Id, V); end Set_Reverse_Storage_Order; + procedure Set_Rewritten_For_C (Id : E; V : B := True) is + begin + pragma Assert (Ekind (Id) = E_Function); + Set_Flag287 (Id, V); + end Set_Rewritten_For_C; + procedure Set_RM_Size (Id : E; V : U) is begin pragma Assert (Is_Type (Id)); @@ -8964,6 +8976,7 @@ package body Einfo is W ("Returns_Limited_View", Flag134 (Id)); W ("Reverse_Bit_Order", Flag164 (Id)); W ("Reverse_Storage_Order", Flag93 (Id)); + W ("Rewritten_For_C", Flag287 (Id)); W ("Sec_Stack_Needed_For_Return", Flag167 (Id)); W ("Size_Depends_On_Discriminant", Flag177 (Id)); W ("Size_Known_At_Compile_Time", Flag92 (Id)); @@ -10246,6 +10259,9 @@ package body Einfo is procedure Write_Field38_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Function | E_Procedure => + Write_Str ("Class-wide preconditions"); + when others => Write_Str ("Field38??"); end case; @@ -10258,6 +10274,9 @@ package body Einfo is procedure Write_Field39_Name (Id : Entity_Id) is begin case Ekind (Id) is + when E_Function | E_Procedure => + Write_Str ("Class-wide postcondition"); + when others => Write_Str ("Field39??"); end case; diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 1426c4fccb8..b27405f2477 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3943,6 +3943,12 @@ package Einfo is -- the Bit_Order aspect must be set to the same value (either explicitly -- or as the target default value). +-- Rewritten_For_C (Flag287) +-- Defined on functions that return a constrained array type, when +-- Modify_Tree_For_C is set. indicates that a procedure with an extra +-- out parameter has been created for it, and calls must be rewritten as +-- calls to the new procedure. + -- RM_Size (Uint13) -- Defined in all type and subtype entities. Contains the value of -- type'Size as defined in the RM. See also the Esize field and @@ -5908,6 +5914,7 @@ package Einfo is -- Return_Present (Flag54) -- Returns_By_Ref (Flag90) -- Returns_Limited_View (Flag134) (non-generic case only) + -- Rewritten_For_C (Flag287) -- Sec_Stack_Needed_For_Return (Flag167) -- SPARK_Pragma_Inherited (Flag265) -- Uses_Sec_Stack (Flag95) @@ -7078,6 +7085,7 @@ package Einfo is function Returns_Limited_View (Id : E) return B; function Reverse_Bit_Order (Id : E) return B; function Reverse_Storage_Order (Id : E) return B; + function Rewritten_For_C (Id : E) return B; function RM_Size (Id : E) return U; function Scalar_Range (Id : E) return N; function Scale_Value (Id : E) return U; @@ -7743,6 +7751,7 @@ package Einfo is procedure Set_Returns_Limited_View (Id : E; V : B := True); procedure Set_Reverse_Bit_Order (Id : E; V : B := True); procedure Set_Reverse_Storage_Order (Id : E; V : B := True); + procedure Set_Rewritten_For_C (Id : E; V : B := True); procedure Set_RM_Size (Id : E; V : U); procedure Set_Scalar_Range (Id : E; V : N); procedure Set_Scale_Value (Id : E; V : U); @@ -8564,6 +8573,7 @@ package Einfo is pragma Inline (Returns_Limited_View); pragma Inline (Reverse_Bit_Order); pragma Inline (Reverse_Storage_Order); + pragma Inline (Rewritten_For_C); pragma Inline (RM_Size); pragma Inline (Scalar_Range); pragma Inline (Scale_Value); @@ -9024,6 +9034,7 @@ package Einfo is pragma Inline (Set_Returns_Limited_View); pragma Inline (Set_Reverse_Bit_Order); pragma Inline (Set_Reverse_Storage_Order); + pragma Inline (Set_Rewritten_For_C); pragma Inline (Set_RM_Size); pragma Inline (Set_Scalar_Range); pragma Inline (Set_Scale_Value); diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 407ecef7b1e..ca0f33b4bf5 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -258,6 +258,10 @@ package body Exp_Ch6 is -- Expand simple return from function. In the case where we are returning -- from a function body this is called by Expand_N_Simple_Return_Statement. + procedure Rewrite_Function_Call_For_C (N : Node_Id); + -- When generating C code, replace a call to a function that returns an + -- array into the generated procedure with an additional out parameter. + procedure Set_Enclosing_Sec_Stack_Return (N : Node_Id); -- N is a return statement for a function that returns its result on the -- secondary stack. This sets the Sec_Stack_Needed_For_Return flag on the @@ -2507,6 +2511,18 @@ package body Exp_Ch6 is end; end if; + -- When generating C code, transform a function call that returns a + -- constrained array type into procedure form. + + if Modify_Tree_For_C + and then Nkind (Call_Node) = N_Function_Call + and then Is_Entity_Name (Name (Call_Node)) + and then Rewritten_For_C (Entity (Name (Call_Node))) + then + Rewrite_Function_Call_For_C (Call_Node); + return; + end if; + -- First step, compute extra actuals, corresponding to any Extra_Formals -- present. Note that we do not access Extra_Formals directly, instead -- we simply note the presence of the extra formals as we process the @@ -4940,21 +4956,23 @@ package body Exp_Ch6 is Body_Id : constant Entity_Id := Defining_Entity (N); HSS : constant Node_Id := Handled_Statement_Sequence (N); Loc : constant Source_Ptr := Sloc (N); - Except_H : Node_Id; - L : List_Id; - Spec_Id : Entity_Id; - procedure Add_Return (S : List_Id); - -- Append a return statement to the statement sequence S if the last - -- statement is not already a return or a goto statement. Note that - -- the latter test is not critical, it does not matter if we add a few - -- extra returns, since they get eliminated anyway later on. + procedure Add_Return (Spec_Id : Entity_Id; Stmts : List_Id); + -- Append a return statement to the statement sequence Stmts if the last + -- statement is not already a return or a goto statement. Note that the + -- latter test is not critical, it does not matter if we add a few extra + -- returns, since they get eliminated anyway later on. Spec_Id denotes + -- the corresponding spec of the subprogram body. + + procedure Build_Procedure_Body_Form (Func_Id : Entity_Id); + -- Create a procedure body which emulates the behavior of function + -- Func_Id. ---------------- -- Add_Return -- ---------------- - procedure Add_Return (S : List_Id) is + procedure Add_Return (Spec_Id : Entity_Id; Stmts : List_Id) is Last_Stmt : Node_Id; Loc : Source_Ptr; Stmt : Node_Id; @@ -4963,7 +4981,7 @@ package body Exp_Ch6 is -- Get last statement, ignoring any Pop_xxx_Label nodes, which are -- not relevant in this context since they are not executable. - Last_Stmt := Last (S); + Last_Stmt := Last (Stmts); while Nkind (Last_Stmt) in N_Pop_xxx_Label loop Prev (Last_Stmt); end loop; @@ -4979,8 +4997,8 @@ package body Exp_Ch6 is -- all the statements within the handler are made invisible -- to the debugger. - if Nkind (Parent (S)) = N_Exception_Handler - and then not Comes_From_Source (Parent (S)) + if Nkind (Parent (Stmts)) = N_Exception_Handler + and then not Comes_From_Source (Parent (Stmts)) then Loc := Sloc (Last_Stmt); elsif Present (End_Label (HSS)) then @@ -5005,7 +5023,7 @@ package body Exp_Ch6 is -- added to it. A guard in Sem_Elab is needed to prevent that -- spurious check, see Check_Elab_Call. - Append_To (S, Stmt); + Append_To (Stmts, Stmt); Set_Analyzed (Stmt); -- Call the _Postconditions procedure if the related subprogram @@ -5022,10 +5040,128 @@ package body Exp_Ch6 is end if; end Add_Return; + ------------------------------- + -- Build_Procedure_Body_Form -- + ------------------------------- + + procedure Build_Procedure_Body_Form (Func_Id : Entity_Id) is + Proc_Decl : constant Node_Id := + Next (Unit_Declaration_Node (Func_Id)); + -- It is assumed that the next node following the declaration of the + -- corresponding subprogram spec is the declaration of the procedure + -- form. + + Proc_Id : constant Entity_Id := Defining_Entity (Proc_Decl); + + procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id); + -- Replace each return statement found in the list Stmts with an + -- assignment of the return expression to parameter Param_Id. + + --------------------- + -- Replace_Returns -- + --------------------- + + procedure Replace_Returns (Param_Id : Entity_Id; Stmts : List_Id) is + Stmt : Node_Id; + + begin + Stmt := First (Stmts); + while Present (Stmt) loop + if Nkind (Stmt) = N_Block_Statement then + Replace_Returns (Param_Id, Statements (Stmt)); + + elsif Nkind (Stmt) = N_Case_Statement then + declare + Alt : Node_Id; + begin + Alt := First (Alternatives (Stmt)); + while Present (Alt) loop + Replace_Returns (Param_Id, Statements (Alt)); + Next (Alt); + end loop; + end; + + elsif Nkind (Stmt) = N_If_Statement then + Replace_Returns (Param_Id, Then_Statements (Stmt)); + Replace_Returns (Param_Id, Else_Statements (Stmt)); + + declare + Part : Node_Id; + begin + Part := First (Elsif_Parts (Stmt)); + while Present (Part) loop + Replace_Returns (Part, Then_Statements (Part)); + Next (Part); + end loop; + end; + + elsif Nkind (Stmt) = N_Loop_Statement then + Replace_Returns (Param_Id, Statements (Stmt)); + + elsif Nkind (Stmt) = N_Simple_Return_Statement then + + -- Generate: + -- Param := Expr; + -- return; + + Rewrite (Stmt, + Make_Assignment_Statement (Sloc (Stmt), + Name => New_Occurrence_Of (Param_Id, Loc), + Expression => Relocate_Node (Expression (Stmt)))); + + Insert_After (Stmt, Make_Simple_Return_Statement (Loc)); + + -- Skip the added return + + Next (Stmt); + end if; + + Next (Stmt); + end loop; + end Replace_Returns; + + -- Local variables + + Stmts : List_Id; + + -- Start of processing for Build_Procedure_Body_Form + + begin + -- This routine performs the following expansion: + + -- function F (...) return Array_Typ is + -- begin + -- ... + -- return Something; + -- end F; + + -- procedure P (..., Result : out Array_Typ) is + -- begin + -- ... + -- Result := Something; + -- end P; + + Stmts := New_Copy_List (Statements (HSS)); + Replace_Returns (Last_Entity (Proc_Id), Stmts); + + Insert_After_And_Analyze (N, + Make_Subprogram_Body (Loc, + Specification => + Copy_Subprogram_Spec (Specification (Proc_Decl)), + Declarations => New_Copy_List (Declarations (N)), + Handled_Statement_Sequence => + Make_Handled_Sequence_Of_Statements (Loc, + Statements => Stmts))); + end Build_Procedure_Body_Form; + -- Local varaibles Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Except_H : Node_Id; + L : List_Id; + Spec_Id : Entity_Id; + -- Start of processing for Expand_N_Subprogram_Body begin @@ -5221,12 +5357,12 @@ package body Exp_Ch6 is -- the subprogram. if Ekind_In (Spec_Id, E_Procedure, E_Generic_Procedure) then - Add_Return (Statements (HSS)); + Add_Return (Spec_Id, Statements (HSS)); if Present (Exception_Handlers (HSS)) then Except_H := First_Non_Pragma (Exception_Handlers (HSS)); while Present (Except_H) loop - Add_Return (Statements (Except_H)); + Add_Return (Spec_Id, Statements (Except_H)); Next_Non_Pragma (Except_H); end loop; end if; @@ -5316,6 +5452,17 @@ package body Exp_Ch6 is Unest_Bodies.Append ((Spec_Id, N)); end if; + -- When generating C code, transform a function that returns a + -- constrained array type into a procedure with an out parameter + -- that carries the return value. + + if Modify_Tree_For_C + and then Ekind (Spec_Id) = E_Function + and then Rewritten_For_C (Spec_Id) + then + Build_Procedure_Body_Form (Spec_Id); + end if; + Ghost_Mode := Save_Ghost_Mode; end Expand_N_Subprogram_Body; @@ -5343,13 +5490,73 @@ package body Exp_Ch6 is -- If the declaration is for a null procedure, emit null body procedure Expand_N_Subprogram_Declaration (N : Node_Id) is - Loc : constant Source_Ptr := Sloc (N); - Subp : constant Entity_Id := Defining_Entity (N); + Loc : constant Source_Ptr := Sloc (N); + Subp : constant Entity_Id := Defining_Entity (N); + + procedure Build_Procedure_Form; + -- Create a procedure declaration which emulates the behavior of + -- function Subp. + + -------------------------- + -- Build_Procedure_Form -- + -------------------------- + + procedure Build_Procedure_Form is + Func_Formal : Entity_Id; + Proc_Formals : List_Id; + + begin + Proc_Formals := New_List; + + -- Create a list of formal parameters with the same types as the + -- function. + + Func_Formal := First_Formal (Subp); + while Present (Func_Formal) loop + Append_To (Proc_Formals, + Make_Parameter_Specification (Loc, + Defining_Identifier => + Make_Defining_Identifier (Loc, Chars (Func_Formal)), + Parameter_Type => + New_Occurrence_Of (Etype (Func_Formal), Loc))); + + Next_Formal (Func_Formal); + end loop; + + -- Add an extra out parameter to carry the function result + + Append_To (Proc_Formals, + Make_Parameter_Specification (Loc, + Defining_Identifier => Make_Temporary (Loc, 'R'), + Out_Present => True, + Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc))); + + -- The new procedure declaration is inserted immediately after the + -- function declaration. The processing in Build_Procedure_Body_Form + -- relies on this order. + + Insert_After_And_Analyze (N, + Make_Subprogram_Declaration (Loc, + Specification => + Make_Procedure_Specification (Loc, + Defining_Unit_Name => + Make_Defining_Identifier (Loc, Chars (Subp)), + Parameter_Specifications => Proc_Formals))); + + -- Mark the function as having a procedure form + + Set_Rewritten_For_C (Subp); + end Build_Procedure_Form; + + -- Local variables + Scop : constant Entity_Id := Scope (Subp); Prot_Bod : Node_Id; Prot_Decl : Node_Id; Prot_Id : Entity_Id; + -- Start of processing for Expand_N_Subprogram_Declaration + begin -- In SPARK, subprogram declarations are only allowed in package -- specifications. @@ -5451,6 +5658,18 @@ package body Exp_Ch6 is Set_Is_Inlined (Subp, False); end; end if; + + -- When generating C code, transform a function that returns a + -- constrained array type into a procedure with an out parameter + -- that carries the return value. + + if Modify_Tree_For_C + and then Nkind (Specification (N)) = N_Function_Specification + and then Is_Array_Type (Etype (Subp)) + and then Is_Constrained (Etype (Subp)) + then + Build_Procedure_Form; + end if; end Expand_N_Subprogram_Declaration; -------------------------------- @@ -9363,6 +9582,76 @@ package body Exp_Ch6 is end if; end Needs_Result_Accessibility_Level; + --------------------------------- + -- Rewrite_Function_Call_For_C -- + --------------------------------- + + procedure Rewrite_Function_Call_For_C (N : Node_Id) is + Func_Id : constant Entity_Id := Entity (Name (N)); + Func_Decl : constant Node_Id := Unit_Declaration_Node (Func_Id); + Par : constant Node_Id := Parent (N); + Loc : constant Source_Ptr := Sloc (Par); + Proc_Id : constant Entity_Id := Defining_Entity (Next (Func_Decl)); + Actuals : List_Id; + + begin + Actuals := Parameter_Associations (N); + + -- If the function call is the expression of an assignment statement, + -- transform the assignment into a procedure call. Generate: + + -- LHS := Func_Call (...); + + -- Proc_Call (..., LHS); + + if Nkind (Par) = N_Assignment_Statement then + Append_To (Actuals, (Name (Par))); + Rewrite (Par, + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Proc_Id, Loc), + Parameter_Associations => Actuals)); + Analyze (Par); + + -- Otherwise the context is an expression. Generate a temporary and a + -- procedure call to obtain the function result. Generate: + + -- ... Func_Call (...) ... + + -- Temp : ...; + -- Proc_Call (..., Temp); + -- ... Temp ... + + else + declare + Temp_Id : constant Entity_Id := Make_Temporary (Loc, 'T'); + Call : Node_Id; + Decl : Node_Id; + + begin + -- Generate: + -- Temp : ...; + + Decl := + Make_Object_Declaration (Loc, + Defining_Identifier => Temp_Id, + Object_Definition => + New_Occurrence_Of (Etype (Func_Id), Loc)); + + -- Generate: + -- Proc_Call (..., Temp); + + Append_To (Actuals, New_Occurrence_Of (Temp_Id, Loc)); + Call := + Make_Procedure_Call_Statement (Loc, + Name => New_Occurrence_Of (Proc_Id, Loc), + Parameter_Associations => Actuals); + + Insert_Actions (Par, New_List (Decl, Call)); + Rewrite (N, New_Occurrence_Of (Temp_Id, Loc)); + end; + end if; + end Rewrite_Function_Call_For_C; + ------------------------------------ -- Set_Enclosing_Sec_Stack_Return -- ------------------------------------ diff --git a/gcc/ada/exp_dbug.adb b/gcc/ada/exp_dbug.adb index 2775cef92d9..37f3920370d 100644 --- a/gcc/ada/exp_dbug.adb +++ b/gcc/ada/exp_dbug.adb @@ -785,7 +785,7 @@ package body Exp_Dbug is if Is_Ignored_Ghost_Entity (E) or else (Debug_Flag_Dot_5 and Is_Ghost_Entity (E)) then - Add_Str_To_Name_Buffer ("_ghost_"); + Add_Str_To_Name_Buffer ("___ghost_"); end if; -- Case of interface name being used diff --git a/gcc/ada/exp_dbug.ads b/gcc/ada/exp_dbug.ads index 0cca7851325..f8df41cb794 100644 --- a/gcc/ada/exp_dbug.ads +++ b/gcc/ada/exp_dbug.ads @@ -76,9 +76,9 @@ package Exp_Dbug is -- qualification for such entities. In particular this means that direct -- local variables of a procedure are not qualified. - -- For ignored Ghost entities, the encoding adds a prefix "_ghost_" to aid - -- the detection of leaks in the "living" space. Ignored Ghost entities and - -- any code associated with them should be removed by the compiler in a + -- For ignored Ghost entities, the encoding adds a prefix "___ghost_" to + -- aid the detection of leaks in the "living" space. Ignored Ghost entities + -- and any code associated with them should be removed by the compiler in a -- post-processing pass. As a result, object files should not contain any -- occurrences of this prefix. diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index cabcc2b32ce..f2ac16b5421 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -801,9 +801,10 @@ package body Ghost is Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); -- A source construct ends the region where pragma Ghost may appear, - -- stop the traversal. + -- stop the traversal. Check the original node as source constructs + -- may be rewritten into something else by expansion. - elsif Comes_From_Source (Decl) then + elsif Comes_From_Source (Original_Node (Decl)) then exit; end if; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 06f018db6c5..f62b2f3472d 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -648,7 +648,7 @@ procedure Gnat1drv is -- back end some day, it would not be true for this test, but it -- would be non-GCC, so this is a bit troublesome ??? - Front_End_Inlining := AAMP_On_Target; + Front_End_Inlining := AAMP_On_Target or Generate_C_Code; end if; -- Set back end inlining indication @@ -659,6 +659,10 @@ procedure Gnat1drv is not AAMP_On_Target + -- No back end inlining available on C generation + + and then not Generate_C_Code + -- No back end inlining in GNATprove mode, since it just confuses -- the formal verification process.