From 8ed68165ed9a61e0e0a0d3de377d37718ee24b61 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 1 Aug 2011 17:51:41 +0200 Subject: [PATCH] [multiple changes] 2011-08-01 Yannick Moy * sem_util.ads, sem_util.adb, par.adb, par_util.adb (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move procedures out of these packages. * errout.ads, errout.adb (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move procedures in of this package (Formal_Error_Msg_NE): new procedure for wrapper on Error_Msg_NE * par-ch5.adb (Parse_Decls_Begin_End): issue syntax error in SPARK mode on misplaced later vs initial declarations, like in Ada 83 * sem_attr.adb (Processing for Analyze_Attribute): issue error in formal mode on attribute of private type whose full type declaration is not visible * sem_ch3.adb (Analyze_Declarations): issue error in formal mode on a package declaration inside a package specification (Analyze_Full_Type_Declaration): issue error in formal mode on controlled type or discriminant type * sem_ch6.adb (Analyze_Subprogram_Specification): only issue error on user-defined operator means that it should come from the source (New_Overloaded_Entity): issue error in formal mode on overloaded entity. * sem_ch6.ads, sem_ch13.ads: typos in comments. 2011-08-01 Thomas Quinot * atree.adb: Minor reformatting. * checks.adb: Minor reformatting. From-SVN: r177052 --- gcc/ada/ChangeLog | 29 +++++++++++++++++++++++++++++ gcc/ada/atree.adb | 6 +++--- gcc/ada/checks.adb | 13 ++++++++++--- gcc/ada/errout.adb | 43 +++++++++++++++++++++++++++++++++++++++++++ gcc/ada/errout.ads | 19 +++++++++++++++++++ gcc/ada/par-ch5.adb | 12 ++++++++++-- gcc/ada/par-util.adb | 10 ---------- gcc/ada/par.adb | 4 ---- gcc/ada/sem_attr.adb | 14 ++++++++++++++ gcc/ada/sem_ch13.ads | 6 +++--- gcc/ada/sem_ch3.adb | 26 ++++++++++++++++++++++++++ gcc/ada/sem_ch6.adb | 10 ++++++++++ gcc/ada/sem_ch6.ads | 2 +- gcc/ada/sem_util.adb | 22 +--------------------- gcc/ada/sem_util.ads | 8 -------- 15 files changed, 169 insertions(+), 55 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index dcbdad8c4a9..810203732bd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2011-08-01 Yannick Moy + + * sem_util.ads, sem_util.adb, par.adb, par_util.adb + (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move + procedures out of these packages. + * errout.ads, errout.adb + (Formal_Error_Msg, Formal_Error_Msg_N, Formal_Error_Msg_SP): move + procedures in of this package + (Formal_Error_Msg_NE): new procedure for wrapper on Error_Msg_NE + * par-ch5.adb (Parse_Decls_Begin_End): issue syntax error in SPARK mode + on misplaced later vs initial declarations, like in Ada 83 + * sem_attr.adb (Processing for Analyze_Attribute): issue error in + formal mode on attribute of private type whose full type declaration + is not visible + * sem_ch3.adb (Analyze_Declarations): issue error in formal mode on a + package declaration inside a package specification + (Analyze_Full_Type_Declaration): issue error in formal mode on + controlled type or discriminant type + * sem_ch6.adb (Analyze_Subprogram_Specification): only issue error on + user-defined operator means that it should come from the source + (New_Overloaded_Entity): issue error in formal mode on overloaded + entity. + * sem_ch6.ads, sem_ch13.ads: typos in comments. + +2011-08-01 Thomas Quinot + + * atree.adb: Minor reformatting. + * checks.adb: Minor reformatting. + 2011-08-01 Vincent Celier * s-parame-vms-ia64.ads: Fix typo in comment diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 7852d1de1d5..d0a9cc29229 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -1196,14 +1196,14 @@ package body Atree is Nodes.Table (New_Id).Link := Empty_List_Or_Node; Nodes.Table (New_Id).In_List := False; - -- If the original is marked as a rewrite insertion, then unmark - -- the copy, since we inserted the original, not the copy. + -- If the original is marked as a rewrite insertion, then unmark the + -- copy, since we inserted the original, not the copy. Nodes.Table (New_Id).Rewrite_Ins := False; pragma Debug (New_Node_Debugging_Output (New_Id)); -- Clear Is_Overloaded since we cannot have semantic interpretations - -- of this new node + -- of this new node. if Nkind (Source) in N_Subexpr then Set_Is_Overloaded (New_Id, False); diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb index e45f013fd2e..62dd861557c 100644 --- a/gcc/ada/checks.adb +++ b/gcc/ada/checks.adb @@ -4560,6 +4560,10 @@ package body Checks is function Entity_Of_Prefix return Entity_Id; -- Returns the entity of the prefix of N (or Empty if not found) + ---------------------- + -- Entity_Of_Prefix -- + ---------------------- + function Entity_Of_Prefix return Entity_Id is P : Node_Id := Prefix (N); begin @@ -4583,6 +4587,8 @@ package body Checks is A_Ent : constant Entity_Id := Entity_Of_Prefix; Sub : Node_Id; + -- Start of processing for Generate_Index_Checks + begin -- Ignore call if the prefix is not an array since we have a serious -- error in the sources. Ignore it also if index checks are suppressed @@ -4599,7 +4605,7 @@ package body Checks is -- Generate a raise of constraint error with the appropriate reason and -- a condition of the form: - -- Base_Type(Sub) not in array'range (subscript) + -- Base_Type (Sub) not in Array'Range (Subscript) -- Note that the reason we generate the conversion to the base type here -- is that we definitely want the range check to take place, even if it @@ -4627,7 +4633,7 @@ package body Checks is Duplicate_Subexpr_Move_Checks (Sub)), Right_Opnd => Make_Attribute_Reference (Loc, - Prefix => New_Reference_To (Etype (A), Loc), + Prefix => New_Reference_To (Etype (A), Loc), Attribute_Name => Name_Range)), Reason => CE_Index_Check_Failed)); end if; @@ -4680,7 +4686,8 @@ package body Checks is then Range_N := Make_Attribute_Reference (Loc, - Prefix => New_Reference_To (Etype (A_Idx), Loc), + Prefix => + New_Reference_To (Etype (A_Idx), Loc), Attribute_Name => Name_Range); -- For arrays with non-constant bounds we cannot generate diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 0fb8f9e1278..0703afc89a7 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -1402,6 +1402,49 @@ package body Errout is return S; end First_Sloc; + ---------------------- + -- Formal_Error_Msg -- + ---------------------- + + procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is + begin + pragma Assert (Formal_Verification_Mode); + Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location); + end Formal_Error_Msg; + + ------------------------ + -- Formal_Error_Msg_N -- + ------------------------ + + procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is + begin + pragma Assert (Formal_Verification_Mode); + Error_Msg_N ("(" & Formal_Language & ") " & Msg, N); + end Formal_Error_Msg_N; + + ------------------------- + -- Formal_Error_Msg_NE -- + ------------------------- + + procedure Formal_Error_Msg_NE + (Msg : String; + N : Node_Or_Entity_Id; + E : Node_Or_Entity_Id) is + begin + pragma Assert (Formal_Verification_Mode); + Error_Msg_NE ("(" & Formal_Language & ") " & Msg, N, E); + end Formal_Error_Msg_NE; + + ------------------------- + -- Formal_Error_Msg_SP -- + ------------------------- + + procedure Formal_Error_Msg_SP (Msg : String) is + begin + pragma Assert (Formal_Verification_Mode); + Error_Msg_SP ("(" & Formal_Language & ") " & Msg); + end Formal_Error_Msg_SP; + ---------------- -- Initialize -- ---------------- diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index e9ddb7e3e87..af219647a57 100644 --- a/gcc/ada/errout.ads +++ b/gcc/ada/errout.ads @@ -735,6 +735,25 @@ package Errout is -- where the expression is parenthesized, an attempt is made to include -- the parentheses (i.e. to return the location of the initial paren). + procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr); + -- Wrapper on Error_Msg which adds a prefix to Msg giving the name of + -- the formal language analyzed (spark or alfa) + + procedure Formal_Error_Msg_N (Msg : String; N : Node_Id); + -- Wrapper on Error_Msg_N which adds a prefix to Msg giving the name of + -- the formal language analyzed (spark or alfa) + + procedure Formal_Error_Msg_NE + (Msg : String; + N : Node_Or_Entity_Id; + E : Node_Or_Entity_Id); + -- Wrapper on Error_Msg_NE which adds a prefix to Msg giving the name of + -- the formal language analyzed (spark or alfa) + + procedure Formal_Error_Msg_SP (Msg : String); + -- Wrapper on Error_Msg_SP which adds a prefix to Msg giving the name of + -- the formal language analyzed (spark or alfa) + procedure Purge_Messages (From : Source_Ptr; To : Source_Ptr) renames Erroutc.Purge_Messages; -- All error messages whose location is in the range From .. To (not diff --git a/gcc/ada/par-ch5.adb b/gcc/ada/par-ch5.adb index 1949595720b..acea49b7445 100644 --- a/gcc/ada/par-ch5.adb +++ b/gcc/ada/par-ch5.adb @@ -2110,9 +2110,12 @@ package body Ch5 is begin Decls := P_Declarative_Part; - -- Check for misplacement of later vs basic declarations in Ada 83 + -- Check for misplacement of later vs basic declarations in Ada 83. + -- The same is true for the SPARK mode: although SPARK 95 removes + -- the distinction between initial and later declarative items, + -- the distinction remains in the Examiner. (JB01-005) - if Ada_Version = Ada_83 then + if Ada_Version = Ada_83 or else SPARK_Mode then Decl := First (Decls); -- Loop through sequence of basic declarative items @@ -2139,6 +2142,11 @@ package body Ch5 is Error_Msg_Sloc := Body_Sloc; Error_Msg_N ("(Ada 83) decl cannot appear after body#", Decl); + else + pragma Assert (SPARK_Mode); + Error_Msg_Sloc := Body_Sloc; + Formal_Error_Msg_N + ("decl cannot appear after body#", Decl); end if; end if; diff --git a/gcc/ada/par-util.adb b/gcc/ada/par-util.adb index eeb93af639a..6a0e8efc6cb 100644 --- a/gcc/ada/par-util.adb +++ b/gcc/ada/par-util.adb @@ -377,16 +377,6 @@ package body Util is null; end Discard_Junk_Node; - ------------------------- - -- Formal_Error_Msg_SP -- - ------------------------- - - procedure Formal_Error_Msg_SP (Msg : String) is - begin - pragma Assert (Formal_Verification_Mode); - Error_Msg_SP ("(" & Formal_Language & ") " & Msg); - end Formal_Error_Msg_SP; - ------------ -- Ignore -- ------------ diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index da84343b53a..99f6806057d 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -1158,10 +1158,6 @@ function Par (Configuration_Pragmas : Boolean) return List_Id is -- the argument. A typical use is to skip by some junk that is not -- expected in the current context. - procedure Formal_Error_Msg_SP (Msg : String); - -- Wrapper on Errout.Error_Msg_SP which adds a prefix to Msg giving - -- the name of the formal language analyzed (spark or alfa) - procedure Ignore (T : Token_Type); -- If current token matches T, then give an error message and skip -- past it, otherwise the call has no effect at all. T may be any diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 33a40b3ba36..73239e600aa 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -2055,6 +2055,20 @@ package body Sem_Attr is end if; end if; + -- In SPARK or ALFA, attributes of private types are only allowed if + -- the full type declaration is visible + + if Formal_Verification_Mode + and then Is_Entity_Name (P) + and then Is_Type (Entity (P)) + and then Is_Private_Type (P_Type) + and then not In_Open_Scopes (Scope (P_Type)) + and then not In_Spec_Expression + then + Formal_Error_Msg_NE + ("invisible attribute of}", N, First_Subtype (P_Type)); + end if; + -- Remaining processing depends on attribute case Attr_Id is diff --git a/gcc/ada/sem_ch13.ads b/gcc/ada/sem_ch13.ads index b2c66ff2f30..32b3237ee4c 100644 --- a/gcc/ada/sem_ch13.ads +++ b/gcc/ada/sem_ch13.ads @@ -40,9 +40,9 @@ package Sem_Ch13 is (N : Node_Id; E : Entity_Id; L : List_Id); - -- This procedure is called to analyze aspect specifications for node N. E - -- is the corresponding entity declared by the declaration node N, and L is - -- the list of aspect specifications for this node. If L is No_List, the + -- This procedure is called to analyze aspect specifications for node N. + -- E is the corresponding entity declared by the declaration node N, and L + -- is the list of aspect specifications for this node. If L is No_List, the -- call is ignored. Note that we can't use a simpler interface of just -- passing the node N, since the analysis of the node may cause it to be -- rewritten to a node not permitting aspect specifications. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index fe23c3be837..74180844272 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2027,6 +2027,17 @@ package body Sem_Ch3 is D := First (L); while Present (D) loop + -- Package specification cannot contain a package declaration in + -- SPARK or ALFA + + if Formal_Verification_Mode + and then Nkind (D) = N_Package_Declaration + and then Nkind (Parent (L)) = N_Package_Specification + then + Formal_Error_Msg_N ("package specification cannot contain " + & "a package declaration", D); + end if; + -- Complete analysis of declaration Analyze (D); @@ -2347,6 +2358,21 @@ package body Sem_Ch3 is return; end if; + if Formal_Verification_Mode then + + -- Controlled type is not allowed in SPARK and ALFA + + if Is_Visibly_Controlled (T) then + Formal_Error_Msg_N ("controlled type is not allowed", N); + end if; + + -- Discriminant type is not allowed in SPARK and ALFA + + if Present (Discriminant_Specifications (N)) then + Formal_Error_Msg_N ("discriminant type is not allowed", N); + end if; + end if; + -- Some common processing for all types Set_Depends_On_Private (T, Has_Private_Component (T)); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index a49f9973917..d96499db2e2 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -3072,6 +3072,7 @@ package body Sem_Ch6 is -- User-defined operator is not allowed in SPARK or ALFA if Formal_Verification_Mode + and then Comes_From_Source (N) and then Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol then Formal_Error_Msg_N ("user-defined operator is not allowed", N); @@ -8493,6 +8494,15 @@ package body Sem_Ch6 is Check_Overriding_Indicator (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp); + -- Overloading is not allowed in SPARK or ALFA + + if Formal_Verification_Mode + and then Comes_From_Source (S) + then + Error_Msg_Sloc := Sloc (Homonym (S)); + Formal_Error_Msg_N ("overloading not allowed with entity#", S); + end if; + -- If S is a derived operation for an untagged type then by -- definition it's not a dispatching operation (even if the parent -- operation was dispatching), so we don't call diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads index 8dc87ffec0b..2fc59b43652 100644 --- a/gcc/ada/sem_ch6.ads +++ b/gcc/ada/sem_ch6.ads @@ -205,7 +205,7 @@ package Sem_Ch6 is -- Process new overloaded entity. Overloaded entities are created by -- enumeration type declarations, subprogram specifications, entry -- declarations, and (implicitly) by type derivations. Derived_Type non- - -- Empty indicates that this is subprogram derived for that type. + -- Empty indicates that this is a subprogram derived for that type. procedure Process_Formals (T : List_Id; Related_Nod : Node_Id); -- Enter the formals in the scope of the subprogram or entry, and diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d1754bdeae8..6631e1c04fd 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -9,7 +9,7 @@ -- Copyright (C) 1992-2011, 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- -- +-- terms of the GNU Genconflieral Public License as published by the Free Soft- -- -- ware Foundation; either version 3, or (at your option) any later ver- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- @@ -3644,26 +3644,6 @@ package body Sem_Util is end if; end First_Actual; - ---------------------- - -- Formal_Error_Msg -- - ---------------------- - - procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr) is - begin - pragma Assert (Formal_Verification_Mode); - Error_Msg ("(" & Formal_Language & ") " & Msg, Flag_Location); - end Formal_Error_Msg; - - ------------------------ - -- Formal_Error_Msg_N -- - ------------------------ - - procedure Formal_Error_Msg_N (Msg : String; N : Node_Id) is - begin - pragma Assert (Formal_Verification_Mode); - Error_Msg_N ("(" & Formal_Language & ") " & Msg, N); - end Formal_Error_Msg_N; - ----------------------- -- Gather_Components -- ----------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a8b58903f22..df74a1f5689 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -407,14 +407,6 @@ package Sem_Util is -- is always the expression (not the N_Parameter_Association nodes, -- even if named association is used). - procedure Formal_Error_Msg (Msg : String; Flag_Location : Source_Ptr); - -- Wrapper on Errout.Error_Msg which adds a prefix to Msg giving - -- the name of the formal language analyzed (spark or alfa) - - procedure Formal_Error_Msg_N (Msg : String; N : Node_Id); - -- Wrapper on Errout.Error_Msg_N which adds a prefix to Msg giving - -- the name of the formal language analyzed (spark or alfa) - procedure Gather_Components (Typ : Entity_Id; Comp_List : Node_Id; -- 2.30.2