From 9f90d12301fa640d4664b7924cbacb75e9e304d2 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 2 Aug 2011 09:42:46 +0200 Subject: [PATCH] [multiple changes] 2011-08-02 Robert Dewar * gnat_rm.texi: Minor reformatting. * sem_prag.adb: Minor reformatting. 2011-08-02 Tristan Gingold * vms_data.ads: Add VMS qualifier for -gnateP. 2011-08-02 Robert Dewar * par-ch13.adb (P_Aspect_Specification): New meaning of Decl = Empty * par-ch7.adb (P_Package): Proper placement of aspects for package decl/instantiation. * par-endh.adb (Check_End): Ad Is_Sloc parameter (End_Statements): Add Is_Sloc parameterr * par.adb (P_Aspect_Specification): New meaning of Decl = Empty (Check_End): Ad Is_Sloc parameter (End_Statements): Add Is_Sloc parameterr 2011-08-02 Vincent Celier * ug_words: Add VMS qualifier equivalent to -gnateP: /SYMBOL_PREPROCESSING. 2011-08-02 Jose Ruiz * gnat-style.texi: For hexadecimal numeric literals the typical grouping of digits is 4 to represent 2 bytes. A procedure spec which is split into several lines is indented two characters. 2011-08-02 Yannick Moy * exp_aggr.adb (Is_Others_Aggregate): move function to other unit. * sem_aggr.adb, sem_aggr.ads (Is_Others_Aggregate): move function here (Resolve_Aggregate): issue errors in formal modes when aggregate is not properly qualified (Resolve_Array_Aggregate): issue errors in formal modes on non-static choice in array aggregate (Resolve_Extension_Aggregate): issue errors in formal modes on subtype mark as ancestor (Resolve_Record_Aggregate): issue errors in formal modes on mixed positional and named aggregate for record, or others in record aggregate, or multiple choice in record aggregate * sem_res.adb (Resolve_Logical_Op): issue errors in formal mode when array operands to logical operations AND, OR and XOR do not have the same static lower and higher bounds * sem_ch5.adb, sinfo.ads: Correct typos in comments From-SVN: r177086 --- gcc/ada/ChangeLog | 50 +++++++++++++++++++ gcc/ada/exp_aggr.adb | 17 +------ gcc/ada/gnat-style.texi | 10 ++-- gcc/ada/gnat_rm.texi | 20 +++++--- gcc/ada/par-ch13.adb | 16 +++++- gcc/ada/par-ch7.adb | 34 +++++++++++-- gcc/ada/par-endh.adb | 36 +++++++++++--- gcc/ada/par.adb | 38 +++++++++++--- gcc/ada/sem_aggr.adb | 107 ++++++++++++++++++++++++++++++++++++++++ gcc/ada/sem_aggr.ads | 5 +- gcc/ada/sem_ch5.adb | 2 +- gcc/ada/sem_prag.adb | 4 ++ gcc/ada/sem_res.adb | 51 +++++++++++++++++++ gcc/ada/ug_words | 1 + gcc/ada/vms_data.ads | 14 ++++++ 15 files changed, 355 insertions(+), 50 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9cfb1e2b753..8702efb41f2 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,53 @@ +2011-08-02 Robert Dewar + + * gnat_rm.texi: Minor reformatting. + * sem_prag.adb: Minor reformatting. + +2011-08-02 Tristan Gingold + + * vms_data.ads: Add VMS qualifier for -gnateP. + +2011-08-02 Robert Dewar + + * par-ch13.adb (P_Aspect_Specification): New meaning of Decl = Empty + * par-ch7.adb (P_Package): Proper placement of aspects for package + decl/instantiation. + * par-endh.adb (Check_End): Ad Is_Sloc parameter + (End_Statements): Add Is_Sloc parameterr + * par.adb (P_Aspect_Specification): New meaning of Decl = Empty + (Check_End): Ad Is_Sloc parameter + (End_Statements): Add Is_Sloc parameterr + +2011-08-02 Vincent Celier + + * ug_words: Add VMS qualifier equivalent to -gnateP: + /SYMBOL_PREPROCESSING. + +2011-08-02 Jose Ruiz + + * gnat-style.texi: For hexadecimal numeric literals the typical + grouping of digits is 4 to represent 2 bytes. + A procedure spec which is split into several lines is indented two + characters. + +2011-08-02 Yannick Moy + + * exp_aggr.adb (Is_Others_Aggregate): move function to other unit. + * sem_aggr.adb, sem_aggr.ads (Is_Others_Aggregate): move function here + (Resolve_Aggregate): issue errors in formal modes when aggregate is not + properly qualified + (Resolve_Array_Aggregate): issue errors in formal modes on non-static + choice in array aggregate + (Resolve_Extension_Aggregate): issue errors in formal modes on subtype + mark as ancestor + (Resolve_Record_Aggregate): issue errors in formal modes on mixed + positional and named aggregate for record, or others in record + aggregate, or multiple choice in record aggregate + * sem_res.adb (Resolve_Logical_Op): issue errors in formal mode when + array operands to logical operations AND, OR and XOR do not have the + same static lower and higher bounds + * sem_ch5.adb, sinfo.ads: Correct typos in comments + 2011-08-01 Robert Dewar * sem_util.ads, sem_util.adb, sem_ch6.adb (Last_Source_Statement): diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 871de86154d..536b317cab8 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -49,6 +49,7 @@ with Rident; use Rident; with Rtsfind; use Rtsfind; with Ttypes; use Ttypes; with Sem; use Sem; +with Sem_Aggr; use Sem_Aggr; with Sem_Aux; use Sem_Aux; with Sem_Ch3; use Sem_Ch3; with Sem_Eval; use Sem_Eval; @@ -4510,10 +4511,6 @@ package body Exp_Aggr is Obj_Lo : Node_Id; Obj_Hi : Node_Id; - function Is_Others_Aggregate (Aggr : Node_Id) return Boolean; - -- Aggregates that consist of a single Others choice are safe - -- if the single expression is. - function Safe_Aggregate (Aggr : Node_Id) return Boolean; -- Check recursively that each component of a (sub)aggregate does -- not depend on the variable being assigned to. @@ -4522,18 +4519,6 @@ package body Exp_Aggr is -- Verify that an expression cannot depend on the variable being -- assigned to. Room for improvement here (but less than before). - ------------------------- - -- Is_Others_Aggregate -- - ------------------------- - - function Is_Others_Aggregate (Aggr : Node_Id) return Boolean is - begin - return No (Expressions (Aggr)) - and then Nkind - (First (Choices (First (Component_Associations (Aggr))))) - = N_Others_Choice; - end Is_Others_Aggregate; - -------------------- -- Safe_Aggregate -- -------------------- diff --git a/gcc/ada/gnat-style.texi b/gcc/ada/gnat-style.texi index 1e2f365f351..1bba7030935 100644 --- a/gcc/ada/gnat-style.texi +++ b/gcc/ada/gnat-style.texi @@ -196,7 +196,7 @@ readability. @smallexample 1_000_000 - 16#8000_000# + 16#8000_0000# 3.14159_26535_89793_23846 @end smallexample @end itemize @@ -637,10 +637,10 @@ the colons, as in: @smallexample @c adanocomment @group procedure Set_Heading - (Source : String; - Count : Natural; - Pad : Character := Space; - Fill : Boolean := True); + (Source : String; + Count : Natural; + Pad : Character := Space; + Fill : Boolean := True); @end group @end smallexample diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi index 4849daab97c..85fb454101f 100644 --- a/gcc/ada/gnat_rm.texi +++ b/gcc/ada/gnat_rm.texi @@ -4613,21 +4613,27 @@ pragma SPARK_95; @end smallexample @noindent -A configuration pragma that establishes SPARK 95 mode for the unit to which +This is a configuration pragma that establishes SPARK 95 mode +for the unit to which it applies, regardless of the mode set by the command line switches. -In this mode, the compiler rejects constructs outside the SPARK 95 subset of -Ada, which provides a useful initial filter for those projects developed in -SPARK. Syntax and semantic error messages related to SPARK restrictions have -the form: +In this mode, the compiler rejects constructs not permitted by SPARK 95. +Error messages related to SPARK restrictions have the form: @code{(spark) error message}. This is not a replacement for the semantic checks performed by the SPARK Examiner tool, as the compiler only deals currently with code, -not at all with SPARK annotations, so it may well be the case that code which +not at all with SPARK annotations and does not guarantee catching all +cases of constructs forbidden by SPARK 95. + +Thus it may well be the case that code which passes the compiler in SPARK 95 mode is rejected by the SPARK Examiner, e.g. due to the different visibility rules of the Examiner based on -@code{inherit} SPARK annotations. +SPARK @code{inherit} annotations. + +SPARK 95 mode can be useful in providing an initial filter for +code developed using SPARK 95, or in examining legacy code to see how far +it is from meeting SPARK 95 restrictions. @node Pragma Static_Elaboration_Desired @unnumberedsec Pragma Static_Elaboration_Desired diff --git a/gcc/ada/par-ch13.adb b/gcc/ada/par-ch13.adb index e3f72c7d428..95da89c19f9 100644 --- a/gcc/ada/par-ch13.adb +++ b/gcc/ada/par-ch13.adb @@ -556,11 +556,23 @@ package body Ch13 is end if; end loop; - -- If aspects scanned, store them + -- Here if aspects present if Is_Non_Empty_List (Aspects) then - if Decl = Error then + + -- If Decl is Empty, we just ignore the aspects (the caller in this + -- case has always issued an appropriate error message). + + if Decl = Empty then + null; + + -- If Decl is Error, we ignore the aspects, and issue a message + + elsif Decl = Error then Error_Msg ("aspect specifications not allowed here", Ptr); + + -- Here aspects are allowed, and we store them + else Set_Parent (Aspects, Decl); Set_Aspect_Specifications (Decl, Aspects); diff --git a/gcc/ada/par-ch7.adb b/gcc/ada/par-ch7.adb index 45a0fb1beb6..d05aa889801 100644 --- a/gcc/ada/par-ch7.adb +++ b/gcc/ada/par-ch7.adb @@ -98,6 +98,13 @@ package body Ch7 is Name_Node : Node_Id; Package_Sloc : Source_Ptr; + Aspect_Sloc : Source_Ptr := No_Location; + -- Save location of WITH for scanned aspects. Left set to No_Location + -- if no aspects scanned before the IS keyword. + + Is_Sloc : Source_Ptr; + -- Save location of IS token for package declaration + Dummy_Node : constant Node_Id := New_Node (N_Package_Specification, Token_Ptr); -- Dummy node to attach aspect specifications to until we properly @@ -178,7 +185,12 @@ package body Ch7 is -- Generic package instantiation or package declaration else - P_Aspect_Specifications (Dummy_Node, Semicolon => False); + if Aspect_Specifications_Present then + Aspect_Sloc := Token_Ptr; + P_Aspect_Specifications (Dummy_Node, Semicolon => False); + end if; + + Is_Sloc := Token_Ptr; TF_Is; -- Case of generic instantiation @@ -189,6 +201,12 @@ package body Ch7 is ("generic instantiation cannot appear here!"); end if; + if Aspect_Sloc /= No_Location then + Error_Msg + ("misplaced aspects for package instantiation", + Aspect_Sloc); + end if; + Scan; -- past NEW Package_Node := @@ -197,7 +215,15 @@ package body Ch7 is Set_Name (Package_Node, P_Qualified_Simple_Name); Set_Generic_Associations (Package_Node, P_Generic_Actual_Part_Opt); - P_Aspect_Specifications (Error); + + if Aspect_Sloc /= No_Location + and then not Aspect_Specifications_Present + then + Error_Msg_SC ("\info: aspect specifications belong here"); + Move_Aspects (From => Dummy_Node, To => Package_Node); + end if; + + P_Aspect_Specifications (Package_Node); Pop_Scope_Stack; -- Case of package declaration or package specification @@ -251,12 +277,12 @@ package body Ch7 is Discard_Junk_List (P_Sequence_Of_Statements (SS_None)); end if; - End_Statements (Specification_Node); + End_Statements (Specification_Node, Empty, Is_Sloc); + Move_Aspects (From => Dummy_Node, To => Package_Node); end if; end if; end if; - Move_Aspects (From => Dummy_Node, To => Package_Node); return Package_Node; end P_Package; diff --git a/gcc/ada/par-endh.adb b/gcc/ada/par-endh.adb index 12c5509e431..8b0897e1a83 100644 --- a/gcc/ada/par-endh.adb +++ b/gcc/ada/par-endh.adb @@ -166,7 +166,10 @@ package body Endh is -- Check_End -- --------------- - function Check_End (Decl : Node_Id := Empty) return Boolean is + function Check_End + (Decl : Node_Id := Empty; + Is_Loc : Source_Ptr := No_Location) return Boolean + is Name_On_Separate_Line : Boolean; -- Set True if the name on an END line is on a separate source line -- from the END. This is highly suspicious, but is allowed. The point @@ -401,11 +404,31 @@ package body Endh is if End_Type /= E_Record then - -- Scan aspect specifications if permitted here + -- Scan aspect specifications if Aspect_Specifications_Present then + + -- Aspect specifications not allowed + if No (Decl) then - P_Aspect_Specifications (Error); + + -- Package declaration case + + if Is_Loc /= No_Location then + Error_Msg_SC + ("misplaced aspects for package declaration"); + Error_Msg + ("info: aspect specifications belong here", Is_Loc); + P_Aspect_Specifications (Empty); + + -- Other cases where aspect specifications are not allowed + + else + P_Aspect_Specifications (Error); + end if; + + -- Aspect specifications allowed + else P_Aspect_Specifications (Decl); end if; @@ -664,15 +687,16 @@ package body Endh is -- Error recovery: cannot raise Error_Resync; procedure End_Statements - (Parent : Node_Id := Empty; - Decl : Node_Id := Empty) + (Parent : Node_Id := Empty; + Decl : Node_Id := Empty; + Is_Sloc : Source_Ptr := No_Location) is begin -- This loop runs more than once in the case where Check_End rejects -- the END sequence, as indicated by Check_End returning False. loop - if Check_End (Decl) then + if Check_End (Decl, Is_Sloc) then if Present (Parent) then Set_End_Label (Parent, End_Labl); end if; diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index 99f6806057d..4d3e379f938 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -870,7 +870,6 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- Semicolon is True, a terminating semicolon is also scanned. If this -- argument is False, the scan pointer is left pointing past the aspects -- and the caller must check for a proper terminator. - -- left pointing past the aspects, presumably pointing to a terminator. -- -- P_Aspect_Specification is called with the current token pointing to -- either a WITH keyword starting an aspect specification, or an @@ -880,9 +879,13 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- the given declaration node. A list of aspects is built and stored for -- this declaration node using a call to Set_Aspect_Specifications. If -- no WITH keyword is present, then this call has no effect other than - -- scanning out the terminator if it is a semicolon. If Decl is Error on - -- entry, any scanned aspect specifications are ignored and a message is - -- output saying aspect specifications not permitted here. + -- scanning out the terminator if it is a semicolon. + + -- If Decl is Error on entry, any scanned aspect specifications are + -- ignored and a message is output saying aspect specifications not + -- permitted here. If Decl is Empty, then scanned aspect specifications + -- are also ignored, but no error message is given (this is used when + -- the caller has already taken care of the error message). function P_Code_Statement (Subtype_Mark : Node_Id) return Node_Id; -- Function to parse a code statement. The caller has scanned out @@ -908,7 +911,9 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- Routines for handling end lines, including scope recovery package Endh is - function Check_End (Decl : Node_Id := Empty) return Boolean; + function Check_End + (Decl : Node_Id := Empty; + Is_Loc : Source_Ptr := No_Location) return Boolean; -- Called when an end sequence is required. In the absence of an error -- situation, Token contains Tok_End on entry, but in a missing end -- case, this may not be the case. Pop_End_Context is used to determine @@ -922,7 +927,15 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- -- If Decl is non-empty, then aspect specifications are permitted -- following the end, and Decl is the declaration node with which - -- these aspect specifications are to be associated. + -- these aspect specifications are to be associated. If Decl is empty, + -- then aspect specifications are not permitted and will generate an + -- error message. + -- + -- Is_Loc is set to other than the default only for the case of a + -- package declaration. It points to the IS keyword of the declaration, + -- and is used to specialize the error messages for misplaced aspect + -- specifications in this case. Note that Decl is always Empty if Is_Loc + -- is set. procedure End_Skip; -- Skip past an end sequence. On entry Token contains Tok_End, and we @@ -933,8 +946,9 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- error messages while carrying this out. procedure End_Statements - (Parent : Node_Id := Empty; - Decl : Node_Id := Empty); + (Parent : Node_Id := Empty; + Decl : Node_Id := Empty; + Is_Sloc : Source_Ptr := No_Location); -- Called when an end is required or expected to terminate a sequence -- of statements. The caller has already made an appropriate entry in -- the Scope.Table to describe the expected form of the end. This can @@ -945,6 +959,14 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- If Decl is non-null, then it is a declaration node, and aspect -- specifications are permitted after the end statement. These aspect -- specifications, if present, are stored in this declaration node. + -- If Decl is null, then aspect specifications are not permitted after + -- the end statement. + -- + -- In the case where Decl is null, Is_Sloc determines the handling. If + -- it is set to No_Location, then aspect specifications are ignored and + -- an error message is given. Is_Sloc is used in the package declaration + -- case to point to the IS, and is used to specialize the error emssages + -- issued in this case. end Endh; -------------- diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 1d75a3c75a9..3800008954a 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -848,6 +848,18 @@ package body Sem_Aggr is Set_Size_Known_At_Compile_Time (T); end Check_Static_Discriminated_Subtype; + ------------------------- + -- Is_Others_Aggregate -- + ------------------------- + + function Is_Others_Aggregate (Aggr : Node_Id) return Boolean is + begin + return No (Expressions (Aggr)) + and then + Nkind (First (Choices (First (Component_Associations (Aggr))))) + = N_Others_Choice; + end Is_Others_Aggregate; + -------------------------------- -- Make_String_Into_Aggregate -- -------------------------------- @@ -1085,6 +1097,45 @@ package body Sem_Aggr is Error_Msg_N ("illegal context for aggregate", N); end if; + if Formal_Verification_Mode and then Comes_From_Source (N) then + + -- An unqualified aggregate is restricted in SPARK or ALFA to: + -- An 'aggregate item' inside an multi-dimensional aggregate + -- An expression being assigned to an unconstrained array, but only + -- if the aggregate specifies a value for OTHERS only. + + if Nkind (Parent (N)) /= N_Qualified_Expression then + if Is_Array_Type (Etype (N)) then + if Nkind (Parent (N)) = N_Assignment_Statement + and then not Is_Constrained (Etype (Name (Parent (N)))) + then + if not Is_Others_Aggregate (N) then + Error_Msg_F + ("|~~array aggregate should have only OTHERS", N); + end if; + + elsif not (Nkind (Parent (N)) = N_Aggregate + and then Is_Array_Type (Etype (Parent (N))) + and then Number_Dimensions (Etype (Parent (N))) > 1) + then + Error_Msg_F ("|~~array aggregate should be qualified", N); + else + null; + end if; + + elsif Is_Record_Type (Etype (N)) then + Error_Msg_F ("|~~record aggregate should be qualified", N); + + -- The type of aggregate is neither array nor record, so an error + -- must have occurred during resolution. Do not report an + -- additional message here. + + else + null; + end if; + end if; + end if; + -- If we can determine statically that the evaluation of the aggregate -- raises Constraint_Error, then replace the aggregate with an -- N_Raise_Constraint_Error node, but set the Etype to the right @@ -1731,6 +1782,15 @@ package body Sem_Aggr is -- bounds of the array aggregate are within range. Set_Do_Range_Check (Choice, False); + + -- In SPARK or ALFA, the choice must be static + + if Formal_Verification_Mode + and then Comes_From_Source (Original_Node (Choice)) + and then not Is_Static_Expression (Choice) + then + Error_Msg_F ("|~~choice should be static", Choice); + end if; end if; -- If we could not resolve the discrete choice stop here @@ -2372,6 +2432,16 @@ package body Sem_Aggr is Analyze (A); Check_Parameterless_Call (A); + -- In SPARK or ALFA, the ancestor part cannot be a subtype mark + + if Formal_Verification_Mode + and then Comes_From_Source (N) + and then Is_Entity_Name (A) + and then Is_Type (Entity (A)) + then + Error_Msg_F ("|~~ancestor part cannot be a subtype mark", A); + end if; + if not Is_Tagged_Type (Typ) then Error_Msg_N ("type of extension aggregate must be tagged", N); return; @@ -3043,6 +3113,43 @@ package body Sem_Aggr is -- Start of processing for Resolve_Record_Aggregate begin + -- A record aggregate is restricted in SPARK or ALFA: + -- Each named association can have only a single choice. + -- OTHERS cannot be used. + -- Positional and named associations cannot be mixed. + + if Formal_Verification_Mode + and then Comes_From_Source (N) + and then Present (Component_Associations (N)) + then + if Present (Expressions (N)) then + Error_Msg_F + ("|~~named association cannot follow positional association", + First (Choices (First (Component_Associations (N))))); + end if; + + declare + Assoc : Node_Id; + + begin + Assoc := First (Component_Associations (N)); + while Present (Assoc) loop + if List_Length (Choices (Assoc)) > 1 then + Error_Msg_F + ("|~~component association in record aggregate must " + & "contain a single choice", Assoc); + end if; + + if Nkind (First (Choices (Assoc))) = N_Others_Choice then + Error_Msg_F + ("|~~record aggregate cannot contain OTHERS", Assoc); + end if; + + Assoc := Next (Assoc); + end loop; + end; + end if; + -- We may end up calling Duplicate_Subexpr on expressions that are -- attached to New_Assoc_List. For this reason we need to attach it -- to the tree by setting its parent pointer to N. This parent point diff --git a/gcc/ada/sem_aggr.ads b/gcc/ada/sem_aggr.ads index 86adccafb02..597ffe47574 100644 --- a/gcc/ada/sem_aggr.ads +++ b/gcc/ada/sem_aggr.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2007, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -33,4 +33,7 @@ package Sem_Aggr is procedure Resolve_Aggregate (N : Node_Id; Typ : Entity_Id); procedure Resolve_Extension_Aggregate (N : Node_Id; Typ : Entity_Id); + function Is_Others_Aggregate (Aggr : Node_Id) return Boolean; + -- Returns True is aggregate Aggr consists of a single OTHERS choice + end Sem_Aggr; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 1673e5365ca..a6d4e4ab6f6 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -1101,7 +1101,7 @@ package body Sem_Ch5 is Analyze_Choices (N, Exp_Type, Dont_Care, Others_Present); - -- A case statement with a single "others" alternative is not allowed + -- A case statement with a single OTHERS alternative is not allowed -- in SPARK or ALFA. if Formal_Verification_Mode diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d2528acfc75..c42f8bbd999 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -4406,6 +4406,10 @@ package body Sem_Prag is else Make_Inline (Subp); + -- For the pragma case, climb homonym chain. This is + -- what implements allowing the pragma in the renaming + -- case, with the result applying to the ancestors. + if not From_Aspect_Specification (N) then while Present (Homonym (Subp)) and then Scope (Homonym (Subp)) = Current_Scope diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 6cda48eb764..319b2ff8295 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7156,6 +7156,57 @@ package body Sem_Res is Set_Etype (N, B_Typ); Generate_Operator_Reference (N, B_Typ); Eval_Logical_Op (N); + + -- In SPARK or ALFA, logical operations AND, OR and XOR for arrays are + -- defined only when both operands have same static lower and higher + -- bounds. + + if Formal_Verification_Mode + and then Comes_From_Source (Original_Node (N)) + and then Is_Array_Type (Etype (N)) + then + declare + L_Index : Node_Id; + R_Index : Node_Id; + L_Low : Node_Id; + L_High : Node_Id; + R_Low : Node_Id; + R_High : Node_Id; + + L_Typ : constant Node_Id := Etype (Left_Opnd (N)); + R_Typ : constant Node_Id := Etype (Right_Opnd (N)); + + begin + L_Index := First_Index (L_Typ); + R_Index := First_Index (R_Typ); + + Get_Index_Bounds (L_Index, L_Low, L_High); + Get_Index_Bounds (R_Index, R_Low, R_High); + + -- Another error is issued for constrained array types with + -- non-static bounds elsewhere, so only deal with different + -- constrained types, or unconstrained types. + + if L_Typ /= R_Typ or else not Is_Constrained (L_Typ) then + if not Is_Static_Expression (L_Low) + or else not Is_Static_Expression (R_Low) + or else Expr_Value (L_Low) /= Expr_Value (R_Low) + then + Error_Msg_F ("|~~operation defined only when both operands " + & "have the same static lower bound", N); + end if; + + if not Is_Static_Expression (L_High) + or else not Is_Static_Expression (R_High) + or else Expr_Value (L_High) /= Expr_Value (R_High) + then + Error_Msg_F ("|~~operation defined only when both operands " + & "have the same static higher bound", N); + end if; + end if; + end; + end if; + end Resolve_Logical_Op; --------------------------- diff --git a/gcc/ada/ug_words b/gcc/ada/ug_words index aedfc0fe882..eb0a57bbc4a 100644 --- a/gcc/ada/ug_words +++ b/gcc/ada/ug_words @@ -65,6 +65,7 @@ gcc -c ^ GNAT COMPILE -gnateG ^ /GENERATE_PROCESSED_SOURCE -gnatem ^ /MAPPING_FILE -gnatep ^ /DATA_PREPROCESSING +-gnateP ^ /CATEGORIZATION_WARNINGS -gnateS ^ /SCO_OUTPUT -gnatE ^ /CHECKS=ELABORATION -gnatf ^ /REPORT_ERRORS=FULL diff --git a/gcc/ada/vms_data.ads b/gcc/ada/vms_data.ads index 7b482827f5e..3d66e1833b6 100644 --- a/gcc/ada/vms_data.ads +++ b/gcc/ada/vms_data.ads @@ -1293,6 +1293,19 @@ package VMS_Data is -- be sure that they are valid, and code is generated to allow for this -- possibility. The use of /ASSUME_VALID will improve the code. + S_GCC_CategW : aliased constant S := "/CATEGORIZATION_WARNINGS " & + "-gnateP"; + -- /NO_CATEGORIZATION_WARNINGS (D) + -- /CATEGORIZATION_WARNINGS + -- + -- Use to tell the compiler to disable categorization dependency errors. + -- Ada requires that units that WITH one another have compatible + -- categories, for example a Pure unit cannot WITH a Preelaborate unit. + -- If this switch is used, these errors become warnings (which can be + -- ignored, or suppressed in the usual manner). This can be useful in + -- some specialized circumstances such as the temporary use of special + -- test software. + S_GCC_Checks : aliased constant S := "/CHECKS=" & "FULL " & "-gnato,!-gnatE,!-gnatp " & @@ -3517,6 +3530,7 @@ package VMS_Data is S_GCC_Add 'Access, S_GCC_Asm 'Access, S_GCC_AValid 'Access, + S_GCC_CategW 'Access, S_GCC_Checks 'Access, S_GCC_ChecksX 'Access, S_GCC_Compres 'Access, -- 2.30.2