OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

sem_aggr.adb, [...]: cleanup of SPARK mode 

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

From-SVN: r177175
This commit is contained in:
Yannick Moy 2011-08-02 15:10:17 +00:00 committed by Arnaud Charlet
parent 0f85303509
commit 2ba431e53e
21 changed files with 218 additions and 282 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
gcc/ada/ChangeLog
View File

@ -1,3 +1,11 @@
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

11
gcc/ada/debug.adb
View File

@ -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.

7
gcc/ada/err_vars.ads
View File

@ -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;

22
gcc/ada/errout.adb
View File

@ -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

22
gcc/ada/errout.ads
View File

@ -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

10
gcc/ada/exp_ch6.adb
View File

@ -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;

14
gcc/ada/gnat1drv.adb
View File

@ -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;
--------------------

5
gcc/ada/opt.ads
View File

@ -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

13
gcc/ada/restrict.adb
View File

@ -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

4
gcc/ada/restrict.ads
View File

@ -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);

26
gcc/ada/sem_aggr.adb
View File

@ -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;

20
gcc/ada/sem_attr.adb
View File

@ -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;

6
gcc/ada/sem_ch11.adb
View File

@ -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);

110
gcc/ada/sem_ch3.adb
View File

@ -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;

16
gcc/ada/sem_ch4.adb
View File

@ -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);

33
gcc/ada/sem_ch5.adb
View File

@ -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));

35
gcc/ada/sem_ch6.adb
View File

@ -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

35
gcc/ada/sem_ch8.adb
View File

@ -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

26
gcc/ada/sem_ch9.adb
View File

@ -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

66
gcc/ada/sem_res.adb
View File

@ -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;

11
gcc/ada/sem_util.adb
View File

@ -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;