diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 81d1faa3ffc..408f6d07c4a 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,30 @@ +2014-07-30 Pat Rogers + + * gnat_rm.texi: Minor word error. + +2014-07-30 Ed Schonberg + + * 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 + + * 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 * debug.adb: Minor comment update. diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index a93af0f6a30..64162ef0602 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -80,7 +80,7 @@ package body Debug is -- 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 @@ -438,11 +438,6 @@ package body Debug is -- 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 diff --git a/gcc/ada/exp_prag.adb b/gcc/ada/exp_prag.adb index 696d0635065..c48f3d2acf1 100644 --- a/gcc/ada/exp_prag.adb +++ b/gcc/ada/exp_prag.adb @@ -440,6 +440,9 @@ package body Exp_Prag is -- Generate a temporary to capture the value of the prefix: -- Temp : ; + -- 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, @@ -448,7 +451,7 @@ package body Exp_Prag is New_Occurrence_Of (Etype (Pref), Loc)); Set_No_Initialization (Decl); - Append_To (Decls, Decl); + Prepend_To (Decls, Decl); -- Evaluate the prefix, generate: -- Temp := ; diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 18673029661..b0a018bf497 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -7215,7 +7215,7 @@ The meaning of a test case is that there is at least one context where 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 diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 4f099585da4..be556fb2eb8 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1692,13 +1692,14 @@ package body Inline is 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. + -- 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 (Body_Id) - and then (No (SPARK_Pragma (Body_Id)) - or else - Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) /= On) + 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; @@ -1708,6 +1709,12 @@ package body Inline is 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. diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index a9fa109e98c..f359b486901 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1497,7 +1497,7 @@ package body Sem_Ch13 is -- 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; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 393d557ad6a..72ee3824687 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3034,10 +3034,6 @@ package body Sem_Ch6 is 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 @@ -3077,13 +3073,51 @@ package body Sem_Ch6 is 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); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 122d47ce312..983cb321752 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -19830,11 +19830,6 @@ package body Sem_Prag is 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"); @@ -19869,6 +19864,11 @@ package body Sem_Prag is 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. diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 88356fd6127..92317edaf49 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6210,7 +6210,6 @@ package body Sem_Res is 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 @@ -6220,23 +6219,54 @@ package body Sem_Res is 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;