From ac072cb2f4dd884d48fb7527cadf2aa0b1a656d0 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Wed, 30 Jul 2014 12:47:17 +0200 Subject: [PATCH] [multiple changes] 2014-07-30 Robert Dewar * sem_ch4.adb (Analyze_If_Expression): Resolve condition before analyzing branches. * sem_eval.adb (Out_Of_Range): Check for statically unevaluated expression case. 2014-07-30 Robert Dewar * sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use of predicate aspect on entity other than a type. 2014-07-30 Ed Schonberg * sem_ch6.adb (Body_Has_Contract): New predicate to determine when a subprogram body without a previous spec cannot be inlined in GNATprove mode, because it includes aspects or pragmas that generate a SPARK contract clause. * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram instance cannot be inlined. From-SVN: r213247 --- gcc/ada/ChangeLog | 21 ++++++++++++++ gcc/ada/inline.adb | 10 ++++--- gcc/ada/sem_ch13.adb | 9 ++++++ gcc/ada/sem_ch4.adb | 11 +++++++ gcc/ada/sem_ch6.adb | 69 ++++++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_eval.adb | 15 ++++++++-- 6 files changed, 128 insertions(+), 7 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 768c313a281..dea492c7be4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2014-07-30 Robert Dewar + + * sem_ch4.adb (Analyze_If_Expression): Resolve condition before + analyzing branches. + * sem_eval.adb (Out_Of_Range): Check for statically unevaluated + expression case. + +2014-07-30 Robert Dewar + + * sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use + of predicate aspect on entity other than a type. + +2014-07-30 Ed Schonberg + + * sem_ch6.adb (Body_Has_Contract): New predicate to determine + when a subprogram body without a previous spec cannot be inlined + in GNATprove mode, because it includes aspects or pragmas that + generate a SPARK contract clause. + * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram + instance cannot be inlined. + 2014-07-30 Robert Dewar * debug.adb: Document that d7 suppresses compilation time output. diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 69388ac26a7..c2ee80783b3 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1490,13 +1490,12 @@ package body Inline is function Has_Some_Contract (Id : Entity_Id) return Boolean is Items : constant Node_Id := Contract (Id); + begin return Present (Items) and then (Present (Pre_Post_Conditions (Items)) - or else - Present (Contract_Test_Cases (Items)) - or else - Present (Classifications (Items))); + or else Present (Contract_Test_Cases (Items)) + or else Present (Classifications (Items))); end Has_Some_Contract; -------------------------- @@ -1589,6 +1588,9 @@ package body Inline is then return False; + elsif Is_Generic_Instance (Spec_Id) then + return False; + -- Only inline subprograms whose body is marked SPARK_Mode On elsif No (SPARK_Pragma (Body_Id)) diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index c7d039dca57..f6a8707c169 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1778,6 +1778,15 @@ package body Sem_Ch13 is Aspect_Predicate | Aspect_Static_Predicate => + -- These aspects apply only to subtypes + + if not Is_Type (E) then + Error_Msg_N + ("predicate can only be specified for a subtype", + Aspect); + goto Continue; + end if; + -- Construct the pragma (always a pragma Predicate, with -- flags recording whether it is static/dynamic). We also -- set flags recording this in the type itself. diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 968619762d8..f7d6aa895b6 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -2046,7 +2046,18 @@ package body Sem_Ch4 is Check_Compiler_Unit ("if expression", N); end if; + -- Analyze and resolve the condition. We need to resolve this now so + -- that it gets folded to True/False if possible, before we analyze + -- the THEN/ELSE branches, because when analyzing these branches, we + -- may call Is_Statically_Unevaluated, which expects the condition of + -- an enclosing IF to have been analyze/resolved/evaluated. + Analyze_Expression (Condition); + Resolve (Condition, Any_Boolean); + + -- Analyze THEN expression and (if present) ELSE expression. For those + -- we delay resolution in the normal manner, because of overloading etc. + Analyze_Expression (Then_Expr); if Present (Else_Expr) then diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 815ab546f9c..e2b267bb968 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2167,6 +2167,10 @@ package body Sem_Ch6 is -- Analyze the aspect specifications of a subprogram body [stub]. It is -- assumed that N has aspects. + function Body_Has_Contract return Boolean; + -- Check whether unanalyzed body has an aspect or pragma that may + -- generate a SPARK contrac. + procedure Check_Anonymous_Return; -- Ada 2005: if a function returns an access type that denotes a task, -- or a type that contains tasks, we must create a master entity for @@ -2339,6 +2343,68 @@ package body Sem_Ch6 is end if; end Analyze_Aspects_On_Body_Or_Stub; + ----------------------- + -- Body_Has_Contract -- + ----------------------- + + function Body_Has_Contract return Boolean is + Decls : constant List_Id := Declarations (N); + A_Spec : Node_Id; + A : Aspect_Id; + Decl : Node_Id; + P_Id : Pragma_Id; + + begin + -- Check for unanalyzed aspects in the body that will + -- generate a contract. + + if Present (Aspect_Specifications (N)) then + A_Spec := First (Aspect_Specifications (N)); + while Present (A_Spec) loop + A := Get_Aspect_Id (Chars (Identifier (A_Spec))); + + if A = Aspect_Contract_Cases + or else A = Aspect_Depends + or else A = Aspect_Global + or else A = Aspect_Pre + or else A = Aspect_Precondition + or else A = Aspect_Post + or else A = Aspect_Postcondition + then + return True; + end if; + + Next (A_Spec); + end loop; + end if; + + -- Check for pragmas that may generate a contract. + + if Present (Decls) then + Decl := First (Decls); + while Present (Decl) loop + if Nkind (Decl) = N_Pragma then + P_Id := Get_Pragma_Id (Pragma_Name (Decl)); + + if P_Id = Pragma_Contract_Cases + or else P_Id = Pragma_Depends + or else P_Id = Pragma_Global + or else P_Id = Pragma_Pre + or else P_Id = Pragma_Precondition + or else P_Id = Pragma_Post + or else P_Id = Pragma_Postcondition + then + return True; + end if; + end if; + + Next (Decl); + end loop; + end if; + + return False; + end Body_Has_Contract; + ---------------------------- -- Check_Anonymous_Return -- ---------------------------- @@ -2969,6 +3035,7 @@ package body Sem_Ch6 is and then Full_Analysis and then Comes_From_Source (Body_Id) and then Is_List_Member (N) + and then not Body_Has_Contract then declare Body_Spec : constant Node_Id := @@ -3410,6 +3477,7 @@ package body Sem_Ch6 is and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) + and then not Body_Has_Contract then Build_Body_To_Inline (N, Spec_Id); end if; @@ -3437,6 +3505,7 @@ package body Sem_Ch6 is and then Present (Spec_Id) and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id) + and then not Body_Has_Contract then Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id); end if; diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index addd3319261..6c41a4e5290 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -5280,15 +5280,22 @@ package body Sem_Eval is -- If we have the static expression case, then this is an illegality -- in Ada 95 mode, except that in an instance, we never generate an -- error (if the error is legitimate, it was already diagnosed in the - -- template). The expression to compute the length of a packed array is - -- attached to the array type itself, and deserves a separate message. + -- template). if Is_Static_Expression (N) and then not In_Instance and then not In_Inlined_Body and then Ada_Version >= Ada_95 then - if Nkind (Parent (N)) = N_Defining_Identifier + -- No message if we are staticallly unevaluated + + if Is_Statically_Unevaluated (N) then + null; + + -- The expression to compute the length of a packed array is attached + -- to the array type itself, and deserves a separate message. + + elsif Nkind (Parent (N)) = N_Defining_Identifier and then Is_Array_Type (Parent (N)) and then Present (Packed_Array_Impl_Type (Parent (N))) and then Present (First_Rep_Item (Parent (N))) @@ -5298,6 +5305,8 @@ package body Sem_Eval is First_Rep_Item (Parent (N))); Rewrite (N, Make_Integer_Literal (Sloc (N), Uint_1)); + -- All cases except the special array case + else Apply_Compile_Time_Constraint_Error (N, "value not in range of}", CE_Range_Check_Failed); -- 2.30.2