+2017-04-27 Steve Baird <baird@adacore.com>
+
+ * exp_util.adb (Build_Allocate_Deallocate_Proc):
+ Add "Suppress => All_Checks" to avoid generating unnecessary
+ checks.
+
+2017-04-27 Yannick Moy <moy@adacore.com>
+
+ * 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 <charlet@adacore.com>
+
+ * 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 <moy@adacore.com>
* exp_util.ads, exp_util.adb (Evaluate_Name): Force evaluation
-- 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
-- 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
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 /
-- 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;
-- 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;
-- 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
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;
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;