+2014-07-30 Pat Rogers <rogers@adacore.com>
+
+ * gnat_rm.texi: Minor word error.
+
+2014-07-30 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_prag.adb (Expand_Old): Insert declarationss of temporaries
+ created to capture the value of the prefix of 'Old at the
+ beginning of the current declarative part, to prevent data flow
+ anomalies in the postcondition procedure that will follow.
+
+2014-07-30 Yannick Moy <moy@adacore.com>
+
+ * debug.adb: Retire debug flag -gnatdQ.
+ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check SPARK_Mode
+ on decl, not on body. Ignore predicate functions.
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Remove use of
+ debug flag -gnatdQ. Correctly analyze SPARK_Mode on decl and
+ body when generating a decl for a body on which SPARK_Mode aspect
+ is given.
+ * sem_prag.adb (Analyze_Pragma|SPARK_Mode): Reorder tests for
+ attaching pragma to entity, to account for declaration not coming
+ from source.
+ * sem_res.adb (Resolve_Call): Issue warning and flag subprogram
+ as not always inlined in GNATprove mode, when called in an
+ assertion context.
+
2014-07-30 Vincent Celier <celier@adacore.com>
* debug.adb: Minor comment update.
-- dN No file name information in exception messages
-- dO Output immediate error messages
-- dP Do not check for controlled objects in preelaborable packages
- -- dQ Enable inlining of bodies-without-decl in GNATprove mode
+ -- dQ
-- dR Bypass check for correct version of s-rpc
-- dS Never convert numbers to machine numbers in Sem_Eval
-- dT Convert to machine numbers only for constant declarations
-- in preelaborable packages, but this restriction is a huge pain,
-- especially in the predefined library units.
- -- dQ Enable inlining of bodies-without-decl in GNATprove mode. A decl is
- -- created by the frontend so that the usual frontend inlining
- -- mechanism can be used for formal verification. Under a debug flag
- -- until fully reliable.
-
-- dR Bypass the check for a proper version of s-rpc being present
-- to use the -gnatz? switch. This allows debugging of the use
-- of stubs generation without needing to have GLADE (or some
-- Generate a temporary to capture the value of the prefix:
-- Temp : <Pref type>;
+ -- Place that temporary at the beginning of declarations, to
+ -- prevent anomolies in the GNATprove flow analysis pass in
+ -- the precondition procedure that follows.
Decl :=
Make_Object_Declaration (Loc,
New_Occurrence_Of (Etype (Pref), Loc));
Set_No_Initialization (Decl);
- Append_To (Decls, Decl);
+ Prepend_To (Decls, Decl);
-- Evaluate the prefix, generate:
-- Temp := <Pref>;
that context, then @code{Ensures} holds when the subprogram returns.
Mode @code{Nominal} indicates that the input context should also satisfy the
precondition of the subprogram, and the output context should also satisfy its
-postcondition. More @code{Robustness} indicates that the precondition and
+postcondition. Mode @code{Robustness} indicates that the precondition and
postcondition of the subprogram should be ignored for this test case.
@node Pragma Thread_Local_Storage
elsif Is_Generic_Instance (Spec_Id) then
return False;
- -- Only inline subprograms whose body is marked SPARK_Mode On. Other
- -- subprogram bodies should not be analyzed.
-
- elsif Present (Body_Id)
- and then (No (SPARK_Pragma (Body_Id))
- or else
- Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On)
+ -- Only inline subprograms whose spec is marked SPARK_Mode On. For
+ -- the subprogram body, a similar check is performed after the body
+ -- is analyzed, as this is where a pragma SPARK_Mode might be inserted.
+
+ elsif Present (Spec_Id)
+ and then (No (SPARK_Pragma (Spec_Id))
+ or else
+ Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
then
return False;
elsif Instantiation_Location (Sloc (Id)) /= No_Location then
return False;
+ -- Predicate functions are treated specially by GNATprove. Do not inline
+ -- them.
+
+ elsif Is_Predicate_Function (Id) then
+ return False;
+
-- Otherwise, this is a subprogram declared inside the private part of a
-- package, or inside a package body, or locally in a subprogram, and it
-- does not have any contract. Inline it.
-- Start of processing for Analyze_One_Aspect
begin
- -- Skip aspect if already analyzed (not clear if this is needed)
+ -- Skip aspect if already analyzed, to avoid looping in some cases
if Analyzed (Aspect) then
goto Continue;
if No (Spec_Id)
and then GNATprove_Mode
- -- Under a debug flag until remaining issues are fixed
-
- and then Debug_Flag_QQ
-
-- Inlining does not apply during pre-analysis of code
and then Full_Analysis
New_Decl : constant Node_Id :=
Make_Subprogram_Declaration (Loc,
Copy_Separate_Tree (Specification (N)));
+ SPARK_Mode_Aspect : Node_Id;
+ Aspects : List_Id;
+ Prag, Aspect : Node_Id;
begin
Insert_Before (N, New_Decl);
Move_Aspects (From => N, To => New_Decl);
+
+ -- Mark the newly moved aspects as not analyzed, so that
+ -- their effect on New_Decl is properly analyzed.
+
+ Aspect := First (Aspect_Specifications (New_Decl));
+ while Present (Aspect) loop
+ Set_Analyzed (Aspect, False);
+ Next (Aspect);
+ end loop;
+
Analyze (New_Decl);
+
+ -- The analysis of the generated subprogram declaration
+ -- may have introduced pragmas, which need to be
+ -- analyzed.
+
+ Prag := Next (New_Decl);
+ while Prag /= N loop
+ Analyze (Prag);
+ Next (Prag);
+ end loop;
+
Spec_Id := Defining_Entity (New_Decl);
+ -- If aspect SPARK_Mode was specified on the body, it
+ -- needs to be repeated on the generated decl and the
+ -- body. Since the original aspect was moved to the
+ -- generated decl, copy it for the body.
+
+ if Has_Aspect (Spec_Id, Aspect_SPARK_Mode) then
+ SPARK_Mode_Aspect :=
+ New_Copy (Find_Aspect (Spec_Id, Aspect_SPARK_Mode));
+ Set_Analyzed (SPARK_Mode_Aspect, False);
+ Aspects := New_List;
+ Append (SPARK_Mode_Aspect, Aspects);
+ Set_Aspect_Specifications (N, Aspects);
+ end if;
+
Set_Specification (N, Body_Spec);
Body_Id := Analyze_Subprogram_Specification (Body_Spec);
Set_Corresponding_Spec (N, Spec_Id);
raise Pragma_Exit;
end if;
- -- Skip internally generated code
-
- elsif not Comes_From_Source (Stmt) then
- null;
-
elsif Nkind (Stmt) in N_Generic_Declaration then
Error_Pragma
("incorrect placement of pragma% on a generic");
Set_SPARK_Pragma_Inherited (Spec_Id, False);
return;
+ -- Skip internally generated code
+
+ elsif not Comes_From_Source (Stmt) then
+ null;
+
-- The pragma does not apply to a legal construct, issue an
-- error and stop the analysis.
if GNATprove_Mode
and then Is_Overloadable (Nam)
and then SPARK_Mode = On
- and then Full_Analysis
then
-- Retrieve the body to inline from the ultimate alias of Nam, if
-- there is one, otherwise calls that should be inlined end up not
Nam_Alias : constant Entity_Id := Ultimate_Alias (Nam);
Decl : constant Node_Id := Unit_Declaration_Node (Nam_Alias);
begin
- if Nkind (Decl) = N_Subprogram_Declaration
- and then Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
- and then No (Corresponding_Body (Decl))
+ -- If the subprogram is not eligible for inlining in GNATprove
+ -- mode, do nothing.
+
+ if not Can_Be_Inlined_In_GNATprove_Mode (Nam_Alias, Empty)
+ or else Nkind (Decl) /= N_Subprogram_Declaration
+ or else not Is_Inlined_Always (Nam_Alias)
then
- Error_Msg_NE
- ("?cannot inline call to & (body not seen yet)", N, Nam);
+ null;
+
+ -- Calls cannot be inlined inside assertions, as GNATprove treats
+ -- assertions as logic expressions.
+
+ elsif In_Assertion_Expr /= 0 then
+ Error_Msg_NE ("?cannot inline call to &", N, Nam);
+ Error_Msg_N ("\call appears in assertion expression", N);
Set_Is_Inlined_Always (Nam_Alias, False);
- elsif Nkind (Decl) = N_Subprogram_Declaration
- and then Present (Body_To_Inline (Decl))
- and then Is_Inlined (Nam_Alias)
- then
- if Is_Potentially_Unevaluated (N) then
+ -- Inlining should not be performed during pre-analysis
+
+ elsif Full_Analysis then
+
+ -- With the one-pass inlining technique, a call cannot be
+ -- inlined if the corresponding body has not been seen yet.
+
+ if No (Corresponding_Body (Decl)) then
+ Error_Msg_NE
+ ("?cannot inline call to & (body not seen yet)", N, Nam);
+ Set_Is_Inlined_Always (Nam_Alias, False);
+
+ -- Nothing to do if there is no body to inline, indicating that
+ -- the subprogram is not suitable for inlining in GNATprove
+ -- mode.
+
+ elsif No (Body_To_Inline (Decl)) then
+ null;
+
+ -- Calls cannot be inlined inside potentially unevaluated
+ -- expressions, as this would create complex actions inside
+ -- expressions, that are not handled by GNATprove.
+
+ elsif 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_Always (Nam_Alias, False);
+
+ -- Otherwise, inline the call
+
else
Expand_Inlined_Call (N, Nam_Alias, Nam);
end if;
projects / gcc.git / commitdiff