===================================================================
@@ -1558,10 +1558,15 @@
Id := Body_Id;
end if;
- -- General note. The following comments clearly say what cannot be
- -- inlined, but they do not give any clue on the motivation for the
- -- exclusion. It would be good to document the motivations ???
+ -- Only local subprograms without contracts are inlined in GNATprove
+ -- mode, as these are the subprograms which a user is not interested in
+ -- analyzing in isolation, but rather in the context of their call. This
+ -- is a convenient convention, that could be changed for an explicit
+ -- pragma/aspect one day.
+ -- In a number of special cases, inlining is not desirable or not
+ -- possible, see below.
+
-- Do not inline unit-level subprograms
if Nkind (Parent (Id)) = N_Defining_Program_Unit_Name then
@@ -1584,19 +1589,22 @@
then
return False;
- -- Do not inline expression functions
+ -- Do not inline expression functions, which are directly inlined at the
+ -- prover level.
elsif (Present (Spec_Id) and then Is_Expression_Function (Spec_Id))
or else Is_Expression_Function (Body_Id)
then
return False;
- -- Do not inline generic subprogram instances
+ -- Do not inline generic subprogram instances. The visibility rules of
+ -- generic instances plays badly with inlining.
elsif Is_Generic_Instance (Spec_Id) then
return False;
- -- Only inline subprograms whose body is marked SPARK_Mode On
+ -- Only inline subprograms whose body is marked SPARK_Mode On. Other
+ -- subprogram bodies should not be analyzed.
elsif No (SPARK_Pragma (Body_Id))
or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On
@@ -2952,11 +2960,11 @@
function Process_Sloc (Nod : Node_Id) return Traverse_Result;
-- If the call being expanded is that of an internal subprogram, set the
-- sloc of the generated block to that of the call itself, so that the
- -- expansion is skipped by the "next" command in gdb.
- -- Same processing for a subprogram in a predefined file, e.g.
- -- Ada.Tags. If Debug_Generated_Code is true, suppress this change to
- -- simplify our own development. Same in in GNATprove mode, to ensure
- -- that warnings and diagnostics point to the proper location.
+ -- expansion is skipped by the "next" command in gdb. Same processing
+ -- for a subprogram in a predefined file, e.g. Ada.Tags. If
+ -- Debug_Generated_Code is true, suppress this change to simplify our
+ -- own development. Same in GNATprove mode, to ensure that warnings and
+ -- diagnostics point to the proper location.
procedure Reset_Dispatching_Calls (N : Node_Id);
-- In subtree N search for occurrences of dispatching calls that use the
@@ -3634,8 +3642,9 @@
if Present (Renamed_Object (F)) then
-- If expander is active, it is an error to try to inline a
- -- recursive program. In GNATprove mode, just indicate that
- -- the inlining will not happen.
+ -- recursive program. In GNATprove mode, just indicate that the
+ -- inlining will not happen, and mark the subprogram as not always
+ -- inlined.
if Expander_Active then
Error_Msg_N
@@ -3643,6 +3652,7 @@
else
Cannot_Inline
("cannot inline call to recursive subprogram?", N, Subp);
+ Set_Is_Inlined (Subp, False);
end if;
return;
===================================================================
@@ -2477,6 +2477,10 @@
-- inherited by their instances. It is also set on the body entities
-- of inlined subprograms. See also Has_Pragma_Inline.
+-- Is_Inlined is also set for subprograms that are always inlined in
+-- GNATprove mode. GNATprove uses this flag to know when a body does not
+-- need to be analyzed.
+
-- Is_Instantiated (Flag126)
-- Defined in generic packages and generic subprograms. Set if the unit
-- is instantiated from somewhere in the extended main source unit. This
===================================================================
@@ -6222,7 +6222,14 @@
if Nkind (Decl) = N_Subprogram_Declaration
and then Present (Body_To_Inline (Decl))
then
- Expand_Inlined_Call (N, Nam_Alias, Nam);
+ if Is_Potentially_Unevaluated (N) then
+ Error_Msg_NE ("?cannot inline call to &", N, Nam);
+ Error_Msg_N
+ ("\call appears in potentially unevaluated context", N);
+ Set_Is_Inlined (Nam, False);
+ else
+ Expand_Inlined_Call (N, Nam_Alias, Nam);
+ end if;
end if;
end;
end if;
===================================================================
@@ -3483,6 +3483,7 @@
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
and then not Body_Has_Contract
then
+ Set_Is_Inlined (Spec_Id, True);
Build_Body_To_Inline (N, Spec_Id);
end if;
@@ -3510,6 +3511,7 @@
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
and then not Body_Has_Contract
then
+ Set_Is_Inlined (Spec_Id, True);
Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id);
end if;
@@ -3644,6 +3646,7 @@
and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
then
Set_Body_To_Inline (Parent (Parent (Spec_Id)), Empty);
+ Set_Is_Inlined (Spec_Id, False);
end if;
-- Check completion, and analyze the statements