+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
-- --
-- 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- --
-- 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
-- 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.
-- --
-- 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- --
-- 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;
-- --
-- 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- --
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 --
-----------------------
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
-- --
-- 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- --
-- 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 --
----------------------------------------
-- 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 --
-----------------------------------------------------
-- 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
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;
-- --
-- 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- --
-- 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;
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;
--------------------
-- --
-- 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- --
-- 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
-- --
-- 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- --
-- Check_Formal_Restriction --
------------------------------
- procedure Check_Formal_Restriction
+ procedure Check_SPARK_Restriction
(Msg : String;
N : Node_Id;
Force : Boolean := False)
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;
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;
-- 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
-- --
-- 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- --
-- 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);
-- --
-- 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- --
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
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
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,
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;
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
-- 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.
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;
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;
-- --
-- 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- --
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;
------------------------
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
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
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;
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;
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;
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;
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;
-- --
-- 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- --
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
-- 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);
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)))
-- 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
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
(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
-- 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);
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;
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))));
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
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));
-- 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
-- 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;
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;
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.
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;
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;
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
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
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;
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);
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
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
Bound_Val : Ureal;
begin
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("decimal fixed point type is not allowed", Def);
Check_Restriction (No_Fixed_Point, Def);
-- 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);
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)
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;
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;
-- 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
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
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);
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
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);
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
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;
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;
-- --
-- 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- --
C : Node_Id;
begin
- Check_Formal_Restriction ("allocator is not allowed", N);
+ Check_SPARK_Restriction ("allocator is not allowed", N);
-- Deal with allocator restrictions
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;
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);
-- 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);
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;
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);
-- 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);
-- --
-- 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- --
-- 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
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;
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;
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;
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
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;
-- 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;
-- 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));
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);
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:
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
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;
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;
-- 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;
-- 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
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
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
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
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);
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);
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);
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;
end loop;
if Present (Formal_Type) then
+ CW_Actual := True;
-- Create declaration and body for class-wide operation
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
-- 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);
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;
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;
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
-- --
-- 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- --
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
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.
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);
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
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);
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);
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));
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))
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);
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
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));
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
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
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;
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
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;
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)))
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;
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;
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
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;
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
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;
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;
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;
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;
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;
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
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;
end if;
else
Error_Msg_Sloc := Body_Sloc;
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("decl cannot appear after body#", Decl);
end if;
end if;
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
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;
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;
projects / gcc.git / commitdiff