+2014-07-30 Yannick Moy <moy@adacore.com>
+
+ * einfo.ads (Is_Inlined): Document new use in GNATprove mode.
+ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Add comments
+ to explain rationale for inlining or not in GNATprove mode.
+ (Expand_Inlined_Call): In GNATprove mode, set Is_Inlined flag
+ to False when inlining is not possible.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Set Is_Inlined
+ flag to indicate that subprogram is fully inlined. To be reversed
+ if inlining problem is found.
+ * sem_res.adb (Resolve_Call): Set Is_Inlined flag to False when
+ call in potentially unevaluated context.
+
2014-07-30 Jose Ruiz <ruiz@adacore.com>
* s-tarest.adb, s-tarest.ads: Fix comments.
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
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
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
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
else
Cannot_Inline
("cannot inline call to recursive subprogram?", N, Subp);
+ Set_Is_Inlined (Subp, False);
end if;
return;
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;
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;
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
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;