diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 29fdcfdaf11..375f02bf02b 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,61 @@ +2017-01-19 Javier Miranda + + * exp_aggr.adb (Pass_Aggregate_To_Back_End): Renamed as + Build_Back_End_Aggregate. + (Generate_Aggregate_For_Derived_Type): Code cleanup. + (Prepend_Stored_Values): Code cleanup. + +2017-01-19 Ed Schonberg + + * sem_ch6.adb (Analyze_Expression_Function): Check for an + incomplete return type after attempting to freeze it, so that + other freeze actiona are generated in the proper order. + +2017-01-19 Ed Schonberg + + * sem_aggr.adb (Resolve_Aggregate): If the type is a string + type, ie. a type whose component is a character type, and the + aggregate is positional, do not convert into a string literal + if the index type is not an integer type, because the original + type may be required in an enclosing operation. + +2017-01-19 Bob Duff + + * binde.adb, debug.adb: Enable new elaboration order algorithm + by default. -dp switch reverts to the old algorithm. + +2017-01-19 Hristian Kirtchev + + * sem_ch3.adb Add with and use clauses for Exp_Ch7. + (Analyze_Declarations): Create the DIC and Invariant + procedure bodies s after all freezing has taken place. + (Build_Assertion_Bodies): New routine. + * sem_ch7.adb Remove the with and use clauses for Exp_Ch7 + and Exp_Util. + (Analyze_Package_Specification): Remove the + generation of the DIC and Invariant procedure bodies. This is + now done by Analyze_Declarations. + * sem_disp.adb (Check_Dispatching_Operation): DIC and Invariant + procedures are never treated as primitives. + +2017-01-19 Yannick Moy + + * frontend.adb: Analyze inlined bodies and check elaboration + rules in GNATprove mode too. + * sem_elab.adb (Delay_Element): Add Boolean component to save + indication that call is in SPARK code. (Check_Elab_Calls): + Check elaboration rules in GNATprove mode, and correctly set + the current value of SPARK_Mode. + * lib-xref-spark_specific.adb + (Add_SPARK_Xrefs): Simplify iteration over dereferences. + +2017-01-19 Ed Schonberg + + * exp_ch4.adb (Expand_Concatenate): Do no enable overflow + checks on the expression for the high bound of concatenation + when checks are disabled, to suppress warnings about potential + constraint errors in restricted runtimes. + 2017-01-19 Hristian Kirtchev * exp_ch3.adb (Expand_Freeze_Enumeration_Type): Mark the diff --git a/gcc/ada/binde.adb b/gcc/ada/binde.adb index 7ab20924f92..2becc1b43b1 100644 --- a/gcc/ada/binde.adb +++ b/gcc/ada/binde.adb @@ -37,8 +37,7 @@ with System.OS_Lib; package body Binde is - -- We now have Elab_New, a new elaboration-order algorithm. It has the - -- property that ??? + -- We now have Elab_New, a new elaboration-order algorithm. -- -- However, any change to elaboration order can break some programs. -- Therefore, we are keeping the old algorithm in place, to be selected @@ -289,7 +288,12 @@ package body Binde is function Debug_Flag_Older return Boolean; function Debug_Flag_Old return Boolean; - -- True if debug flags select the old or older algorithms + -- True if debug flags select the old or older algorithms. Pretty much any + -- change to elaboration order can break some programs. For example, + -- programs can depend on elaboration order even without failing + -- access-before-elaboration checks. A trivial example is a program that + -- prints text during elaboration. Therefore, we have flags to revert to + -- the old(er) algorithms. procedure Validate (Order : Unit_Id_Array; Doing_New : Boolean); -- Assert that certain properties are true @@ -1134,10 +1138,7 @@ package body Binde is function Debug_Flag_Old return Boolean is begin - -- For now, Debug_Flag_P means "use the new algorithm". Once it is - -- stable, we intend to remove the "not" below. - - return not Debug_Flag_P; + return Debug_Flag_P; end Debug_Flag_Old; ---------------------- diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 4e1f0fc9810..70dfdc8b910 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -182,7 +182,7 @@ package body Debug is -- dm -- dn List details of manipulation of Num_Pred values -- do Use older preference for elaboration order - -- dp Use new preference for elaboration order + -- dp Use old preference for elaboration order -- dq -- dr -- ds @@ -813,16 +813,15 @@ package body Debug is -- prefer specs with no bodies to specs with bodies, and between two -- specs with bodies, prefers the one whose body is closer to being -- able to be elaborated. This is a clear improvement, but we provide - -- this debug flag in case of regressions. + -- this debug flag in case of regressions. Note: -do is even older than + -- -dp. - -- dp Use new elaboration order preference. The new preference rules + -- dp Use old elaboration order preference. The new preference rules -- elaborate all units within a strongly connected component together, -- with no other units in between. In particular, if a spec/body pair -- can be elaborated together, it will be. In the new order, the binder -- behaves as if every pragma Elaborate_All that would be legal is - -- present, even if it does not appear in the source code. NOTE: We - -- intend to reverse the sense of this switch at some point, so the new - -- preference is the default. + -- present, even if it does not appear in the source code. -- du List unit name and file name for each unit as it is read in diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 96853395095..9da35ddb9c2 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -6507,6 +6507,9 @@ package body Exp_Aggr is -- and the aggregate can be constructed statically and handled by -- the back-end. + procedure Build_Back_End_Aggregate; + -- Build a proper aggregate to be handled by the back-end + function Compile_Time_Known_Composite_Value (N : Node_Id) return Boolean; -- Returns true if N is an expression of composite type which can be -- fully evaluated at compile time without raising constraint error. @@ -6545,13 +6548,325 @@ package body Exp_Aggr is -- because it will not be set when type and its parent are in the -- same scope, and the parent component needs expansion. - procedure Pass_Aggregate_To_Back_End; - -- Build a proper aggregate to be handled by the back-end - function Top_Level_Aggregate (N : Node_Id) return Node_Id; -- For nested aggregates return the ultimate enclosing aggregate; for -- non-nested aggregates return N. + ------------------------------ + -- Build_Back_End_Aggregate -- + ------------------------------ + + procedure Build_Back_End_Aggregate is + Comp : Entity_Id; + New_Comp : Node_Id; + Tag_Value : Node_Id; + + begin + if Nkind (N) = N_Aggregate then + + -- If the aggregate is static and can be handled by the back-end, + -- nothing left to do. + + if Static_Components then + Set_Compile_Time_Known_Aggregate (N); + Set_Expansion_Delayed (N, False); + end if; + end if; + + -- If no discriminants, nothing special to do + + if not Has_Discriminants (Typ) then + null; + + -- Case of discriminants present + + elsif Is_Derived_Type (Typ) then + + -- For untagged types, non-stored discriminants are replaced with + -- stored discriminants, which are the ones that gigi uses to + -- describe the type and its components. + + Generate_Aggregate_For_Derived_Type : declare + procedure Prepend_Stored_Values (T : Entity_Id); + -- Scan the list of stored discriminants of the type, and add + -- their values to the aggregate being built. + + --------------------------- + -- Prepend_Stored_Values -- + --------------------------- + + procedure Prepend_Stored_Values (T : Entity_Id) is + Discr : Entity_Id; + First_Comp : Node_Id := Empty; + + begin + Discr := First_Stored_Discriminant (T); + while Present (Discr) loop + New_Comp := + Make_Component_Association (Loc, + Choices => New_List ( + New_Occurrence_Of (Discr, Loc)), + Expression => + New_Copy_Tree + (Get_Discriminant_Value + (Discr, + Typ, + Discriminant_Constraint (Typ)))); + + if No (First_Comp) then + Prepend_To (Component_Associations (N), New_Comp); + else + Insert_After (First_Comp, New_Comp); + end if; + + First_Comp := New_Comp; + Next_Stored_Discriminant (Discr); + end loop; + end Prepend_Stored_Values; + + -- Local variables + + Constraints : constant List_Id := New_List; + + Discr : Entity_Id; + Decl : Node_Id; + Num_Disc : Nat := 0; + Num_Gird : Nat := 0; + + -- Start of processing for Generate_Aggregate_For_Derived_Type + + begin + -- Remove the associations for the discriminant of derived type + + declare + First_Comp : Node_Id; + + begin + First_Comp := First (Component_Associations (N)); + while Present (First_Comp) loop + Comp := First_Comp; + Next (First_Comp); + + if Ekind (Entity (First (Choices (Comp)))) = + E_Discriminant + then + Remove (Comp); + Num_Disc := Num_Disc + 1; + end if; + end loop; + end; + + -- Insert stored discriminant associations in the correct + -- order. If there are more stored discriminants than new + -- discriminants, there is at least one new discriminant that + -- constrains more than one of the stored discriminants. In + -- this case we need to construct a proper subtype of the + -- parent type, in order to supply values to all the + -- components. Otherwise there is one-one correspondence + -- between the constraints and the stored discriminants. + + Discr := First_Stored_Discriminant (Base_Type (Typ)); + while Present (Discr) loop + Num_Gird := Num_Gird + 1; + Next_Stored_Discriminant (Discr); + end loop; + + -- Case of more stored discriminants than new discriminants + + if Num_Gird > Num_Disc then + + -- Create a proper subtype of the parent type, which is the + -- proper implementation type for the aggregate, and convert + -- it to the intended target type. + + Discr := First_Stored_Discriminant (Base_Type (Typ)); + while Present (Discr) loop + New_Comp := + New_Copy_Tree + (Get_Discriminant_Value + (Discr, + Typ, + Discriminant_Constraint (Typ))); + + Append (New_Comp, Constraints); + Next_Stored_Discriminant (Discr); + end loop; + + Decl := + Make_Subtype_Declaration (Loc, + Defining_Identifier => Make_Temporary (Loc, 'T'), + Subtype_Indication => + Make_Subtype_Indication (Loc, + Subtype_Mark => + New_Occurrence_Of (Etype (Base_Type (Typ)), Loc), + Constraint => + Make_Index_Or_Discriminant_Constraint + (Loc, Constraints))); + + Insert_Action (N, Decl); + Prepend_Stored_Values (Base_Type (Typ)); + + Set_Etype (N, Defining_Identifier (Decl)); + Set_Analyzed (N); + + Rewrite (N, Unchecked_Convert_To (Typ, N)); + Analyze (N); + + -- Case where we do not have fewer new discriminants than + -- stored discriminants, so in this case we can simply use the + -- stored discriminants of the subtype. + + else + Prepend_Stored_Values (Typ); + end if; + end Generate_Aggregate_For_Derived_Type; + end if; + + if Is_Tagged_Type (Typ) then + + -- In the tagged case, _parent and _tag component must be created + + -- Reset Null_Present unconditionally. Tagged records always have + -- at least one field (the tag or the parent). + + Set_Null_Record_Present (N, False); + + -- When the current aggregate comes from the expansion of an + -- extension aggregate, the parent expr is replaced by an + -- aggregate formed by selected components of this expr. + + if Present (Parent_Expr) and then Is_Empty_List (Comps) then + Comp := First_Component_Or_Discriminant (Typ); + while Present (Comp) loop + + -- Skip all expander-generated components + + if not Comes_From_Source (Original_Record_Component (Comp)) + then + null; + + else + New_Comp := + Make_Selected_Component (Loc, + Prefix => + Unchecked_Convert_To (Typ, + Duplicate_Subexpr (Parent_Expr, True)), + Selector_Name => New_Occurrence_Of (Comp, Loc)); + + Append_To (Comps, + Make_Component_Association (Loc, + Choices => New_List ( + New_Occurrence_Of (Comp, Loc)), + Expression => New_Comp)); + + Analyze_And_Resolve (New_Comp, Etype (Comp)); + end if; + + Next_Component_Or_Discriminant (Comp); + end loop; + end if; + + -- Compute the value for the Tag now, if the type is a root it + -- will be included in the aggregate right away, otherwise it will + -- be propagated to the parent aggregate. + + if Present (Orig_Tag) then + Tag_Value := Orig_Tag; + + elsif not Tagged_Type_Expansion then + Tag_Value := Empty; + + else + Tag_Value := + New_Occurrence_Of + (Node (First_Elmt (Access_Disp_Table (Typ))), Loc); + end if; + + -- For a derived type, an aggregate for the parent is formed with + -- all the inherited components. + + if Is_Derived_Type (Typ) then + declare + First_Comp : Node_Id; + Parent_Comps : List_Id; + Parent_Aggr : Node_Id; + Parent_Name : Node_Id; + + begin + -- Remove the inherited component association from the + -- aggregate and store them in the parent aggregate + + First_Comp := First (Component_Associations (N)); + Parent_Comps := New_List; + while Present (First_Comp) + and then + Scope (Original_Record_Component + (Entity (First (Choices (First_Comp))))) /= + Base_Typ + loop + Comp := First_Comp; + Next (First_Comp); + Remove (Comp); + Append (Comp, Parent_Comps); + end loop; + + Parent_Aggr := + Make_Aggregate (Loc, + Component_Associations => Parent_Comps); + Set_Etype (Parent_Aggr, Etype (Base_Type (Typ))); + + -- Find the _parent component + + Comp := First_Component (Typ); + while Chars (Comp) /= Name_uParent loop + Comp := Next_Component (Comp); + end loop; + + Parent_Name := New_Occurrence_Of (Comp, Loc); + + -- Insert the parent aggregate + + Prepend_To (Component_Associations (N), + Make_Component_Association (Loc, + Choices => New_List (Parent_Name), + Expression => Parent_Aggr)); + + -- Expand recursively the parent propagating the right Tag + + Expand_Record_Aggregate + (Parent_Aggr, Tag_Value, Parent_Expr); + + -- The ancestor part may be a nested aggregate that has + -- delayed expansion: recheck now. + + if Component_Not_OK_For_Backend then + Convert_To_Assignments (N, Typ); + end if; + end; + + -- For a root type, the tag component is added (unless compiling + -- for the VMs, where tags are implicit). + + elsif Tagged_Type_Expansion then + declare + Tag_Name : constant Node_Id := + New_Occurrence_Of + (First_Tag_Component (Typ), Loc); + Typ_Tag : constant Entity_Id := RTE (RE_Tag); + Conv_Node : constant Node_Id := + Unchecked_Convert_To (Typ_Tag, Tag_Value); + + begin + Set_Etype (Conv_Node, Typ_Tag); + Prepend_To (Component_Associations (N), + Make_Component_Association (Loc, + Choices => New_List (Tag_Name), + Expression => Conv_Node)); + end; + end if; + end if; + end Build_Back_End_Aggregate; + ---------------------------------------- -- Compile_Time_Known_Composite_Value -- ---------------------------------------- @@ -6726,310 +7041,6 @@ package body Exp_Aggr is end loop; end Has_Visible_Private_Ancestor; - -------------------------------- - -- Pass_Aggregate_To_Back_End -- - -------------------------------- - - procedure Pass_Aggregate_To_Back_End is - Comp : Entity_Id; - New_Comp : Node_Id; - Tag_Value : Node_Id; - - begin - if Nkind (N) = N_Aggregate then - - -- If the aggregate is static and can be handled by the back-end, - -- nothing left to do. - - if Static_Components then - Set_Compile_Time_Known_Aggregate (N); - Set_Expansion_Delayed (N, False); - end if; - end if; - - -- If no discriminants, nothing special to do - - if not Has_Discriminants (Typ) then - null; - - -- Case of discriminants present - - elsif Is_Derived_Type (Typ) then - - -- For untagged types, non-stored discriminants are replaced with - -- stored discriminants, which are the ones that gigi uses to - -- describe the type and its components. - - Generate_Aggregate_For_Derived_Type : declare - Constraints : constant List_Id := New_List; - First_Comp : Node_Id; - Discriminant : Entity_Id; - Decl : Node_Id; - Num_Disc : Nat := 0; - Num_Gird : Nat := 0; - - procedure Prepend_Stored_Values (T : Entity_Id); - -- Scan the list of stored discriminants of the type, and add - -- their values to the aggregate being built. - - --------------------------- - -- Prepend_Stored_Values -- - --------------------------- - - procedure Prepend_Stored_Values (T : Entity_Id) is - begin - Discriminant := First_Stored_Discriminant (T); - while Present (Discriminant) loop - New_Comp := - Make_Component_Association (Loc, - Choices => New_List ( - New_Occurrence_Of (Discriminant, Loc)), - Expression => - New_Copy_Tree - (Get_Discriminant_Value - (Discriminant, - Typ, - Discriminant_Constraint (Typ)))); - - if No (First_Comp) then - Prepend_To (Component_Associations (N), New_Comp); - else - Insert_After (First_Comp, New_Comp); - end if; - - First_Comp := New_Comp; - Next_Stored_Discriminant (Discriminant); - end loop; - end Prepend_Stored_Values; - - -- Start of processing for Generate_Aggregate_For_Derived_Type - - begin - -- Remove the associations for the discriminant of derived type - - First_Comp := First (Component_Associations (N)); - while Present (First_Comp) loop - Comp := First_Comp; - Next (First_Comp); - - if Ekind (Entity (First (Choices (Comp)))) = E_Discriminant - then - Remove (Comp); - Num_Disc := Num_Disc + 1; - end if; - end loop; - - -- Insert stored discriminant associations in the correct - -- order. If there are more stored discriminants than new - -- discriminants, there is at least one new discriminant that - -- constrains more than one of the stored discriminants. In - -- this case we need to construct a proper subtype of the - -- parent type, in order to supply values to all the - -- components. Otherwise there is one-one correspondence - -- between the constraints and the stored discriminants. - - First_Comp := Empty; - - Discriminant := First_Stored_Discriminant (Base_Type (Typ)); - while Present (Discriminant) loop - Num_Gird := Num_Gird + 1; - Next_Stored_Discriminant (Discriminant); - end loop; - - -- Case of more stored discriminants than new discriminants - - if Num_Gird > Num_Disc then - - -- Create a proper subtype of the parent type, which is the - -- proper implementation type for the aggregate, and convert - -- it to the intended target type. - - Discriminant := First_Stored_Discriminant (Base_Type (Typ)); - while Present (Discriminant) loop - New_Comp := - New_Copy_Tree - (Get_Discriminant_Value - (Discriminant, - Typ, - Discriminant_Constraint (Typ))); - - Append (New_Comp, Constraints); - Next_Stored_Discriminant (Discriminant); - end loop; - - Decl := - Make_Subtype_Declaration (Loc, - Defining_Identifier => Make_Temporary (Loc, 'T'), - Subtype_Indication => - Make_Subtype_Indication (Loc, - Subtype_Mark => - New_Occurrence_Of (Etype (Base_Type (Typ)), Loc), - Constraint => - Make_Index_Or_Discriminant_Constraint - (Loc, Constraints))); - - Insert_Action (N, Decl); - Prepend_Stored_Values (Base_Type (Typ)); - - Set_Etype (N, Defining_Identifier (Decl)); - Set_Analyzed (N); - - Rewrite (N, Unchecked_Convert_To (Typ, N)); - Analyze (N); - - -- Case where we do not have fewer new discriminants than - -- stored discriminants, so in this case we can simply use the - -- stored discriminants of the subtype. - - else - Prepend_Stored_Values (Typ); - end if; - end Generate_Aggregate_For_Derived_Type; - end if; - - if Is_Tagged_Type (Typ) then - - -- In the tagged case, _parent and _tag component must be created - - -- Reset Null_Present unconditionally. Tagged records always have - -- at least one field (the tag or the parent). - - Set_Null_Record_Present (N, False); - - -- When the current aggregate comes from the expansion of an - -- extension aggregate, the parent expr is replaced by an - -- aggregate formed by selected components of this expr. - - if Present (Parent_Expr) and then Is_Empty_List (Comps) then - Comp := First_Component_Or_Discriminant (Typ); - while Present (Comp) loop - - -- Skip all expander-generated components - - if not Comes_From_Source (Original_Record_Component (Comp)) - then - null; - - else - New_Comp := - Make_Selected_Component (Loc, - Prefix => - Unchecked_Convert_To (Typ, - Duplicate_Subexpr (Parent_Expr, True)), - Selector_Name => New_Occurrence_Of (Comp, Loc)); - - Append_To (Comps, - Make_Component_Association (Loc, - Choices => - New_List (New_Occurrence_Of (Comp, Loc)), - Expression => New_Comp)); - - Analyze_And_Resolve (New_Comp, Etype (Comp)); - end if; - - Next_Component_Or_Discriminant (Comp); - end loop; - end if; - - -- Compute the value for the Tag now, if the type is a root it - -- will be included in the aggregate right away, otherwise it will - -- be propagated to the parent aggregate. - - if Present (Orig_Tag) then - Tag_Value := Orig_Tag; - elsif not Tagged_Type_Expansion then - Tag_Value := Empty; - else - Tag_Value := - New_Occurrence_Of - (Node (First_Elmt (Access_Disp_Table (Typ))), Loc); - end if; - - -- For a derived type, an aggregate for the parent is formed with - -- all the inherited components. - - if Is_Derived_Type (Typ) then - declare - First_Comp : Node_Id; - Parent_Comps : List_Id; - Parent_Aggr : Node_Id; - Parent_Name : Node_Id; - - begin - -- Remove the inherited component association from the - -- aggregate and store them in the parent aggregate - - First_Comp := First (Component_Associations (N)); - Parent_Comps := New_List; - while Present (First_Comp) - and then - Scope (Original_Record_Component - (Entity (First (Choices (First_Comp))))) /= - Base_Typ - loop - Comp := First_Comp; - Next (First_Comp); - Remove (Comp); - Append (Comp, Parent_Comps); - end loop; - - Parent_Aggr := - Make_Aggregate (Loc, - Component_Associations => Parent_Comps); - Set_Etype (Parent_Aggr, Etype (Base_Type (Typ))); - - -- Find the _parent component - - Comp := First_Component (Typ); - while Chars (Comp) /= Name_uParent loop - Comp := Next_Component (Comp); - end loop; - - Parent_Name := New_Occurrence_Of (Comp, Loc); - - -- Insert the parent aggregate - - Prepend_To (Component_Associations (N), - Make_Component_Association (Loc, - Choices => New_List (Parent_Name), - Expression => Parent_Aggr)); - - -- Expand recursively the parent propagating the right Tag - - Expand_Record_Aggregate - (Parent_Aggr, Tag_Value, Parent_Expr); - - -- The ancestor part may be a nested aggregate that has - -- delayed expansion: recheck now. - - if Component_Not_OK_For_Backend then - Convert_To_Assignments (N, Typ); - end if; - end; - - -- For a root type, the tag component is added (unless compiling - -- for the VMs, where tags are implicit). - - elsif Tagged_Type_Expansion then - declare - Tag_Name : constant Node_Id := - New_Occurrence_Of - (First_Tag_Component (Typ), Loc); - Typ_Tag : constant Entity_Id := RTE (RE_Tag); - Conv_Node : constant Node_Id := - Unchecked_Convert_To (Typ_Tag, Tag_Value); - - begin - Set_Etype (Conv_Node, Typ_Tag); - Prepend_To (Component_Associations (N), - Make_Component_Association (Loc, - Choices => New_List (Tag_Name), - Expression => Conv_Node)); - end; - end if; - end if; - end Pass_Aggregate_To_Back_End; - ------------------------- -- Top_Level_Aggregate -- ------------------------- @@ -7101,7 +7112,7 @@ package body Exp_Aggr is -- the back-end else - Pass_Aggregate_To_Back_End; + Build_Back_End_Aggregate; end if; -- Gigi doesn't properly handle temporaries of variable size so we @@ -7178,7 +7189,7 @@ package body Exp_Aggr is -- In all other cases, build a proper aggregate to be handled by gigi else - Pass_Aggregate_To_Back_End; + Build_Back_End_Aggregate; end if; end Expand_Record_Aggregate; diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index f2c39a60f1c..385456764e0 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -3286,9 +3286,12 @@ package body Exp_Ch4 is -- very weird cases, so in the general case we need an overflow check on -- the high bound. We can avoid this for the common case of string types -- and other types whose index is Positive, since we chose a wider range - -- for the arithmetic type. + -- for the arithmetic type. If checks are suppressed we do not set the + -- flag, and possibly superfluous warnings will be omitted. - if Istyp /= Standard_Positive then + if Istyp /= Standard_Positive + and then not Overflow_Checks_Suppressed (Istyp) + then Activate_Overflow_Check (High_Bound); end if; diff --git a/gcc/ada/frontend.adb b/gcc/ada/frontend.adb index 5ad319d1fb3..dd79db5cb79 100644 --- a/gcc/ada/frontend.adb +++ b/gcc/ada/frontend.adb @@ -420,7 +420,10 @@ begin Instantiate_Bodies; end if; - if Operating_Mode = Generate_Code then + -- Analyze inlined bodies and check elaboration rules in GNATprove + -- mode as well as during compilation. + + if Operating_Mode = Generate_Code or else GNATprove_Mode then if Inline_Processing_Required then Analyze_Inlined_Bodies; end if; diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 8cd50af281b..14948d50579 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -701,10 +701,13 @@ package body SPARK_Specific is end; end loop; - for Index in Drefs.First .. Drefs.Last loop - Xrefs.Append (Drefs.Table (Index)); - Nrefs := Nrefs + 1; - end loop; + declare + Drefs_Table : Drefs.Table_Type + renames Drefs.Table (Drefs.First .. Drefs.Last); + begin + Xrefs.Append_All (Xrefs.Table_Type (Drefs_Table)); + Nrefs := Nrefs + Drefs_Table'Length; + end; -- Capture the definition Sloc values. As in the case of normal cross -- references, we have to wait until now to get the correct value. diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 92b9da6f303..10ea8a52b67 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -986,13 +986,16 @@ package body Sem_Aggr is elsif Is_Array_Type (Typ) then - -- First a special test, for the case of a positional aggregate - -- of characters which can be replaced by a string literal. + -- First a special test, for the case of a positional aggregate of + -- characters which can be replaced by a string literal. - -- Do not perform this transformation if this was a string literal to - -- start with, whose components needed constraint checks, or if the - -- component type is non-static, because it will require those checks - -- and be transformed back into an aggregate. + -- Do not perform this transformation if this was a string literal + -- to start with, whose components needed constraint checks, or if + -- the component type is non-static, because it will require those + -- checks and be transformed back into an aggregate. If the index + -- type is not Integer the aggregate may represent a user-defined + -- string type but the context might need the original type so we + -- do not perform the transformation at this point. if Number_Dimensions (Typ) = 1 and then Is_Standard_Character_Type (Component_Type (Typ)) @@ -1002,6 +1005,8 @@ package body Sem_Aggr is and then not Is_Bit_Packed_Array (Typ) and then Nkind (Original_Node (Parent (N))) /= N_String_Literal and then Is_OK_Static_Subtype (Component_Type (Typ)) + and then Base_Type (Etype (First_Index (Typ))) = + Base_Type (Standard_Integer) then declare Expr : Node_Id; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 77ab2545589..dbbb25e7f0d 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -33,6 +33,7 @@ with Einfo; use Einfo; with Errout; use Errout; with Eval_Fat; use Eval_Fat; with Exp_Ch3; use Exp_Ch3; +with Exp_Ch7; use Exp_Ch7; with Exp_Ch9; use Exp_Ch9; with Exp_Disp; use Exp_Disp; with Exp_Dist; use Exp_Dist; @@ -2153,6 +2154,17 @@ package body Sem_Ch3 is -- (They have the sloc of the label as found in the source, and that -- is ahead of the current declarative part). + procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id); + -- Create the subprogram bodies which verify the run-time semantics of + -- the pragmas listed below for each elibigle type found in declarative + -- list Decls. The pragmas are: + -- + -- Default_Initial_Condition + -- Invariant + -- Type_Invariant + -- + -- Context denotes the owner of the declarative list. + procedure Check_Entry_Contracts; -- Perform a pre-analysis of the pre- and postconditions of an entry -- declaration. This must be done before full resolution and creation @@ -2195,6 +2207,85 @@ package body Sem_Ch3 is end loop; end Adjust_Decl; + ---------------------------- + -- Build_Assertion_Bodies -- + ---------------------------- + + procedure Build_Assertion_Bodies (Decls : List_Id; Context : Node_Id) is + procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id); + -- Create the subprogram bodies which verify the run-time semantics + -- of the pragmas listed below for type Typ. The pragmas are: + -- + -- Default_Initial_Condition + -- Invariant + -- Type_Invariant + + ------------------------------------- + -- Build_Assertion_Bodies_For_Type -- + ------------------------------------- + + procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is + begin + -- Preanalyze and resolve the Default_Initial_Condition assertion + -- expression at the end of the declarations to catch any errors. + + if Has_DIC (Typ) then + Build_DIC_Procedure_Body (Typ); + end if; + + if Nkind (Context) = N_Package_Specification then + + -- Preanalyze and resolve the invariants of a private type + -- at the end of the visible declarations to catch potential + -- errors. Inherited class-wide invariants are not included + -- because they have already been resolved. + + if Decls = Visible_Declarations (Context) + and then Ekind_In (Typ, E_Limited_Private_Type, + E_Private_Type, + E_Record_Type_With_Private) + and then Has_Own_Invariants (Typ) + then + Build_Invariant_Procedure_Body + (Typ => Typ, + Partial_Invariant => True); + + -- Preanalyze and resolve the invariants of a private type's + -- full view at the end of the private declarations to catch + -- potential errors. + + elsif Decls = Private_Declarations (Context) + and then not Is_Private_Type (Typ) + and then Has_Private_Declaration (Typ) + and then Has_Invariants (Typ) + then + Build_Invariant_Procedure_Body (Typ); + end if; + end if; + end Build_Assertion_Bodies_For_Type; + + -- Local variables + + Decl : Node_Id; + Decl_Id : Entity_Id; + + -- Start of processing for Build_Assertion_Bodies + + begin + Decl := First (Decls); + while Present (Decl) loop + if Is_Declaration (Decl) then + Decl_Id := Defining_Entity (Decl); + + if Is_Type (Decl_Id) then + Build_Assertion_Bodies_For_Type (Decl_Id); + end if; + end if; + + Next (Decl); + end loop; + end Build_Assertion_Bodies; + --------------------------- -- Check_Entry_Contracts -- --------------------------- @@ -2581,11 +2672,13 @@ package body Sem_Ch3 is Decl := Next_Decl; end loop; - -- Analyze the contracts of packages and their bodies + -- Post-freezing actions if Present (L) then Context := Parent (L); + -- Analyze the contracts of packages and their bodies + if Nkind (Context) = N_Package_Specification then -- When a package has private declarations, its contract must be @@ -2643,6 +2736,15 @@ package body Sem_Ch3 is -- protected, subprogram, or task body (SPARK RM 7.2.2(3)). Check_State_Refinements (Context); + + -- Create the subprogram bodies which verify the run-time semantics + -- of pragmas Default_Initial_Condition and [Type_]Invariant for all + -- types within the current declarative list. This ensures that all + -- assertion expressions are preanalyzed and resolved at the end of + -- the declarative part. Note that the resolution happens even when + -- freezing does not take place. + + Build_Assertion_Bodies (L, Context); end if; end Analyze_Declarations; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 6e4818d6e3e..12486f252d3 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -369,31 +369,29 @@ package body Sem_Ch6 is Set_Is_Inlined (Prev); Ret_Type := Etype (Prev); - -- An expression function that is a completion freezes the - -- expression. This means freezing the return type, and if it is an - -- access type, freezing its designated type as well. + -- An expression function which acts as a completion freezes the + -- expression. This means freezing the return type, and if it is + -- an access type, freezing its designated type as well. -- Note that we cannot defer this freezing to the analysis of the -- expression itself, because a freeze node might appear in a nested -- scope, leading to an elaboration order issue in gigi. - -- An entity can only be frozen if it has a completion, so we must - -- check this explicitly. If it is declared elsewhere it will have - -- been frozen already, so only types declared in currently opened - -- scopes need to be tested. + Freeze_Before (N, Ret_Type); - if Ekind (Ret_Type) = E_Private_Type - and then In_Open_Scopes (Scope (Ret_Type)) + -- An entity can only be frozen if it is complete, so if the type + -- is still unfrozen it must still be incomplete in some way, e.g. + -- a privte type without a full view, or a type derived from such + -- in an enclosing scope. Except in a generic context, such an + -- incomplete type is an error. + + if not Is_Frozen (Ret_Type) and then not Is_Generic_Type (Ret_Type) - and then not Is_Frozen (Ret_Type) - and then No (Full_View (Ret_Type)) + and then not Inside_A_Generic then Error_Msg_NE ("premature use of private type&", Result_Definition (Specification (N)), Ret_Type); - - else - Freeze_Before (N, Ret_Type); end if; if Is_Access_Type (Etype (Prev)) then diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 4e1a27e77cc..95774e278e4 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -35,11 +35,9 @@ with Debug; use Debug; with Einfo; use Einfo; with Elists; use Elists; with Errout; use Errout; -with Exp_Ch7; use Exp_Ch7; with Exp_Disp; use Exp_Disp; with Exp_Dist; use Exp_Dist; with Exp_Dbug; use Exp_Dbug; -with Exp_Util; use Exp_Util; with Freeze; use Freeze; with Ghost; use Ghost; with Lib; use Lib; @@ -1432,30 +1430,6 @@ package body Sem_Ch7 is Error_Msg_N ("no declaration in visible part for incomplete}", E); end if; - if Is_Type (E) then - - -- Preanalyze and resolve the Default_Initial_Condition assertion - -- expression at the end of the visible declarations to catch any - -- errors. - - if Has_DIC (E) then - Build_DIC_Procedure_Body (E); - end if; - - -- Preanalyze and resolve the invariants of a private type at the - -- end of the visible declarations to catch potential errors. Note - -- that inherited class-wide invariants are not considered because - -- they have already been resolved. - - if Ekind_In (E, E_Limited_Private_Type, - E_Private_Type, - E_Record_Type_With_Private) - and then Has_Own_Invariants (E) - then - Build_Invariant_Procedure_Body (E, Partial_Invariant => True); - end if; - end if; - Next_Entity (E); end loop; @@ -1635,30 +1609,6 @@ package body Sem_Ch7 is ("full view of & does not have preelaborable initialization", E); end if; - if Is_Type (E) and then Serious_Errors_Detected > 0 then - - -- Preanalyze and resolve the Default_Initial_Condition assertion - -- expression at the end of the private declarations when freezing - -- did not take place due to errors or because the context is a - -- generic unit. - - if Has_DIC (E) then - Build_DIC_Procedure_Body (E); - end if; - - -- Preanalyze and resolve the invariants of a private type's full - -- view at the end of the private declarations in case freezing - -- did not take place either due to errors or because the context - -- is a generic unit. - - if not Is_Private_Type (E) - and then Has_Private_Declaration (E) - and then Has_Invariants (E) - then - Build_Invariant_Procedure_Body (E); - end if; - end if; - Next_Entity (E); end loop; diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index f621fa5e189..ef1a20b151a 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -932,13 +932,29 @@ package body Sem_Disp is --------------------------------- procedure Check_Dispatching_Operation (Subp, Old_Subp : Entity_Id) is - Tagged_Type : Entity_Id; - Has_Dispatching_Parent : Boolean := False; Body_Is_Last_Primitive : Boolean := False; + Has_Dispatching_Parent : Boolean := False; Ovr_Subp : Entity_Id := Empty; + Tagged_Type : Entity_Id; begin - if not Ekind_In (Subp, E_Procedure, E_Function) then + if not Ekind_In (Subp, E_Function, E_Procedure) then + return; + + -- The Default_Initial_Condition procedure is not a primitive subprogram + -- even if it relates to a tagged type. This routine is not meant to be + -- inherited or overridden. + + elsif Is_DIC_Procedure (Subp) then + return; + + -- The "partial" and "full" type invariant procedures are not primitive + -- subprograms even if they relate to a tagged type. These routines are + -- not meant to be inherited or overridden. + + elsif Is_Invariant_Procedure (Subp) + or else Is_Partial_Invariant_Procedure (Subp) + then return; end if; diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index a735393f816..89b21a0ef6a 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -112,6 +112,9 @@ package body Sem_Elab is -- The current scope of the call. This is restored when we complete the -- delayed call, so that we do this in the right scope. + From_SPARK_Code : Boolean; + -- Save indication of whether this call is under SPARK_Mode => On + From_Elab_Code : Boolean; -- Save indication of whether this call is from elaboration code @@ -1941,13 +1944,17 @@ package body Sem_Elab is ---------------------- procedure Check_Elab_Calls is + Save_SPARK_Mode : SPARK_Mode_Type; + begin - -- If expansion is disabled, do not generate any checks. Also skip + -- If expansion is disabled, do not generate any checks, unless we + -- are in GNATprove mode, so that errors are issued in GNATprove for + -- violations of static elaboration rules in SPARK code. Also skip -- checks if any subunits are missing because in either case we lack the -- full information that we need, and no object file will be created in -- any case. - if not Expander_Active + if (not Expander_Active and not GNATprove_Mode) or else Is_Generic_Unit (Cunit_Entity (Main_Unit)) or else Subunits_Missing then @@ -1964,12 +1971,21 @@ package body Sem_Elab is Push_Scope (Delay_Check.Table (J).Curscop); From_Elab_Code := Delay_Check.Table (J).From_Elab_Code; + -- Set appropriate value of SPARK_Mode + + Save_SPARK_Mode := SPARK_Mode; + + if Delay_Check.Table (J).From_SPARK_Code then + SPARK_Mode := On; + end if; + Check_Internal_Call_Continue ( N => Delay_Check.Table (J).N, E => Delay_Check.Table (J).E, Outer_Scope => Delay_Check.Table (J).Outer_Scope, Orig_Ent => Delay_Check.Table (J).Orig_Ent); + SPARK_Mode := Save_SPARK_Mode; Pop_Scope; end loop; @@ -2223,12 +2239,13 @@ package body Sem_Elab is if Delaying_Elab_Checks then Delay_Check.Append ( - (N => N, - E => E, - Orig_Ent => Orig_Ent, - Curscop => Current_Scope, - Outer_Scope => Outer_Scope, - From_Elab_Code => From_Elab_Code)); + (N => N, + E => E, + Orig_Ent => Orig_Ent, + Curscop => Current_Scope, + Outer_Scope => Outer_Scope, + From_Elab_Code => From_Elab_Code, + From_SPARK_Code => SPARK_Mode = On)); return; -- Otherwise, call phase 2 continuation right now