diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 11 | ||||
| -rw-r--r-- | gcc/ada/err_vars.ads | 7 | ||||
| -rw-r--r-- | gcc/ada/errout.adb | 22 | ||||
| -rw-r--r-- | gcc/ada/errout.ads | 22 | ||||
| -rw-r--r-- | gcc/ada/exp_ch6.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 14 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/restrict.adb | 13 | ||||
| -rw-r--r-- | gcc/ada/restrict.ads | 4 | ||||
| -rw-r--r-- | gcc/ada/sem_aggr.adb | 26 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 20 | ||||
| -rw-r--r-- | gcc/ada/sem_ch11.adb | 6 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 110 | ||||
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/sem_ch5.adb | 33 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 35 | ||||
| -rw-r--r-- | gcc/ada/sem_ch8.adb | 35 | ||||
| -rw-r--r-- | gcc/ada/sem_ch9.adb | 26 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 66 | ||||
| -rw-r--r-- | gcc/ada/sem_util.adb | 11 |
21 files changed, 218 insertions, 282 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d9c354f..7330a20 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,13 @@ 2011-08-02 Yannick Moy <moy@adacore.com> + * sem_aggr.adb, err_vars.ads, sem_ch3.adb, sem_ch5.adb, sem_ch9.adb, + debug.adb, sem_util.adb, sem_res.adb, sem_attr.adb, gnat1drv.adb, + errout.adb, errout.ads, exp_ch6.adb, sem_ch4.adb, restrict.adb, + restrict.ads, sem_ch6.adb, sem_ch8.adb, sem_ch11.adb, + opt.ads: cleanup of SPARK mode + +2011-08-02 Yannick Moy <moy@adacore.com> + * cstand.adb (Create_Standard): sets Is_In_ALFA component of standard types. * einfo.adb, einfo.ads (Is_In_ALFA): add flag for all entities diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 27ce9b0..8f38609 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -121,7 +121,7 @@ package body Debug is -- d.A Read/write Aspect_Specifications hash table to tree -- d.B -- d.C Generate concatenation call, do not generate inline code - -- d.D Accept only the SPARK subset of Ada + -- d.D -- d.E SPARK generation mode -- d.F Why generation mode -- d.G @@ -574,13 +574,6 @@ package body Debug is -- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases -- where we would normally generate inline concatenation code. - -- d.D Issue compiler errors on Ada input outside the SPARK subset of - -- Ada. This only deals currently with the Ada code, not SPARK - -- annotations, so it may well be the case that code which passes - -- the compiler with this flag is rejected by the SPARK Examiner, - -- e.g. due to the different visibility rules of the Examiner based - -- on 'inherit' SPARK annotations. - -- d.E SPARK generation mode. Generate intermediate code for the sake of -- formal verification through SPARK and the SPARK toolset. diff --git a/gcc/ada/err_vars.ads b/gcc/ada/err_vars.ads index 2f1b048..10a0262 100644 --- a/gcc/ada/err_vars.ads +++ b/gcc/ada/err_vars.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -150,9 +150,4 @@ package Err_Vars is -- Used if current message contains a ~ insertion character to indicate -- insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen). - Error_Msg_Lang : String (1 .. 16); - Error_Msg_Langlen : Natural; - -- Used if current message contains a ~~ insertion character to indicate - -- insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen). - end Err_Vars; diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 169540e..e794057 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -2185,19 +2185,6 @@ package body Errout is Set_Casing (Desired_Case); end Set_Identifier_Casing; - ------------------------ - -- Set_Error_Msg_Lang -- - ------------------------ - - procedure Set_Error_Msg_Lang (To : String) is - begin - Error_Msg_Lang (1) := '('; - Error_Msg_Lang (2 .. To'Length + 1) := To; - Error_Msg_Lang (To'Length + 2) := ')'; - Error_Msg_Lang (To'Length + 3) := ' '; - Error_Msg_Langlen := To'Length + 3; - end Set_Error_Msg_Lang; - ----------------------- -- Set_Ignore_Errors -- ----------------------- @@ -2716,12 +2703,7 @@ package body Errout is P := P + 1; when '~' => - if P <= Text'Last and then Text (P) = '~' then - P := P + 1; - Set_Msg_Str (Error_Msg_Lang (1 .. Error_Msg_Langlen)); - else - Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen)); - end if; + Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen)); -- Upper case letter diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads index fc2cf49..2e850f8 100644 --- a/gcc/ada/errout.ads +++ b/gcc/ada/errout.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -346,16 +346,6 @@ package Errout is -- inserted to replace the ~ character. The string is inserted in the -- literal form it appears, without any action on special characters. - -- Insertion character ~~ (Two tildes: insert language string) - -- Indicates that Error_Msg_Lang (1 .. Error_Msg_Langlen) is to be - -- inserted to replace the ~~ character. Typically the language string - -- will be inserted in parentheses as a prefix of the error message, as - -- in "(spark) error msg". The string is inserted in the literal form - -- it appears, without any action on special characters. Error_Msg_Lang - -- and Error_Msg_Langlen are expected to be set only once before - -- parsing starts, so that the caller to an error procedure does not - -- need to set them repeatedly. - ---------------------------------------- -- Specialization of Messages for VMS -- ---------------------------------------- @@ -469,11 +459,6 @@ package Errout is -- Used if current message contains a ~ insertion character to indicate -- insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen). - Error_Msg_Lang : String renames Err_Vars.Error_Msg_Lang; - Error_Msg_Langlen : Natural renames Err_Vars.Error_Msg_Langlen; - -- Used if current message contains a ~~ insertion character to indicate - -- insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen). - ----------------------------------------------------- -- Format of Messages and Manual Quotation Control -- ----------------------------------------------------- @@ -765,11 +750,6 @@ package Errout is -- Remove warnings on all elements of a list (Calls Remove_Warning_Messages -- on each element of the list, see above). - procedure Set_Error_Msg_Lang (To : String); - -- Set Error_Msg_Lang/Error_Msg_Langlen used for insertion character ~~. - -- The argument is just the language name, e.g. "spark". The stored string - -- is of the form "(langname) ". - procedure Set_Ignore_Errors (To : Boolean); -- Following a call to this procedure with To=True, all error calls are -- ignored. A call with To=False restores the default treatment in which diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index 8a842fb..bf7b44e 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -5449,26 +5449,26 @@ package body Exp_Ch6 is Prot_Id : Entity_Id; begin - -- In SPARK or ALFA, subprogram declarations are only allowed in - -- package specifications. + -- In SPARK, subprogram declarations are only allowed in package + -- specifications. if Nkind (Parent (N)) /= N_Package_Specification then if Nkind (Parent (N)) = N_Compilation_Unit then - Check_Formal_Restriction + Check_SPARK_Restriction ("subprogram declaration is not a library item", N); elsif Present (Next (N)) and then Nkind (Next (N)) = N_Pragma and then Get_Pragma_Id (Pragma_Name (Next (N))) = Pragma_Import then - -- In SPARK or ALFA, subprogram declarations are also permitted in + -- In SPARK, subprogram declarations are also permitted in -- declarative parts when immediately followed by a corresponding -- pragma Import. We only check here that there is some pragma -- Import. null; else - Check_Formal_Restriction + Check_SPARK_Restriction ("subprogram declaration is not allowed here", N); end if; end if; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 06ab52c..4336277 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -392,10 +392,6 @@ procedure Gnat1drv is -- Set switches for formal verification modes - if Debug_Flag_Dot_DD then - SPARK_Mode := True; - end if; - if Debug_Flag_Dot_EE then ALFA_Through_SPARK_Mode := True; end if; @@ -405,14 +401,6 @@ procedure Gnat1drv is end if; ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode; - - if ALFA_Mode then - Set_Error_Msg_Lang ("alfa"); - Formal_Verification_Mode := True; - elsif SPARK_Mode then - Set_Error_Msg_Lang ("spark"); - Formal_Verification_Mode := True; - end if; end Adjust_Global_Switches; -------------------- diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 732fc4d..e611c04 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -1870,9 +1870,6 @@ package Opt is -- These modes are currently defined through debug flags - Formal_Verification_Mode : Boolean := False; - -- Set True if ALFA_Mode or SPARK_Mode - ALFA_Mode : Boolean := False; -- Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index 883128a..c68475b 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -109,7 +109,7 @@ package body Restrict is -- Check_Formal_Restriction -- ------------------------------ - procedure Check_Formal_Restriction + procedure Check_SPARK_Restriction (Msg : String; N : Node_Id; Force : Boolean := False) @@ -129,11 +129,9 @@ package body Restrict is if Msg_Issued then Error_Msg_F ("\\| " & Msg, N); - elsif SPARK_Mode then - Error_Msg_F ("|~~" & Msg, N); end if; end if; - end Check_Formal_Restriction; + end Check_SPARK_Restriction; procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is Msg_Issued : Boolean; @@ -154,9 +152,6 @@ package body Restrict is if Msg_Issued then Error_Msg_F ("\\| " & Msg1, N); Error_Msg_F (Msg2, N); - elsif SPARK_Mode then - Error_Msg_F ("|~~" & Msg1, N); - Error_Msg_F (Msg2, N); end if; end if; end Check_Formal_Restriction; @@ -380,7 +375,7 @@ package body Restrict is -- No_Dispatch restriction is not set. if R = No_Dispatch then - Check_Formal_Restriction ("class-wide is not allowed", N); + Check_SPARK_Restriction ("class-wide is not allowed", N); end if; if UI_Is_In_Int_Range (V) then diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads index f0dcb31..46626c9 100644 --- a/gcc/ada/restrict.ads +++ b/gcc/ada/restrict.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -228,7 +228,7 @@ package Restrict is -- an elaboration routine. If elaboration code is not allowed, an error -- message is posted on the node given as argument. - procedure Check_Formal_Restriction + procedure Check_SPARK_Restriction (Msg : String; N : Node_Id; Force : Boolean := False); diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 89db3d0..e704586 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -809,7 +809,7 @@ package body Sem_Aggr is begin if Level = 0 then if Nkind (Parent (Expr)) /= N_Qualified_Expression then - Check_Formal_Restriction ("aggregate should be qualified", Expr); + Check_SPARK_Restriction ("aggregate should be qualified", Expr); end if; else @@ -978,7 +978,7 @@ package body Sem_Aggr is return; end if; - -- An unqualified aggregate is restricted in SPARK or ALFA to: + -- An unqualified aggregate is restricted in SPARK to: -- An aggregate item inside an aggregate for a multi-dimensional array @@ -997,12 +997,12 @@ package body Sem_Aggr is and then not Is_Constrained (Etype (Name (Parent (N)))) then if not Is_Others_Aggregate (N) then - Check_Formal_Restriction + Check_SPARK_Restriction ("array aggregate should have only OTHERS", N); end if; elsif Is_Top_Level_Aggregate (N) then - Check_Formal_Restriction ("aggregate should be qualified", N); + Check_SPARK_Restriction ("aggregate should be qualified", N); -- The legality of this unqualified aggregate is checked by calling -- Check_Qualified_Aggregate from one of its enclosing aggregate, @@ -1873,13 +1873,13 @@ package body Sem_Aggr is Set_Do_Range_Check (Choice, False); - -- In SPARK or ALFA, the choice must be static + -- In SPARK, the choice must be static if not (Is_Static_Expression (Choice) or else (Nkind (Choice) = N_Range and then Is_Static_Range (Choice))) then - Check_Formal_Restriction + Check_SPARK_Restriction ("choice should be static", Choice); end if; end if; @@ -2523,12 +2523,12 @@ package body Sem_Aggr is Analyze (A); Check_Parameterless_Call (A); - -- In SPARK or ALFA, the ancestor part cannot be a type mark + -- In SPARK, the ancestor part cannot be a type mark if Is_Entity_Name (A) and then Is_Type (Entity (A)) then - Check_Formal_Restriction ("ancestor part cannot be a type mark", A); + Check_SPARK_Restriction ("ancestor part cannot be a type mark", A); end if; if not Is_Tagged_Type (Typ) then @@ -3212,7 +3212,7 @@ package body Sem_Aggr is -- Start of processing for Resolve_Record_Aggregate begin - -- A record aggregate is restricted in SPARK or ALFA: + -- A record aggregate is restricted in SPARK: -- Each named association can have only a single choice. -- OTHERS cannot be used. -- Positional and named associations cannot be mixed. @@ -3222,7 +3222,7 @@ package body Sem_Aggr is then if Present (Expressions (N)) then - Check_Formal_Restriction + Check_SPARK_Restriction ("named association cannot follow positional one", First (Choices (First (Component_Associations (N))))); end if; @@ -3234,13 +3234,13 @@ package body Sem_Aggr is Assoc := First (Component_Associations (N)); while Present (Assoc) loop if List_Length (Choices (Assoc)) > 1 then - Check_Formal_Restriction + Check_SPARK_Restriction ("component association in record aggregate must " & "contain a single choice", Assoc); end if; if Nkind (First (Choices (Assoc))) = N_Others_Choice then - Check_Formal_Restriction + Check_SPARK_Restriction ("record aggregate cannot contain OTHERS", Assoc); end if; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 4ff4ff4..01a9bef 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -1296,7 +1296,7 @@ package body Sem_Attr is procedure Check_Formal_Restriction_On_Attribute is begin Error_Msg_Name_1 := Aname; - Check_Formal_Restriction ("attribute % is not allowed", P); + Check_SPARK_Restriction ("attribute % is not allowed", P); end Check_Formal_Restriction_On_Attribute; ------------------------ @@ -2068,8 +2068,8 @@ 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. + -- In SPARK, attributes of private types are only allowed if the full + -- type declaration is visible. if Is_Entity_Name (P) and then Present (Entity (P)) -- needed in some cases @@ -2079,7 +2079,7 @@ package body Sem_Attr is and then not In_Spec_Expression then Error_Msg_Node_1 := First_Subtype (P_Type); - Check_Formal_Restriction ("invisible attribute of}", N); + Check_SPARK_Restriction ("invisible attribute of}", N); end if; -- Remaining processing depends on attribute @@ -2460,7 +2460,7 @@ package body Sem_Attr is if Nkind (Parent (N)) /= N_Attribute_Reference then Error_Msg_Name_1 := Aname; - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is only allowed as prefix of another attribute", P); end if; @@ -3877,7 +3877,7 @@ package body Sem_Attr is if Is_Boolean_Type (P_Type) then Error_Msg_Name_1 := Aname; Error_Msg_Name_2 := Chars (P_Type); - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is not allowed for type%", P); end if; @@ -3903,7 +3903,7 @@ package body Sem_Attr is if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then Error_Msg_Name_1 := Aname; Error_Msg_Name_2 := Chars (P_Type); - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is not allowed for type%", P); end if; @@ -4461,7 +4461,7 @@ package body Sem_Attr is if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then Error_Msg_Name_1 := Aname; Error_Msg_Name_2 := Chars (P_Type); - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is not allowed for type%", P); end if; @@ -4786,7 +4786,7 @@ package body Sem_Attr is if Is_Boolean_Type (P_Type) then Error_Msg_Name_1 := Aname; Error_Msg_Name_2 := Chars (P_Type); - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is not allowed for type%", P); end if; diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 26ac6d0..357b3f1 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -443,7 +443,7 @@ package body Sem_Ch11 is P : Node_Id; begin - Check_Formal_Restriction ("raise statement is not allowed", N); + Check_SPARK_Restriction ("raise statement is not allowed", N); Check_Unreachable_Code (N); -- Check exception restrictions on the original source @@ -610,7 +610,7 @@ package body Sem_Ch11 is -- Start of processing for Analyze_Raise_xxx_Error begin - Check_Formal_Restriction ("raise statement is not allowed", N); + Check_SPARK_Restriction ("raise statement is not allowed", N); if No (Etype (N)) then Set_Etype (N, Standard_Void_Type); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index afa0f85..55d4c3b 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -714,7 +714,7 @@ package body Sem_Ch3 is Enclosing_Prot_Type : Entity_Id := Empty; begin - Check_Formal_Restriction ("access type is not allowed", N); + Check_SPARK_Restriction ("access type is not allowed", N); if Is_Entry (Current_Scope) and then Is_Task_Type (Etype (Scope (Current_Scope))) @@ -1028,7 +1028,7 @@ package body Sem_Ch3 is -- Start of processing for Access_Subprogram_Declaration begin - Check_Formal_Restriction ("access type is not allowed", T_Def); + Check_SPARK_Restriction ("access type is not allowed", T_Def); -- Associate the Itype node with the inner full-type declaration or -- subprogram spec or entry body. This is required to handle nested @@ -1282,7 +1282,7 @@ package body Sem_Ch3 is S : constant Node_Id := Subtype_Indication (Def); P : constant Node_Id := Parent (Def); begin - Check_Formal_Restriction ("access type is not allowed", Def); + Check_SPARK_Restriction ("access type is not allowed", Def); -- Check for permissible use of incomplete type @@ -1786,7 +1786,7 @@ package body Sem_Ch3 is (Subtype_Indication (Component_Definition (N)), N); if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then - Check_Formal_Restriction ("subtype mark required", Typ); + Check_SPARK_Restriction ("subtype mark required", Typ); end if; -- Ada 2005 (AI-230): Access Definition case @@ -1839,7 +1839,7 @@ package body Sem_Ch3 is -- package Sem). if Present (E) then - Check_Formal_Restriction ("default expression is not allowed", E); + Check_SPARK_Restriction ("default expression is not allowed", E); Preanalyze_Spec_Expression (E, T); Check_Initialization (T, E); @@ -2046,12 +2046,12 @@ package body Sem_Ch3 is while Present (D) loop -- Package specification cannot contain a package declaration in - -- SPARK or ALFA. + -- SPARK. if Nkind (D) = N_Package_Declaration and then Nkind (Parent (L)) = N_Package_Specification then - Check_Formal_Restriction ("package specification cannot contain " + Check_SPARK_Restriction ("package specification cannot contain " & "a package declaration", D); end if; @@ -2273,11 +2273,11 @@ package body Sem_Ch3 is null; -- For record types, discriminants are allowed, unless we are in - -- SPARK or ALFA. + -- SPARK. when N_Record_Definition => if Present (Discriminant_Specifications (N)) then - Check_Formal_Restriction + Check_SPARK_Restriction ("discriminant type is not allowed", Defining_Identifier (First (Discriminant_Specifications (N)))); @@ -2383,10 +2383,10 @@ package body Sem_Ch3 is return; end if; - -- Controlled type is not allowed in SPARK and ALFA + -- Controlled type is not allowed in SPARK if Is_Visibly_Controlled (T) then - Check_Formal_Restriction ("controlled type is not allowed", N); + Check_SPARK_Restriction ("controlled type is not allowed", N); end if; -- Some common processing for all types @@ -2495,7 +2495,7 @@ package body Sem_Ch3 is T : Entity_Id; begin - Check_Formal_Restriction ("incomplete type is not allowed", N); + Check_SPARK_Restriction ("incomplete type is not allowed", N); Generate_Definition (Defining_Identifier (N)); @@ -3040,29 +3040,29 @@ package body Sem_Ch3 is -- is considered, so that the Object_Definition node is still the same -- as in source code. - -- In SPARK or ALFA, the nominal subtype shall be given by a subtype - -- mark and shall not be unconstrained. (The only exception to this - -- is the admission of declarations of constants of type String.) + -- In SPARK, the nominal subtype shall be given by a subtype mark and + -- shall not be unconstrained. (The only exception to this is the + -- admission of declarations of constants of type String.) if not Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name) then - Check_Formal_Restriction + Check_SPARK_Restriction ("subtype mark required", Object_Definition (N)); elsif Is_Array_Type (T) and then not Is_Constrained (T) and then T /= Standard_String then - Check_Formal_Restriction + Check_SPARK_Restriction ("subtype mark of constrained type expected", Object_Definition (N)); end if; - -- There are no aliased objects in SPARK or ALFA + -- There are no aliased objects in SPARK if Aliased_Present (N) then - Check_Formal_Restriction ("aliased object is not allowed", N); + Check_SPARK_Restriction ("aliased object is not allowed", N); end if; -- Process initialization expression if present and not in error @@ -3186,11 +3186,10 @@ package body Sem_Ch3 is -- Only call test if needed - and then (Formal_Verification_Mode - or else Restriction_Check_Required (SPARK)) + and then Restriction_Check_Required (SPARK) and then not Is_SPARK_Initialization_Expr (E) then - Check_Formal_Restriction + Check_SPARK_Restriction ("initialization expression is not appropriate", E); end if; end if; @@ -4029,12 +4028,12 @@ package body Sem_Ch3 is Set_Has_Delayed_Freeze (Id); end if; - -- Subtype of Boolean cannot have a constraint in SPARK or ALFA + -- Subtype of Boolean cannot have a constraint in SPARK if Is_Boolean_Type (T) and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication then - Check_Formal_Restriction + Check_SPARK_Restriction ("subtype of Boolean cannot have constraint", N); end if; @@ -4050,13 +4049,13 @@ package body Sem_Ch3 is One_Cstr := First (Constraints (Cstr)); while Present (One_Cstr) loop - -- Index or discriminant constraint in SPARK or ALFA must be - -- a subtype mark. + -- Index or discriminant constraint in SPARK must be a + -- subtype mark. if not Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name) then - Check_Formal_Restriction + Check_SPARK_Restriction ("subtype mark required", One_Cstr); -- String subtype must have a lower bound of 1 in SPARK. @@ -4070,7 +4069,7 @@ package body Sem_Ch3 is if Is_OK_Static_Expression (Low) and then Expr_Value (Low) /= 1 then - Check_Formal_Restriction + Check_SPARK_Restriction ("String subtype must have lower bound of 1", N); end if; end if; @@ -4089,12 +4088,12 @@ package body Sem_Ch3 is Set_Etype (Id, Base_Type (T)); -- Subtype of unconstrained array without constraint is not allowed - -- in SPARK or ALFA. + -- in SPARK. if Is_Array_Type (T) and then not Is_Constrained (T) then - Check_Formal_Restriction + Check_SPARK_Restriction ("subtype of unconstrained array must have constraint", N); end if; @@ -4617,7 +4616,7 @@ package body Sem_Ch3 is Analyze (Index); if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then - Check_Formal_Restriction ("subtype mark required", Index); + Check_SPARK_Restriction ("subtype mark required", Index); end if; -- Add a subtype declaration for each index of private array type @@ -4692,7 +4691,7 @@ package body Sem_Ch3 is Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C'); if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then - Check_Formal_Restriction ("subtype mark required", Component_Typ); + Check_SPARK_Restriction ("subtype mark required", Component_Typ); end if; -- Ada 2005 (AI-230): Access Definition case @@ -4801,7 +4800,7 @@ package body Sem_Ch3 is Set_Packed_Array_Type (T, Empty); if Aliased_Present (Component_Definition (Def)) then - Check_Formal_Restriction + Check_SPARK_Restriction ("aliased is not allowed", Component_Definition (Def)); Set_Has_Aliased_Components (Etype (T)); end if; @@ -11312,7 +11311,7 @@ package body Sem_Ch3 is else pragma Assert (Nkind (C) = N_Digits_Constraint); - Check_Formal_Restriction ("digits constraint is not allowed", S); + Check_SPARK_Restriction ("digits constraint is not allowed", S); Digits_Expr := Digits_Expression (C); Analyze_And_Resolve (Digits_Expr, Any_Integer); @@ -11551,7 +11550,7 @@ package body Sem_Ch3 is if Nkind (C) = N_Digits_Constraint then - Check_Formal_Restriction ("digits constraint is not allowed", S); + Check_SPARK_Restriction ("digits constraint is not allowed", S); Check_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -11783,7 +11782,7 @@ package body Sem_Ch3 is if Nkind (C) = N_Delta_Constraint then - Check_Formal_Restriction ("delta constraint is not allowed", S); + Check_SPARK_Restriction ("delta constraint is not allowed", S); Check_Restriction (No_Obsolescent_Features, C); if Warn_On_Obsolescent_Feature then @@ -12440,7 +12439,7 @@ package body Sem_Ch3 is Bound_Val : Ureal; begin - Check_Formal_Restriction + Check_SPARK_Restriction ("decimal fixed point type is not allowed", Def); Check_Restriction (No_Fixed_Point, Def); @@ -13946,7 +13945,7 @@ package body Sem_Ch3 is -- parent is also an interface. if Interface_Present (Def) then - Check_Formal_Restriction ("interface is not allowed", Def); + Check_SPARK_Restriction ("interface is not allowed", Def); if not Is_Interface (Parent_Type) then Diagnose_Interface (Indic, Parent_Type); @@ -14188,8 +14187,7 @@ package body Sem_Ch3 is end if; -- Only composite types other than array types are allowed to have - -- discriminants. In SPARK and in ALFA, no types are allowed to have - -- discriminants. + -- discriminants. In SPARK, no types are allowed to have discriminants. if Present (Discriminant_Specifications (N)) then if (Is_Elementary_Type (Parent_Type) @@ -14201,7 +14199,7 @@ package body Sem_Ch3 is Defining_Identifier (First (Discriminant_Specifications (N)))); Set_Has_Discriminants (T, False); else - Check_Formal_Restriction ("discriminant type is not allowed", N); + Check_SPARK_Restriction ("discriminant type is not allowed", N); end if; end if; @@ -14388,11 +14386,11 @@ package body Sem_Ch3 is end if; end if; - -- In SPARK or ALFA, there are no derived type definitions other than - -- type extensions of tagged record types. + -- In SPARK, there are no derived type definitions other than type + -- extensions of tagged record types. if No (Extension) then - Check_Formal_Restriction ("derived type is not allowed", N); + Check_SPARK_Restriction ("derived type is not allowed", N); end if; end Derived_Type_Declaration; @@ -16543,7 +16541,7 @@ package body Sem_Ch3 is -- Non-binary case elsif M_Val < 2 ** Bits then - Check_Formal_Restriction ("modulus should be a power of 2", T); + Check_SPARK_Restriction ("modulus should be a power of 2", T); Set_Non_Binary_Modulus (T); if Bits > System_Max_Nonbinary_Modulus_Power then @@ -17402,7 +17400,7 @@ package body Sem_Ch3 is if Priv_Parent /= Full_Parent then Error_Msg_Name_1 := Chars (Priv_Parent); - Check_Formal_Restriction ("% expected", Full_Indic); + Check_SPARK_Restriction ("% expected", Full_Indic); end if; -- Check the rules of 7.3(10): if the private extension inherits @@ -17967,7 +17965,7 @@ package body Sem_Ch3 is if not In_Iter_Schm and then not Is_Static_Range (R) then - Check_Formal_Restriction ("range should be static", R); + Check_SPARK_Restriction ("range should be static", R); end if; Lo := Low_Bound (R); @@ -18986,11 +18984,11 @@ package body Sem_Ch3 is or else not Interface_Present (Def) then if Limited_Present (Def) then - Check_Formal_Restriction ("limited is not allowed", N); + Check_SPARK_Restriction ("limited is not allowed", N); end if; if Abstract_Present (Def) then - Check_Formal_Restriction ("abstract is not allowed", N); + Check_SPARK_Restriction ("abstract is not allowed", N); end if; -- The flag Is_Tagged_Type might have already been set by @@ -19012,7 +19010,7 @@ package body Sem_Ch3 is or else Abstract_Present (Def)); else - Check_Formal_Restriction ("interface is not allowed", N); + Check_SPARK_Restriction ("interface is not allowed", N); Is_Tagged := True; Analyze_Interface_Declaration (T, Def); @@ -19152,8 +19150,8 @@ package body Sem_Ch3 is T := Prev_T; end if; - -- In SPARK or ALFA, tagged types and type extensions may only be - -- declared in the specification of library unit packages. + -- In SPARK, tagged types and type extensions may only be declared in + -- the specification of library unit packages. if Present (Def) and then Is_Tagged_Type (T) then declare @@ -19174,13 +19172,13 @@ package body Sem_Ch3 is if Nkind (Ctxt) = N_Package_Body and then Nkind (Parent (Ctxt)) = N_Compilation_Unit then - Check_Formal_Restriction + Check_SPARK_Restriction ("type should be defined in package specification", Typ); elsif Nkind (Ctxt) /= N_Package_Specification or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit then - Check_Formal_Restriction + Check_SPARK_Restriction ("type should be defined in library unit package", Typ); end if; end; @@ -19209,14 +19207,14 @@ package body Sem_Ch3 is or else Null_Present (Component_List (Def)) then if not Is_Tagged_Type (T) then - Check_Formal_Restriction ("non-tagged record cannot be null", Def); + Check_SPARK_Restriction ("non-tagged record cannot be null", Def); end if; else Analyze_Declarations (Component_Items (Component_List (Def))); if Present (Variant_Part (Component_List (Def))) then - Check_Formal_Restriction ("variant part is not allowed", Def); + Check_SPARK_Restriction ("variant part is not allowed", Def); Analyze (Variant_Part (Component_List (Def))); end if; end if; diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 5a5169b..ae169c2 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -369,7 +369,7 @@ package body Sem_Ch4 is C : Node_Id; begin - Check_Formal_Restriction ("allocator is not allowed", N); + Check_SPARK_Restriction ("allocator is not allowed", N); -- Deal with allocator restrictions @@ -818,7 +818,7 @@ package body Sem_Ch4 is case Nkind (Actual) is when N_Parameter_Association => if Named_Seen then - Check_Formal_Restriction + Check_SPARK_Restriction ("named association cannot follow positional one", Actual); exit; @@ -1506,7 +1506,7 @@ package body Sem_Ch4 is return; end if; - Check_Formal_Restriction ("conditional expression is not allowed", N); + Check_SPARK_Restriction ("conditional expression is not allowed", N); Else_Expr := Next (Then_Expr); @@ -1706,7 +1706,7 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Explicit_Dereference begin - Check_Formal_Restriction ("explicit dereference is not allowed", N); + Check_SPARK_Restriction ("explicit dereference is not allowed", N); Analyze (P); Set_Etype (N, Any_Type); @@ -2588,7 +2588,7 @@ package body Sem_Ch4 is procedure Analyze_Null (N : Node_Id) is begin - Check_Formal_Restriction ("null is not allowed", N); + Check_SPARK_Restriction ("null is not allowed", N); Set_Etype (N, Any_Access); end Analyze_Null; @@ -3274,7 +3274,7 @@ package body Sem_Ch4 is Iterator : Node_Id; begin - Check_Formal_Restriction ("quantified expression is not allowed", N); + Check_SPARK_Restriction ("quantified expression is not allowed", N); Set_Etype (Ent, Standard_Void_Type); Set_Parent (Ent, N); @@ -4302,7 +4302,7 @@ package body Sem_Ch4 is -- Start of processing for Analyze_Slice begin - Check_Formal_Restriction ("slice is not allowed", N); + Check_SPARK_Restriction ("slice is not allowed", N); Analyze (P); Analyze (D); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 177987c..bfd41d0 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -819,7 +819,7 @@ package body Sem_Ch5 is -- block statements generated by the expander is fine. if Nkind (Original_Node (N)) = N_Block_Statement then - Check_Formal_Restriction ("block statement is not allowed", N); + Check_SPARK_Restriction ("block statement is not allowed", N); end if; -- If no handled statement sequence is present, things are really messed @@ -1108,12 +1108,12 @@ 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 - -- in SPARK or ALFA. + -- in SPARK. if Others_Present and then List_Length (Alternatives (N)) = 1 then - Check_Formal_Restriction + Check_SPARK_Restriction ("OTHERS as unique case alternative is not allowed", N); end if; @@ -1194,7 +1194,7 @@ package body Sem_Ch5 is else if Has_Loop_In_Inner_Open_Scopes (U_Name) then - Check_Formal_Restriction + Check_SPARK_Restriction ("exit label must name the closest enclosing loop", N); end if; @@ -1240,34 +1240,34 @@ package body Sem_Ch5 is if Present (Cond) then if Nkind (Parent (N)) /= N_Loop_Statement then - Check_Formal_Restriction + Check_SPARK_Restriction ("exit with when clause must be directly in loop", N); end if; else if Nkind (Parent (N)) /= N_If_Statement then if Nkind (Parent (N)) = N_Elsif_Part then - Check_Formal_Restriction + Check_SPARK_Restriction ("exit must be in IF without ELSIF", N); else - Check_Formal_Restriction ("exit must be directly in IF", N); + Check_SPARK_Restriction ("exit must be directly in IF", N); end if; elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then - Check_Formal_Restriction + Check_SPARK_Restriction ("exit must be in IF directly in loop", N); -- First test the presence of ELSE, so that an exit in an ELSE -- leads to an error mentioning the ELSE. elsif Present (Else_Statements (Parent (N))) then - Check_Formal_Restriction ("exit must be in IF without ELSE", N); + Check_SPARK_Restriction ("exit must be in IF without ELSE", N); -- An exit in an ELSIF does not reach here, as it would have been -- detected in the case (Nkind (Parent (N)) /= N_If_Statement). elsif Present (Elsif_Parts (Parent (N))) then - Check_Formal_Restriction ("exit must be in IF without ELSIF", N); + Check_SPARK_Restriction ("exit must be in IF without ELSIF", N); end if; end if; @@ -1295,7 +1295,7 @@ package body Sem_Ch5 is Label_Ent : Entity_Id; begin - Check_Formal_Restriction ("goto statement is not allowed", N); + Check_SPARK_Restriction ("goto statement is not allowed", N); -- Actual semantic checks @@ -1963,10 +1963,10 @@ package body Sem_Ch5 is end; -- Loop parameter specification must include subtype mark in - -- SPARK or ALFA. + -- SPARK. if Nkind (DS) = N_Range then - Check_Formal_Restriction + Check_SPARK_Restriction ("loop parameter specification must include subtype mark", N); end if; @@ -2546,8 +2546,7 @@ package body Sem_Ch5 is -- we are in formal mode where goto statements are not allowed. if Nkind (Nxt) = N_Label - and then not (Formal_Verification_Mode - or else Restriction_Check_Required (SPARK)) + and then not Restriction_Check_Required (SPARK) then return; @@ -2605,7 +2604,7 @@ package body Sem_Ch5 is -- Now issue the warning (or error in formal mode) if SPARK_Mode or else Restriction_Check_Required (SPARK) then - Check_Formal_Restriction + Check_SPARK_Restriction ("unreachable code is not allowed", Error_Node); else Error_Msg ("?unreachable code!", Sloc (Error_Node)); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 170533d..3c8f02e 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -227,7 +227,7 @@ package body Sem_Ch6 is Scop : constant Entity_Id := Current_Scope; begin - Check_Formal_Restriction ("abstract subprogram is not allowed", N); + Check_SPARK_Restriction ("abstract subprogram is not allowed", N); Generate_Definition (Designator); Set_Is_Abstract_Subprogram (Designator); @@ -631,20 +631,20 @@ package body Sem_Ch6 is Analyze_And_Resolve (Expr, R_Type); Check_Limited_Return (Expr); - -- The only RETURN allowed in SPARK or ALFA is as the last statement - -- of the function. + -- The only RETURN allowed in SPARK is as the last statement of the + -- function. if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements and then (Nkind (Parent (Parent (N))) /= N_Subprogram_Body or else Present (Next (N))) then - Check_Formal_Restriction + Check_SPARK_Restriction ("RETURN should be the last statement in function", N); end if; else - Check_Formal_Restriction ("extended RETURN is not allowed", N); + Check_SPARK_Restriction ("extended RETURN is not allowed", N); -- Analyze parts specific to extended_return_statement: @@ -1425,7 +1425,7 @@ package body Sem_Ch6 is if Result_Definition (N) /= Error then if Nkind (Result_Definition (N)) = N_Access_Definition then - Check_Formal_Restriction + Check_SPARK_Restriction ("access result is not allowed", Result_Definition (N)); -- Ada 2005 (AI-254): Handle anonymous access to subprograms @@ -1463,12 +1463,12 @@ package body Sem_Ch6 is Set_Is_In_ALFA (Designator, False); end if; - -- Unconstrained array as result is not allowed in SPARK or ALFA + -- Unconstrained array as result is not allowed in SPARK if Is_Array_Type (Typ) and then not Is_Constrained (Typ) then - Check_Formal_Restriction + Check_SPARK_Restriction ("returning an unconstrained array is not allowed", Result_Definition (N)); end if; @@ -1910,7 +1910,7 @@ package body Sem_Ch6 is and then not Nkind_In (Stat, N_Simple_Return_Statement, N_Extended_Return_Statement) then - Check_Formal_Restriction + Check_SPARK_Restriction ("last statement in function should be RETURN", Stat); end if; end; @@ -1928,7 +1928,7 @@ package body Sem_Ch6 is -- borrow the Check_Returns procedure here ??? if Return_Present (Id) then - Check_Formal_Restriction + Check_SPARK_Restriction ("procedure should not have RETURN", N); end if; end if; @@ -2866,12 +2866,12 @@ package body Sem_Ch6 is -- Start of processing for Analyze_Subprogram_Declaration begin - -- Null procedures are not allowed in SPARK or ALFA + -- Null procedures are not allowed in SPARK if Nkind (Specification (N)) = N_Procedure_Specification and then Null_Present (Specification (N)) then - Check_Formal_Restriction ("null procedure is not allowed", N); + Check_SPARK_Restriction ("null procedure is not allowed", N); end if; -- For a null procedure, capture the profile before analysis, for @@ -3118,13 +3118,12 @@ package body Sem_Ch6 is Set_Is_In_ALFA (Designator); - -- User-defined operator is not allowed in SPARK or ALFA, except as - -- a renaming. + -- User-defined operator is not allowed in SPARK, except as a renaming if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration then - Check_Formal_Restriction ("user-defined operator is not allowed", N); + Check_SPARK_Restriction ("user-defined operator is not allowed", N); end if; -- Proceed with analysis @@ -8572,10 +8571,10 @@ package body Sem_Ch6 is Check_Overriding_Indicator (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp); - -- Overloading is not allowed in SPARK or ALFA + -- Overloading is not allowed in SPARK Error_Msg_Sloc := Sloc (Homonym (S)); - Check_Formal_Restriction ("overloading not allowed with entity#", S); + Check_SPARK_Restriction ("overloading not allowed with entity#", S); -- If S is a derived operation for an untagged type then by -- definition it's not a dispatching operation (even if the parent @@ -8853,7 +8852,7 @@ package body Sem_Ch6 is Default := Expression (Param_Spec); if Present (Default) then - Check_Formal_Restriction + Check_SPARK_Restriction ("default expression is not allowed", Default); if Out_Present (Param_Spec) then diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 4a1eedd..20b64a7 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -529,7 +529,7 @@ package body Sem_Ch8 is Nam : constant Node_Id := Name (N); begin - Check_Formal_Restriction ("exception renaming is not allowed", N); + Check_SPARK_Restriction ("exception renaming is not allowed", N); Enter_Name (Id); Analyze (Nam); @@ -626,7 +626,7 @@ package body Sem_Ch8 is return; end if; - Check_Formal_Restriction ("generic renaming is not allowed", N); + Check_SPARK_Restriction ("generic renaming is not allowed", N); Generate_Definition (New_P); @@ -718,7 +718,7 @@ package body Sem_Ch8 is return; end if; - Check_Formal_Restriction ("object renaming is not allowed", N); + Check_SPARK_Restriction ("object renaming is not allowed", N); Set_Is_Pure (Id, Is_Pure (Current_Scope)); Enter_Name (Id); @@ -1582,6 +1582,11 @@ package body Sem_Ch8 is procedure Analyze_Subprogram_Renaming (N : Node_Id) is Formal_Spec : constant Node_Id := Corresponding_Formal_Spec (N); Is_Actual : constant Boolean := Present (Formal_Spec); + + CW_Actual : Boolean := False; + -- True if the renaming is for a defaulted formal subprogram when the + -- actual for a related formal type is class-wide. For AI05-0071. + Inst_Node : Node_Id := Empty; Nam : constant Node_Id := Name (N); New_S : Entity_Id; @@ -1734,6 +1739,7 @@ package body Sem_Ch8 is end loop; if Present (Formal_Type) then + CW_Actual := True; -- Create declaration and body for class-wide operation @@ -2430,14 +2436,11 @@ package body Sem_Ch8 is elsif Ekind (Old_S) /= E_Operator then - -- If this is a default subprogram, it may be for a class-wide - -- actual, in which case there is no check for mode conformance, - -- given that the signatures do not match (the source mentions T, - -- but the actual mentions T'Class). + -- If this a defaulted subprogram for a class-wide actual there is + -- no check for mode conformance, given that the signatures don't + -- match (the source mentions T but the actual mentions T'class). - if Is_Actual - and then From_Default (N) - then + if CW_Actual then null; else @@ -2745,7 +2748,7 @@ package body Sem_Ch8 is -- Start of processing for Analyze_Use_Package begin - Check_Formal_Restriction ("use clause is not allowed", N); + Check_SPARK_Restriction ("use clause is not allowed", N); Set_Hidden_By_Use_Clause (N, No_Elist); @@ -5551,12 +5554,12 @@ package body Sem_Ch8 is if SPARK_Mode or else Restriction_Check_Required (SPARK) then if Nkind (Selector_Name (N)) = N_Character_Literal then - Check_Formal_Restriction + Check_SPARK_Restriction ("character literal cannot be prefixed", N); elsif Nkind (Selector_Name (N)) = N_Operator_Symbol and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration then - Check_Formal_Restriction ("operator symbol cannot be prefixed", N); + Check_SPARK_Restriction ("operator symbol cannot be prefixed", N); end if; end if; @@ -5888,10 +5891,10 @@ package body Sem_Ch8 is and then (SPARK_Mode or else Restriction_Check_Required (SPARK)) then if Is_Subprogram (P_Name) then - Check_Formal_Restriction + Check_SPARK_Restriction ("prefix of expanded name cannot be a subprogram", P); elsif Ekind (P_Name) = E_Loop then - Check_Formal_Restriction + Check_SPARK_Restriction ("prefix of expanded name cannot be a loop statement", P); end if; end if; @@ -6044,7 +6047,7 @@ package body Sem_Ch8 is elsif Attribute_Name (N) = Name_Base then Error_Msg_Name_1 := Name_Base; - Check_Formal_Restriction + Check_SPARK_Restriction ("attribute% is only allowed as prefix of another attribute", N); if Ada_Version = Ada_83 and then Comes_From_Source (N) then diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 09214b8..399d36e 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2010, Free Software Foundation, Inc. -- +-- 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- -- @@ -101,7 +101,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("abort statement is not allowed", N); + Check_SPARK_Restriction ("abort statement is not allowed", N); T_Name := First (Names (N)); while Present (T_Name) loop @@ -172,7 +172,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("accept statement is not allowed", N); + Check_SPARK_Restriction ("accept statement is not allowed", N); -- Entry name is initialized to Any_Id. It should get reset to the -- matching entry entity. An error is signalled if it is not reset. @@ -403,7 +403,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("select statement is not allowed", N); + Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (Max_Asynchronous_Select_Nesting, N); Check_Restriction (No_Select_Statements, N); @@ -449,7 +449,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("select statement is not allowed", N); + Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Ada 2005 (AI-345): The trigger may be a dispatching call @@ -546,7 +546,7 @@ package body Sem_Ch9 is E : constant Node_Id := Expression (N); begin Tasking_Used := True; - Check_Formal_Restriction ("delay statement is not allowed", N); + Check_SPARK_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Relative_Delay, N); Check_Restriction (No_Delay, N); Check_Potentially_Blocking_Operation (N); @@ -564,7 +564,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("delay statement is not allowed", N); + Check_SPARK_Restriction ("delay statement is not allowed", N); Check_Restriction (No_Delay, N); Check_Potentially_Blocking_Operation (N); Analyze (E); @@ -851,7 +851,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("entry call is not allowed", N); + Check_SPARK_Restriction ("entry call is not allowed", N); if Present (Pragmas_Before (N)) then Analyze_List (Pragmas_Before (N)); @@ -1114,7 +1114,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("protected definition is not allowed", N); + Check_SPARK_Restriction ("protected definition is not allowed", N); Analyze_Declarations (Visible_Declarations (N)); if Present (Private_Declarations (N)) @@ -1308,7 +1308,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("requeue statement is not allowed", N); + Check_SPARK_Restriction ("requeue statement is not allowed", N); Check_Restriction (No_Requeue_Statements, N); Check_Unreachable_Code (N); @@ -1582,7 +1582,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("select statement is not allowed", N); + Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Loop to analyze alternatives @@ -1960,7 +1960,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("task definition is not allowed", N); + Check_SPARK_Restriction ("task definition is not allowed", N); if Present (Visible_Declarations (N)) then Analyze_Declarations (Visible_Declarations (N)); @@ -2120,7 +2120,7 @@ package body Sem_Ch9 is begin Tasking_Used := True; - Check_Formal_Restriction ("select statement is not allowed", N); + Check_SPARK_Restriction ("select statement is not allowed", N); Check_Restriction (No_Select_Statements, N); -- Ada 2005 (AI-345): The trigger may be a dispatching call diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index ef406e1..1f0cc13 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3605,7 +3605,7 @@ package body Sem_Res is begin if not Is_SPARK_Object_Reference (Operand) then - Check_Formal_Restriction + Check_SPARK_Restriction ("object required", Operand); -- In formal mode, the only view conversions are those @@ -3621,11 +3621,11 @@ package body Sem_Res is if Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) then - Check_Formal_Restriction + Check_SPARK_Restriction ("ancestor conversion is the only permitted " & "view conversion", A); else - Check_Formal_Restriction + Check_SPARK_Restriction ("ancestor conversion required", A); end if; @@ -3635,7 +3635,7 @@ package body Sem_Res is end; else - Check_Formal_Restriction ("object required", A); + Check_SPARK_Restriction ("object required", A); end if; -- In formal mode, the only view conversions are those @@ -3644,7 +3644,7 @@ package body Sem_Res is elsif Nkind (A) = N_Type_Conversion and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) then - Check_Formal_Restriction + Check_SPARK_Restriction ("ancestor conversion is the only permitted view " & "conversion", A); end if; @@ -4887,9 +4887,9 @@ package body Sem_Res is Generate_Operator_Reference (N, Typ); Eval_Arithmetic_Op (N); - -- In SPARK and ALFA, a multiplication or division with operands of - -- fixed point types shall be qualified or explicitly converted to - -- identify the result type. + -- In SPARK, a multiplication or division with operands of fixed point + -- types shall be qualified or explicitly converted to identify the + -- result type. if (Is_Fixed_Point_Type (Etype (L)) or else Is_Fixed_Point_Type (Etype (R))) @@ -4897,7 +4897,7 @@ package body Sem_Res is and then not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion) then - Check_Formal_Restriction + Check_SPARK_Restriction ("operation should be qualified or explicitly converted", N); end if; @@ -5960,16 +5960,16 @@ package body Sem_Res is Generate_Operator_Reference (N, T); Check_Low_Bound_Tested (N); - -- In SPARK or ALFA, ordering operators <, <=, >, >= are not defined - -- for Boolean types or array types except String. + -- In SPARK, ordering operators <, <=, >, >= are not defined for Boolean + -- types or array types except String. if Is_Boolean_Type (T) then - Check_Formal_Restriction + Check_SPARK_Restriction ("comparison is not defined on Boolean type", N); elsif Is_Array_Type (T) and then Base_Type (T) /= Standard_String then - Check_Formal_Restriction + Check_SPARK_Restriction ("comparison is not defined on array types other than String", N); else null; @@ -6817,9 +6817,9 @@ package body Sem_Res is Resolve (L, T); Resolve (R, T); - -- In SPARK or ALFA, equality operators = and /= for array types - -- other than String are only defined when, for each index position, - -- the operands have equal static bounds. + -- In SPARK, equality operators = and /= for array types other than + -- String are only defined when, for each index position, the + -- operands have equal static bounds. if Is_Array_Type (T) and then Base_Type (T) /= Standard_String @@ -6828,7 +6828,7 @@ package body Sem_Res is and then Etype (R) /= Any_Composite -- or else R in error and then not Matching_Static_Array_Bounds (Etype (L), Etype (R)) then - Check_Formal_Restriction + Check_SPARK_Restriction ("array types should have matching static bounds", N); end if; @@ -7357,10 +7357,10 @@ package body Sem_Res is 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. Of course the types have to match, so only check if operands - -- are compatible and the node itself has no errors. + -- In SPARK, logical operations AND, OR and XOR for arrays are defined + -- only when both operands have same static lower and higher bounds. Of + -- course the types have to match, so only check if operands are + -- compatible and the node itself has no errors. if Is_Array_Type (B_Typ) and then Nkind (N) in N_Binary_Op @@ -7374,7 +7374,7 @@ package body Sem_Res is and then Right_Typ /= Any_Composite -- or Right_Opnd in error and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ) then - Check_Formal_Restriction + Check_SPARK_Restriction ("array types should have matching static bounds", N); end if; end; @@ -7627,7 +7627,7 @@ package body Sem_Res is end loop; if Base_Type (Etype (N)) /= Standard_String then - Check_Formal_Restriction + Check_SPARK_Restriction ("result of concatenation should have type String", N); end if; end Resolve_Op_Concat; @@ -7734,21 +7734,21 @@ package body Sem_Res is Resolve (Arg, Btyp); end if; - -- Concatenation is restricted in SPARK or ALFA: each operand must be - -- either a string literal, a static character expression, or another + -- Concatenation is restricted in SPARK: each operand must be either a + -- string literal, a static character expression, or another -- concatenation. Arg cannot be a concatenation here as callers of -- Resolve_Op_Concat_Arg call it separately on each final operand, past -- concatenation operations. if Is_Character_Type (Etype (Arg)) then if not Is_Static_Expression (Arg) then - Check_Formal_Restriction + Check_SPARK_Restriction ("character operand for concatenation should be static", N); end if; elsif Is_String_Type (Etype (Arg)) then if not Is_Static_Expression (Arg) then - Check_Formal_Restriction + Check_SPARK_Restriction ("string operand for concatenation should be static", N); end if; @@ -8032,7 +8032,7 @@ package body Sem_Res is and then Etype (Expr) /= Any_Composite -- or else Expr in error and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr)) then - Check_Formal_Restriction + Check_SPARK_Restriction ("array types should have matching static bounds", N); end if; @@ -9150,15 +9150,15 @@ package body Sem_Res is Resolve (Operand); - -- In SPARK or ALFA, a type conversion between array types should be - -- restricted to types which have matching static bounds. + -- In SPARK, a type conversion between array types should be restricted + -- to types which have matching static bounds. if Is_Array_Type (Target_Typ) and then Is_Array_Type (Operand_Typ) and then Operand_Typ /= Any_Composite -- or else Operand in error and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ) then - Check_Formal_Restriction + Check_SPARK_Restriction ("array types should have matching static bounds", N); end if; @@ -9172,7 +9172,7 @@ package body Sem_Res is and then Is_Ancestor (Target_Typ, Operand_Typ) and then not Is_SPARK_Object_Reference (Operand) then - Check_Formal_Restriction ("object required", Operand); + Check_SPARK_Restriction ("object required", Operand); end if; -- Note: we do the Eval_Type_Conversion call before applying the @@ -9414,7 +9414,7 @@ package body Sem_Res is begin if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then Error_Msg_Name_1 := Chars (Typ); - Check_Formal_Restriction + Check_SPARK_Restriction ("unary operator not defined for modular type%", N); end if; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index ef65040..b69bada 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -1179,7 +1179,7 @@ package body Sem_Util is end if; else Error_Msg_Sloc := Body_Sloc; - Check_Formal_Restriction + Check_SPARK_Restriction ("decl cannot appear after body#", Decl); end if; end if; @@ -3315,11 +3315,10 @@ package body Sem_Util is Append_Entity (Def_Id, S); Set_Public_Status (Def_Id); - -- Declaring a homonym is not allowed in SPARK or ALFA ... + -- Declaring a homonym is not allowed in SPARK ... if Present (C) - and then (Restriction_Check_Required (SPARK) - or else Formal_Verification_Mode) + and then Restriction_Check_Required (SPARK) then declare @@ -3359,7 +3358,7 @@ package body Sem_Util is and then Comes_From_Source (C) then Error_Msg_Sloc := Sloc (C); - Check_Formal_Restriction + Check_SPARK_Restriction ("redeclaration of identifier &#", Def_Id); end if; end; @@ -10789,7 +10788,7 @@ package body Sem_Util is and then (Typ = 't' or else Ekind (Ent) = E_Package) then Error_Msg_Node_1 := Endl; - Check_Formal_Restriction ("`END &` required", Endl, Force => True); + Check_SPARK_Restriction ("`END &` required", Endl, Force => True); end if; end if; |