From c1025b4e6ff78e8c6358f542661e1ba0dbd03e6b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 27 Apr 2017 12:17:42 +0200 Subject: [PATCH] [multiple changes] 2017-04-27 Steve Baird * exp_util.adb (Build_Allocate_Deallocate_Proc): Add "Suppress => All_Checks" to avoid generating unnecessary checks. 2017-04-27 Yannick Moy * debug.adb: Reserve debug flag 'm' for no inlining in GNATprove. * sem_ch6.adb (Anayze_Subprogram_Body_Helper): Skip creation of inlining body in GNATprove mode when switch -gnatdm used. * sem_res.adb (Resolve_Call): Skip detection of lack of inlining in GNATprove mode when switch -gnatdm used. 2017-04-27 Arnaud Charlet * sem_ch13.adb (Analyze_Attribute_Definition_Clause [Attribute_Address]): Call Set_Address_Taken when ignoring rep clauses, so that we keep an indication of the address clause before removing it from the tree. From-SVN: r247312 --- gcc/ada/ChangeLog | 21 +++++++++++++++++++++ gcc/ada/debug.adb | 7 ++++++- gcc/ada/exp_util.adb | 3 ++- gcc/ada/sem_ch13.adb | 6 +++++- gcc/ada/sem_ch6.adb | 2 ++ gcc/ada/sem_res.adb | 3 ++- 6 files changed, 38 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 2362ccf55c2..cfcf449ffb6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2017-04-27 Steve Baird + + * exp_util.adb (Build_Allocate_Deallocate_Proc): + Add "Suppress => All_Checks" to avoid generating unnecessary + checks. + +2017-04-27 Yannick Moy + + * debug.adb: Reserve debug flag 'm' for no inlining in GNATprove. + * sem_ch6.adb (Anayze_Subprogram_Body_Helper): Skip creation of + inlining body in GNATprove mode when switch -gnatdm used. + * sem_res.adb (Resolve_Call): Skip detection of lack of inlining + in GNATprove mode when switch -gnatdm used. + +2017-04-27 Arnaud Charlet + + * sem_ch13.adb (Analyze_Attribute_Definition_Clause + [Attribute_Address]): Call Set_Address_Taken when ignoring rep + clauses, so that we keep an indication of the address clause + before removing it from the tree. + 2017-04-27 Yannick Moy * exp_util.ads, exp_util.adb (Evaluate_Name): Force evaluation diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 46f19ca2e06..c289c98e604 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -49,7 +49,7 @@ package body Debug is -- dj Suppress "junk null check" for access parameter values -- dk Generate GNATBUG message on abort, even if previous errors -- dl Generate unit load trace messages - -- dm + -- dm Prevent special frontend inlining in GNATprove mode -- dn Generate messages for node/list allocation -- do Print source from tree (original code only) -- dp Generate messages for parser scope stack push/pops @@ -281,6 +281,11 @@ package body Debug is -- generated each time a request is made to the library manager to -- load a new unit. + -- dm Prevent special frontend inlining in GNATprove mode. In some cases, + -- some subprogram calls are inlined in GNATprove mode in order to + -- facilitate formal verification. This debug switch prevents that + -- inlining to happen. + -- dn Generate messages for node/list allocation. Each time a node or -- list header is allocated, a line of output is generated. Certain -- other basic tree operations also cause a line of output to be diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index c80cd39a885..4da91dad397 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -991,7 +991,8 @@ package body Exp_Util is Make_Procedure_Call_Statement (Loc, Name => New_Occurrence_Of (Proc_To_Call, Loc), - Parameter_Associations => Actuals))))); + Parameter_Associations => Actuals)))), + Suppress => All_Checks); -- The newly generated Allocate / Deallocate becomes the default -- procedure to call when the back end processes the allocation / diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 34fd7a53b52..2c2366d2192 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -4701,7 +4701,7 @@ package body Sem_Ch13 is -- We do not do anything here with address clauses, they will be -- removed by Freeze later on, but for now, it works better to - -- keep then in the tree. + -- keep them in the tree. when Attribute_Address => null; @@ -4860,8 +4860,12 @@ package body Sem_Ch13 is -- Even when ignoring rep clauses we need to indicate that the -- entity has an address clause and thus it is legal to declare -- it imported. Freeze will get rid of the address clause later. + -- Also call Set_Address_Taken to indicate that an address clause + -- was present, even if we are about to remove it. if Ignore_Rep_Clauses then + Set_Address_Taken (U_Ent); + if Ekind_In (U_Ent, E_Variable, E_Constant) then Record_Rep_Item (U_Ent, N); end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 020ffb8400a..49bcc9b6064 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -4050,6 +4050,7 @@ package body Sem_Ch6 is -- inlining. This inlining should occur after analysis of the body, so -- that it is known whether the value of SPARK_Mode, which can be -- defined by a pragma inside the body, is applicable to the body. + -- Inlining can be disabled with switch -gnatdm elsif GNATprove_Mode and then Full_Analysis @@ -4060,6 +4061,7 @@ package body Sem_Ch6 is and then Body_Has_SPARK_Mode_On and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) and then not Body_Has_Contract + and then not Debug_Flag_M then Build_Body_To_Inline (N, Spec_Id); end if; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 0595b0b0835..383a5a95519 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6621,10 +6621,11 @@ package body Sem_Res is Body_Id := Corresponding_Body (Nam_Decl); -- Nothing to do if the subprogram is not eligible for inlining in - -- GNATprove mode. + -- GNATprove mode, or inlining is disabled with switch -gnatdm if not Is_Inlined_Always (Nam_UA) or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id) + or else Debug_Flag_M then null; -- 2.30.2