[multiple changes]
2014-08-04 Yannick Moy <moy@adacore.com> * sem_aggr.adb, sem_ch3.adb, sem_ch5.adb, sem_ch7.adb, sem_ch9.adb, sem_ch12.adb, sem_util.adb, sem_util.ads, sem_res.adb, sem_attr.adb, exp_ch6.adb, sem_ch4.adb, restrict.adb, restrict.ads, sem_ch6.adb, sem_ch8.adb, sem_ch11.adb: Update some subprogram names to refer to SPARK_05 instead of SPARK. 2014-08-04 Robert Dewar <dewar@adacore.com> * sem.ads: Minor reformatting. * sem_ch13.adb (Analyze_Aspect_External_Or_Link_Name): Minor reformatting. (Analyze_Aspect_Specifications, case Convention): Put External_Name before Link_Name when constructing pragma. From-SVN: r213537
This commit is contained in:
parent
3dd7e28d9f
commit
ce5ba43a4e
|
@ -1,3 +1,19 @@
|
|||
2014-08-04 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* sem_aggr.adb, sem_ch3.adb, sem_ch5.adb, sem_ch7.adb, sem_ch9.adb,
|
||||
sem_ch12.adb, sem_util.adb, sem_util.ads, sem_res.adb, sem_attr.adb,
|
||||
exp_ch6.adb, sem_ch4.adb, restrict.adb, restrict.ads, sem_ch6.adb,
|
||||
sem_ch8.adb, sem_ch11.adb: Update some subprogram names to refer to
|
||||
SPARK_05 instead of SPARK.
|
||||
|
||||
2014-08-04 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* sem.ads: Minor reformatting.
|
||||
* sem_ch13.adb (Analyze_Aspect_External_Or_Link_Name): Minor
|
||||
reformatting.
|
||||
(Analyze_Aspect_Specifications, case Convention): Put External_Name
|
||||
before Link_Name when constructing pragma.
|
||||
|
||||
2014-08-04 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* sem.adb, sem.ads (In_Default_Expr): Global flag that is set
|
||||
|
|
|
@ -5546,7 +5546,7 @@ package body Exp_Ch6 is
|
|||
|
||||
if Nkind (Parent (N)) /= N_Package_Specification then
|
||||
if Nkind (Parent (N)) = N_Compilation_Unit then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subprogram declaration is not a library item", N);
|
||||
|
||||
elsif Present (Next (N))
|
||||
|
@ -5560,7 +5560,7 @@ package body Exp_Ch6 is
|
|||
|
||||
null;
|
||||
else
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subprogram declaration is not allowed here", N);
|
||||
end if;
|
||||
end if;
|
||||
|
|
|
@ -491,7 +491,7 @@ package body Restrict is
|
|||
-- No_Dispatch restriction is not set.
|
||||
|
||||
if R = No_Dispatch then
|
||||
Check_SPARK_Restriction ("class-wide is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("class-wide is not allowed", N);
|
||||
end if;
|
||||
|
||||
if UI_Is_In_Int_Range (V) then
|
||||
|
@ -1418,11 +1418,11 @@ package body Restrict is
|
|||
end if;
|
||||
end Set_Restriction_No_Use_Of_Pragma;
|
||||
|
||||
-----------------------------
|
||||
-- Check_SPARK_Restriction --
|
||||
-----------------------------
|
||||
--------------------------------
|
||||
-- Check_SPARK_05_Restriction --
|
||||
--------------------------------
|
||||
|
||||
procedure Check_SPARK_Restriction
|
||||
procedure Check_SPARK_05_Restriction
|
||||
(Msg : String;
|
||||
N : Node_Id;
|
||||
Force : Boolean := False)
|
||||
|
@ -1471,9 +1471,9 @@ package body Restrict is
|
|||
Error_Msg_F ("\\| " & Msg, N);
|
||||
end if;
|
||||
end if;
|
||||
end Check_SPARK_Restriction;
|
||||
end Check_SPARK_05_Restriction;
|
||||
|
||||
procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id) is
|
||||
procedure Check_SPARK_05_Restriction (Msg1, Msg2 : String; N : Node_Id) is
|
||||
Msg_Issued : Boolean;
|
||||
Save_Error_Msg_Sloc : Source_Ptr;
|
||||
|
||||
|
@ -1500,7 +1500,7 @@ package body Restrict is
|
|||
Error_Msg_F (Msg2, N);
|
||||
end if;
|
||||
end if;
|
||||
end Check_SPARK_Restriction;
|
||||
end Check_SPARK_05_Restriction;
|
||||
|
||||
----------------------------------
|
||||
-- Suppress_Restriction_Message --
|
||||
|
|
|
@ -258,7 +258,7 @@ package Restrict is
|
|||
-- elaboration routine. If elaboration code is not allowed, an error
|
||||
-- message is posted on the node given as argument.
|
||||
|
||||
procedure Check_SPARK_Restriction
|
||||
procedure Check_SPARK_05_Restriction
|
||||
(Msg : String;
|
||||
N : Node_Id;
|
||||
Force : Boolean := False);
|
||||
|
@ -267,9 +267,9 @@ package Restrict is
|
|||
-- the SPARK_05 restriction is set, then an error is issued on N. Msg
|
||||
-- is appended to the restriction failure message.
|
||||
|
||||
procedure Check_SPARK_Restriction (Msg1, Msg2 : String; N : Node_Id);
|
||||
-- Same as Check_SPARK_Restriction except there is a continuation message
|
||||
-- Msg2 following the initial message Msg1.
|
||||
procedure Check_SPARK_05_Restriction (Msg1, Msg2 : String; N : Node_Id);
|
||||
-- Same as Check_SPARK_05_Restriction except there is a continuation
|
||||
-- message Msg2 following the initial message Msg1.
|
||||
|
||||
procedure Check_No_Implicit_Aliasing (Obj : Node_Id);
|
||||
-- Obj is a node for which Is_Aliased_View is True, which is being used in
|
||||
|
|
|
@ -250,13 +250,13 @@ package Sem is
|
|||
-- that expression. Probably a boolean would be good enough, since we think
|
||||
-- that such expressions cannot nest, but that might not be true in the
|
||||
-- future (e.g. if let expressions are added to Ada) so we prepare for that
|
||||
-- future possibility by making it a counter. Like In_Spec_Expression, it
|
||||
-- must be recursively saved on a Semantics call.
|
||||
-- future possibility by making it a counter. As with In_Spec_Expression,
|
||||
-- it must be recursively saved and restored for a Semantics call.
|
||||
|
||||
In_Default_Expr : Boolean := False;
|
||||
-- Switch to indicate that we are analyzing a default component expression.
|
||||
-- Like In_Spec_Expression, it must be recursively saved on a Semantics
|
||||
-- call.
|
||||
-- As with In_Spec_Expression, it must be recursively saved and restored
|
||||
-- for a Semantics call.
|
||||
|
||||
In_Inlined_Body : Boolean := False;
|
||||
-- Switch to indicate that we are analyzing and resolving an inlined body.
|
||||
|
|
|
@ -712,7 +712,7 @@ package body Sem_Aggr is
|
|||
begin
|
||||
if Level = 0 then
|
||||
if Nkind (Parent (Expr)) /= N_Qualified_Expression then
|
||||
Check_SPARK_Restriction ("aggregate should be qualified", Expr);
|
||||
Check_SPARK_05_Restriction ("aggregate should be qualified", Expr);
|
||||
end if;
|
||||
|
||||
else
|
||||
|
@ -925,12 +925,12 @@ package body Sem_Aggr is
|
|||
and then not Is_Constrained (Etype (Name (Parent (N))))
|
||||
then
|
||||
if not Is_Others_Aggregate (N) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("array aggregate should have only OTHERS", N);
|
||||
end if;
|
||||
|
||||
elsif Is_Top_Level_Aggregate (N) then
|
||||
Check_SPARK_Restriction ("aggregate should be qualified", N);
|
||||
Check_SPARK_05_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,
|
||||
|
@ -1934,7 +1934,7 @@ package body Sem_Aggr is
|
|||
or else (Nkind (Choice) = N_Range
|
||||
and then Is_OK_Static_Range (Choice)))
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("choice should be static", Choice);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -2744,7 +2744,7 @@ package body Sem_Aggr is
|
|||
if Is_Entity_Name (A)
|
||||
and then Is_Type (Entity (A))
|
||||
then
|
||||
Check_SPARK_Restriction ("ancestor part cannot be a type mark", A);
|
||||
Check_SPARK_05_Restriction ("ancestor part cannot be a type mark", A);
|
||||
|
||||
-- AI05-0115: if the ancestor part is a subtype mark, the ancestor
|
||||
-- must not have unknown discriminants.
|
||||
|
@ -3512,7 +3512,7 @@ package body Sem_Aggr is
|
|||
then
|
||||
|
||||
if Present (Expressions (N)) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("named association cannot follow positional one",
|
||||
First (Choices (First (Component_Associations (N)))));
|
||||
end if;
|
||||
|
@ -3524,13 +3524,13 @@ package body Sem_Aggr is
|
|||
Assoc := First (Component_Associations (N));
|
||||
while Present (Assoc) loop
|
||||
if List_Length (Choices (Assoc)) > 1 then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("component association in record aggregate must "
|
||||
& "contain a single choice", Assoc);
|
||||
end if;
|
||||
|
||||
if Nkind (First (Choices (Assoc))) = N_Others_Choice then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("record aggregate cannot contain OTHERS", Assoc);
|
||||
end if;
|
||||
|
||||
|
|
|
@ -320,7 +320,7 @@ package body Sem_Attr is
|
|||
-- Verify that prefix of attribute N is a float type and that
|
||||
-- two attribute expressions are present
|
||||
|
||||
procedure Check_SPARK_Restriction_On_Attribute;
|
||||
procedure Check_SPARK_05_Restriction_On_Attribute;
|
||||
-- Issue an error in formal mode because attribute N is allowed
|
||||
|
||||
procedure Check_Integer_Type;
|
||||
|
@ -755,7 +755,7 @@ package body Sem_Attr is
|
|||
-- Start of processing for Analyze_Access_Attribute
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_E0;
|
||||
|
||||
if Nkind (P) = N_Character_Literal then
|
||||
|
@ -1804,14 +1804,14 @@ package body Sem_Attr is
|
|||
end Check_Scalar_Type;
|
||||
|
||||
------------------------------------------
|
||||
-- Check_SPARK_Restriction_On_Attribute --
|
||||
-- Check_SPARK_05_Restriction_On_Attribute --
|
||||
------------------------------------------
|
||||
|
||||
procedure Check_SPARK_Restriction_On_Attribute is
|
||||
procedure Check_SPARK_05_Restriction_On_Attribute is
|
||||
begin
|
||||
Error_Msg_Name_1 := Aname;
|
||||
Check_SPARK_Restriction ("attribute % is not allowed", P);
|
||||
end Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction ("attribute % is not allowed", P);
|
||||
end Check_SPARK_05_Restriction_On_Attribute;
|
||||
|
||||
---------------------------
|
||||
-- Check_Standard_Prefix --
|
||||
|
@ -2556,7 +2556,7 @@ package body Sem_Attr is
|
|||
and then not In_Open_Scopes (Scope (P_Type))
|
||||
and then not In_Spec_Expression
|
||||
then
|
||||
Check_SPARK_Restriction ("invisible attribute of type", N);
|
||||
Check_SPARK_05_Restriction ("invisible attribute of type", N);
|
||||
end if;
|
||||
|
||||
-- Remaining processing depends on attribute
|
||||
|
@ -2726,7 +2726,7 @@ package body Sem_Attr is
|
|||
|
||||
if Nkind (Parent (N)) /= N_Attribute_Reference then
|
||||
Error_Msg_Name_1 := Aname;
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is only allowed as prefix of another attribute", P);
|
||||
end if;
|
||||
|
||||
|
@ -3571,7 +3571,7 @@ package body Sem_Attr is
|
|||
|
||||
when Attribute_Image => Image :
|
||||
begin
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_Scalar_Type;
|
||||
Set_Etype (N, Standard_String);
|
||||
|
||||
|
@ -4770,7 +4770,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is not allowed for type%", P);
|
||||
end if;
|
||||
|
||||
|
@ -4796,7 +4796,8 @@ 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_SPARK_Restriction ("attribute% is not allowed for type%", P);
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is not allowed for type%", P);
|
||||
end if;
|
||||
|
||||
Resolve (E1, P_Base_Type);
|
||||
|
@ -5689,7 +5690,8 @@ 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_SPARK_Restriction ("attribute% is not allowed for type%", P);
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is not allowed for type%", P);
|
||||
end if;
|
||||
|
||||
Resolve (E1, P_Base_Type);
|
||||
|
@ -6392,7 +6394,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is not allowed for type%", P);
|
||||
end if;
|
||||
|
||||
|
@ -6471,7 +6473,7 @@ package body Sem_Attr is
|
|||
|
||||
when Attribute_Value => Value :
|
||||
begin
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_E1;
|
||||
Check_Scalar_Type;
|
||||
|
||||
|
@ -6550,7 +6552,7 @@ package body Sem_Attr is
|
|||
|
||||
when Attribute_Wide_Image => Wide_Image :
|
||||
begin
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_Scalar_Type;
|
||||
Set_Etype (N, Standard_Wide_String);
|
||||
Check_E1;
|
||||
|
@ -6593,7 +6595,7 @@ package body Sem_Attr is
|
|||
|
||||
when Attribute_Wide_Value => Wide_Value :
|
||||
begin
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_E1;
|
||||
Check_Scalar_Type;
|
||||
|
||||
|
@ -6650,7 +6652,7 @@ package body Sem_Attr is
|
|||
----------------
|
||||
|
||||
when Attribute_Wide_Width =>
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_E0;
|
||||
Check_Scalar_Type;
|
||||
Set_Etype (N, Universal_Integer);
|
||||
|
@ -6660,7 +6662,7 @@ package body Sem_Attr is
|
|||
-----------
|
||||
|
||||
when Attribute_Width =>
|
||||
Check_SPARK_Restriction_On_Attribute;
|
||||
Check_SPARK_05_Restriction_On_Attribute;
|
||||
Check_E0;
|
||||
Check_Scalar_Type;
|
||||
Set_Etype (N, Universal_Integer);
|
||||
|
|
|
@ -437,7 +437,7 @@ package body Sem_Ch11 is
|
|||
Check_Compiler_Unit ("raise expression", N);
|
||||
end if;
|
||||
|
||||
Check_SPARK_Restriction ("raise expression is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("raise expression is not allowed", N);
|
||||
|
||||
-- Check exception restrictions on the original source
|
||||
|
||||
|
@ -495,7 +495,7 @@ package body Sem_Ch11 is
|
|||
|
||||
begin
|
||||
if Comes_From_Source (N) then
|
||||
Check_SPARK_Restriction ("raise statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("raise statement is not allowed", N);
|
||||
end if;
|
||||
|
||||
Check_Unreachable_Code (N);
|
||||
|
@ -702,7 +702,7 @@ package body Sem_Ch11 is
|
|||
|
||||
begin
|
||||
if Nkind (Original_Node (N)) = N_Raise_Statement then
|
||||
Check_SPARK_Restriction ("raise statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("raise statement is not allowed", N);
|
||||
end if;
|
||||
|
||||
if No (Etype (N)) then
|
||||
|
|
|
@ -3189,7 +3189,7 @@ package body Sem_Ch12 is
|
|||
Decl : Node_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("generic is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("generic is not allowed", N);
|
||||
|
||||
-- We introduce a renaming of the enclosing package, to have a usable
|
||||
-- entity as the prefix of an expanded name for a local entity of the
|
||||
|
@ -3322,7 +3322,7 @@ package body Sem_Ch12 is
|
|||
Typ : Entity_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("generic is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("generic is not allowed", N);
|
||||
|
||||
-- Create copy of generic unit, and save for instantiation. If the unit
|
||||
-- is a child unit, do not copy the specifications for the parent, which
|
||||
|
@ -3618,7 +3618,7 @@ package body Sem_Ch12 is
|
|||
-- Start of processing for Analyze_Package_Instantiation
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("generic is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("generic is not allowed", N);
|
||||
|
||||
-- Very first thing: check for Text_IO sp[ecial unit in case we are
|
||||
-- instantiating one of the children of [[Wide_]Wide_]Text_IO.
|
||||
|
@ -4865,7 +4865,7 @@ package body Sem_Ch12 is
|
|||
-- Start of processing for Analyze_Subprogram_Instantiation
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("generic is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("generic is not allowed", N);
|
||||
|
||||
-- Very first thing: check for special Text_IO unit in case we are
|
||||
-- instantiating one of the children of [[Wide_]Wide_]Text_IO. Of course
|
||||
|
|
|
@ -1927,14 +1927,14 @@ package body Sem_Ch13 is
|
|||
|
||||
-- Assemble the full argument list
|
||||
|
||||
if Present (Link_Arg) then
|
||||
Append_To (Args, Link_Arg);
|
||||
end if;
|
||||
|
||||
if Present (Extern_Arg) then
|
||||
Append_To (Args, Extern_Arg);
|
||||
end if;
|
||||
|
||||
if Present (Link_Arg) then
|
||||
Append_To (Args, Link_Arg);
|
||||
end if;
|
||||
|
||||
Make_Aitem_Pragma
|
||||
(Pragma_Argument_Associations => Args,
|
||||
Pragma_Name => Prag_Nam);
|
||||
|
|
|
@ -730,7 +730,7 @@ package body Sem_Ch3 is
|
|||
Enclosing_Prot_Type : Entity_Id := Empty;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("access type is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("access type is not allowed", N);
|
||||
|
||||
if Is_Entry (Current_Scope)
|
||||
and then Is_Task_Type (Etype (Scope (Current_Scope)))
|
||||
|
@ -1053,7 +1053,7 @@ package body Sem_Ch3 is
|
|||
-- Start of processing for Access_Subprogram_Declaration
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("access type is not allowed", T_Def);
|
||||
Check_SPARK_05_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
|
||||
|
@ -1322,7 +1322,7 @@ package body Sem_Ch3 is
|
|||
Full_Desig : Entity_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("access type is not allowed", Def);
|
||||
Check_SPARK_05_Restriction ("access type is not allowed", Def);
|
||||
|
||||
-- Check for permissible use of incomplete type
|
||||
|
||||
|
@ -1884,7 +1884,7 @@ package body Sem_Ch3 is
|
|||
(Subtype_Indication (Component_Definition (N)), N);
|
||||
|
||||
if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
|
||||
Check_SPARK_Restriction ("subtype mark required", Typ);
|
||||
Check_SPARK_05_Restriction ("subtype mark required", Typ);
|
||||
end if;
|
||||
|
||||
-- Ada 2005 (AI-230): Access Definition case
|
||||
|
@ -1937,7 +1937,7 @@ package body Sem_Ch3 is
|
|||
-- package Sem).
|
||||
|
||||
if Present (E) then
|
||||
Check_SPARK_Restriction ("default expression is not allowed", E);
|
||||
Check_SPARK_05_Restriction ("default expression is not allowed", E);
|
||||
Preanalyze_Default_Expression (E, T);
|
||||
Check_Initialization (T, E);
|
||||
|
||||
|
@ -2256,7 +2256,7 @@ package body Sem_Ch3 is
|
|||
if Nkind (Decl) = N_Package_Declaration
|
||||
and then Nkind (Parent (L)) = N_Package_Specification
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("package specification cannot contain a package declaration",
|
||||
Decl);
|
||||
end if;
|
||||
|
@ -2549,7 +2549,7 @@ package body Sem_Ch3 is
|
|||
|
||||
when N_Record_Definition =>
|
||||
if Present (Discriminant_Specifications (N)) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("discriminant type is not allowed",
|
||||
Defining_Identifier
|
||||
(First (Discriminant_Specifications (N))));
|
||||
|
@ -2658,7 +2658,7 @@ package body Sem_Ch3 is
|
|||
-- Controlled type is not allowed in SPARK
|
||||
|
||||
if Is_Visibly_Controlled (T) then
|
||||
Check_SPARK_Restriction ("controlled type is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("controlled type is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- Some common processing for all types
|
||||
|
@ -2775,7 +2775,7 @@ package body Sem_Ch3 is
|
|||
T : Entity_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("incomplete type is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("incomplete type is not allowed", N);
|
||||
|
||||
Generate_Definition (Defining_Identifier (N));
|
||||
|
||||
|
@ -3448,14 +3448,14 @@ package body Sem_Ch3 is
|
|||
if not
|
||||
Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subtype mark of constrained type expected",
|
||||
Object_Definition (N));
|
||||
end if;
|
||||
|
@ -3463,7 +3463,7 @@ package body Sem_Ch3 is
|
|||
-- There are no aliased objects in SPARK
|
||||
|
||||
if Aliased_Present (N) then
|
||||
Check_SPARK_Restriction ("aliased object is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("aliased object is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- Process initialization expression if present and not in error
|
||||
|
@ -3618,9 +3618,9 @@ package body Sem_Ch3 is
|
|||
-- Only call test if needed
|
||||
|
||||
and then Restriction_Check_Required (SPARK_05)
|
||||
and then not Is_SPARK_Initialization_Expr (Original_Node (E))
|
||||
and then not Is_SPARK_05_Initialization_Expr (Original_Node (E))
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("initialization expression is not appropriate", E);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -3676,7 +3676,7 @@ package body Sem_Ch3 is
|
|||
-- only for constants of type string.
|
||||
|
||||
if Is_String_Type (T) and then not Constant_Present (N) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("declaration of object of unconstrained type not allowed", N);
|
||||
end if;
|
||||
|
||||
|
@ -4460,7 +4460,7 @@ package body Sem_Ch3 is
|
|||
if Is_Boolean_Type (T)
|
||||
and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subtype of Boolean cannot have constraint", N);
|
||||
end if;
|
||||
|
||||
|
@ -4482,7 +4482,7 @@ package body Sem_Ch3 is
|
|||
if not
|
||||
Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subtype mark required", One_Cstr);
|
||||
|
||||
-- String subtype must have a lower bound of 1 in SPARK.
|
||||
|
@ -4496,7 +4496,7 @@ package body Sem_Ch3 is
|
|||
if Is_OK_Static_Expression (Low)
|
||||
and then Expr_Value (Low) /= 1
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("String subtype must have lower bound of 1", N);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -4518,7 +4518,7 @@ package body Sem_Ch3 is
|
|||
-- in SPARK.
|
||||
|
||||
if Is_Array_Type (T) and then not Is_Constrained (T) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subtype of unconstrained array must have constraint", N);
|
||||
end if;
|
||||
|
||||
|
@ -5092,7 +5092,7 @@ package body Sem_Ch3 is
|
|||
-- Check SPARK restriction requiring a subtype mark
|
||||
|
||||
if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
|
||||
Check_SPARK_Restriction ("subtype mark required", Index);
|
||||
Check_SPARK_05_Restriction ("subtype mark required", Index);
|
||||
end if;
|
||||
|
||||
-- Add a subtype declaration for each index of private array type
|
||||
|
@ -5169,7 +5169,8 @@ package body Sem_Ch3 is
|
|||
Set_Etype (Component_Typ, Element_Type);
|
||||
|
||||
if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
|
||||
Check_SPARK_Restriction ("subtype mark required", Component_Typ);
|
||||
Check_SPARK_05_Restriction
|
||||
("subtype mark required", Component_Typ);
|
||||
end if;
|
||||
|
||||
-- Ada 2005 (AI-230): Access Definition case
|
||||
|
@ -5282,7 +5283,7 @@ package body Sem_Ch3 is
|
|||
Set_Packed_Array_Impl_Type (T, Empty);
|
||||
|
||||
if Aliased_Present (Component_Definition (Def)) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("aliased is not allowed", Component_Definition (Def));
|
||||
Set_Has_Aliased_Components (Etype (T));
|
||||
end if;
|
||||
|
@ -12123,7 +12124,7 @@ package body Sem_Ch3 is
|
|||
else
|
||||
pragma Assert (Nkind (C) = N_Digits_Constraint);
|
||||
|
||||
Check_SPARK_Restriction ("digits constraint is not allowed", S);
|
||||
Check_SPARK_05_Restriction ("digits constraint is not allowed", S);
|
||||
|
||||
Digits_Expr := Digits_Expression (C);
|
||||
Analyze_And_Resolve (Digits_Expr, Any_Integer);
|
||||
|
@ -12351,7 +12352,7 @@ package body Sem_Ch3 is
|
|||
|
||||
if Nkind (C) = N_Digits_Constraint then
|
||||
|
||||
Check_SPARK_Restriction ("digits constraint is not allowed", S);
|
||||
Check_SPARK_05_Restriction ("digits constraint is not allowed", S);
|
||||
Check_Restriction (No_Obsolescent_Features, C);
|
||||
|
||||
if Warn_On_Obsolescent_Feature then
|
||||
|
@ -12582,7 +12583,7 @@ package body Sem_Ch3 is
|
|||
|
||||
if Nkind (C) = N_Delta_Constraint then
|
||||
|
||||
Check_SPARK_Restriction ("delta constraint is not allowed", S);
|
||||
Check_SPARK_05_Restriction ("delta constraint is not allowed", S);
|
||||
Check_Restriction (No_Obsolescent_Features, C);
|
||||
|
||||
if Warn_On_Obsolescent_Feature then
|
||||
|
@ -13235,7 +13236,7 @@ package body Sem_Ch3 is
|
|||
Bound_Val : Ureal;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("decimal fixed point type is not allowed", Def);
|
||||
Check_Restriction (No_Fixed_Point, Def);
|
||||
|
||||
|
@ -14790,7 +14791,7 @@ package body Sem_Ch3 is
|
|||
-- parent is also an interface.
|
||||
|
||||
if Interface_Present (Def) then
|
||||
Check_SPARK_Restriction ("interface is not allowed", Def);
|
||||
Check_SPARK_05_Restriction ("interface is not allowed", Def);
|
||||
|
||||
if not Is_Interface (Parent_Type) then
|
||||
Diagnose_Interface (Indic, Parent_Type);
|
||||
|
@ -15044,7 +15045,7 @@ package body Sem_Ch3 is
|
|||
Defining_Identifier (First (Discriminant_Specifications (N))));
|
||||
Set_Has_Discriminants (T, False);
|
||||
else
|
||||
Check_SPARK_Restriction ("discriminant type is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("discriminant type is not allowed", N);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
@ -15235,7 +15236,7 @@ package body Sem_Ch3 is
|
|||
-- extensions of tagged record types.
|
||||
|
||||
if No (Extension) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("derived type is not allowed", Original_Node (N));
|
||||
end if;
|
||||
end Derived_Type_Declaration;
|
||||
|
@ -17577,7 +17578,7 @@ package body Sem_Ch3 is
|
|||
-- Non-binary case
|
||||
|
||||
elsif M_Val < 2 ** Bits then
|
||||
Check_SPARK_Restriction ("modulus should be a power of 2", T);
|
||||
Check_SPARK_05_Restriction ("modulus should be a power of 2", T);
|
||||
Set_Non_Binary_Modulus (T);
|
||||
|
||||
if Bits > System_Max_Nonbinary_Modulus_Power then
|
||||
|
@ -18507,7 +18508,7 @@ package body Sem_Ch3 is
|
|||
|
||||
if Priv_Parent /= Full_Parent then
|
||||
Error_Msg_Name_1 := Chars (Priv_Parent);
|
||||
Check_SPARK_Restriction ("% expected", Full_Indic);
|
||||
Check_SPARK_05_Restriction ("% expected", Full_Indic);
|
||||
end if;
|
||||
|
||||
-- Check the rules of 7.3(10): if the private extension inherits
|
||||
|
@ -19113,7 +19114,7 @@ package body Sem_Ch3 is
|
|||
if not In_Iter_Schm
|
||||
and then not Is_OK_Static_Range (R)
|
||||
then
|
||||
Check_SPARK_Restriction ("range should be static", R);
|
||||
Check_SPARK_05_Restriction ("range should be static", R);
|
||||
end if;
|
||||
|
||||
Lo := Low_Bound (R);
|
||||
|
@ -20269,11 +20270,11 @@ package body Sem_Ch3 is
|
|||
or else not Interface_Present (Def)
|
||||
then
|
||||
if Limited_Present (Def) then
|
||||
Check_SPARK_Restriction ("limited is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("limited is not allowed", N);
|
||||
end if;
|
||||
|
||||
if Abstract_Present (Def) then
|
||||
Check_SPARK_Restriction ("abstract is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("abstract is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- The flag Is_Tagged_Type might have already been set by
|
||||
|
@ -20295,7 +20296,7 @@ package body Sem_Ch3 is
|
|||
or else Abstract_Present (Def));
|
||||
|
||||
else
|
||||
Check_SPARK_Restriction ("interface is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("interface is not allowed", N);
|
||||
|
||||
Is_Tagged := True;
|
||||
Analyze_Interface_Declaration (T, Def);
|
||||
|
@ -20459,13 +20460,13 @@ package body Sem_Ch3 is
|
|||
if Nkind (Ctxt) = N_Package_Body
|
||||
and then Nkind (Parent (Ctxt)) = N_Compilation_Unit
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("type should be defined in library unit package", Typ);
|
||||
end if;
|
||||
end;
|
||||
|
@ -20494,14 +20495,14 @@ package body Sem_Ch3 is
|
|||
or else Null_Present (Component_List (Def))
|
||||
then
|
||||
if not Is_Tagged_Type (T) then
|
||||
Check_SPARK_Restriction ("untagged record cannot be null", Def);
|
||||
Check_SPARK_05_Restriction ("untagged record cannot be null", Def);
|
||||
end if;
|
||||
|
||||
else
|
||||
Analyze_Declarations (Component_Items (Component_List (Def)));
|
||||
|
||||
if Present (Variant_Part (Component_List (Def))) then
|
||||
Check_SPARK_Restriction ("variant part is not allowed", Def);
|
||||
Check_SPARK_05_Restriction ("variant part is not allowed", Def);
|
||||
Analyze (Variant_Part (Component_List (Def)));
|
||||
end if;
|
||||
end if;
|
||||
|
|
|
@ -403,7 +403,7 @@ package body Sem_Ch4 is
|
|||
Onode : Node_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("allocator is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("allocator is not allowed", N);
|
||||
|
||||
-- Deal with allocator restrictions
|
||||
|
||||
|
@ -936,7 +936,7 @@ package body Sem_Ch4 is
|
|||
case Nkind (Actual) is
|
||||
when N_Parameter_Association =>
|
||||
if Named_Seen then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("named association cannot follow positional one",
|
||||
Actual);
|
||||
exit;
|
||||
|
@ -1833,7 +1833,7 @@ package body Sem_Ch4 is
|
|||
-- source node check, because ???
|
||||
|
||||
if Comes_From_Source (N) then
|
||||
Check_SPARK_Restriction ("explicit dereference is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("explicit dereference is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- In formal verification mode, keep track of all reads and writes
|
||||
|
@ -2052,7 +2052,7 @@ package body Sem_Ch4 is
|
|||
end if;
|
||||
|
||||
if Comes_From_Source (N) then
|
||||
Check_SPARK_Restriction ("if expression is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("if expression is not allowed", N);
|
||||
end if;
|
||||
|
||||
Else_Expr := Next (Then_Expr);
|
||||
|
@ -2887,7 +2887,7 @@ package body Sem_Ch4 is
|
|||
|
||||
procedure Analyze_Null (N : Node_Id) is
|
||||
begin
|
||||
Check_SPARK_Restriction ("null is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("null is not allowed", N);
|
||||
|
||||
Set_Etype (N, Any_Access);
|
||||
end Analyze_Null;
|
||||
|
@ -3664,7 +3664,7 @@ package body Sem_Ch4 is
|
|||
-- Start of processing for Analyze_Quantified_Expression
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("quantified expression is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("quantified expression is not allowed", N);
|
||||
|
||||
-- Create a scope to emulate the loop-like behavior of the quantified
|
||||
-- expression. The scope is needed to provide proper visibility of the
|
||||
|
@ -4877,7 +4877,7 @@ package body Sem_Ch4 is
|
|||
|
||||
begin
|
||||
if Comes_From_Source (N) then
|
||||
Check_SPARK_Restriction ("slice is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("slice is not allowed", N);
|
||||
end if;
|
||||
|
||||
Analyze (P);
|
||||
|
|
|
@ -893,7 +893,7 @@ package body Sem_Ch5 is
|
|||
-- block statements generated by the expander is fine.
|
||||
|
||||
if Nkind (Original_Node (N)) = N_Block_Statement then
|
||||
Check_SPARK_Restriction ("block statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("block statement is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- If no handled statement sequence is present, things are really messed
|
||||
|
@ -1212,7 +1212,7 @@ package body Sem_Ch5 is
|
|||
-- Case statement with single OTHERS alternative not allowed in SPARK
|
||||
|
||||
if Others_Present and then List_Length (Alternatives (N)) = 1 then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("OTHERS as unique case alternative is not allowed", N);
|
||||
end if;
|
||||
|
||||
|
@ -1299,7 +1299,7 @@ package body Sem_Ch5 is
|
|||
|
||||
else
|
||||
if Has_Loop_In_Inner_Open_Scopes (U_Name) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("exit label must name the closest enclosing loop", N);
|
||||
end if;
|
||||
|
||||
|
@ -1343,34 +1343,34 @@ package body Sem_Ch5 is
|
|||
|
||||
if Present (Cond) then
|
||||
if Nkind (Parent (N)) /= N_Loop_Statement then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("exit must be in IF without ELSIF", N);
|
||||
else
|
||||
Check_SPARK_Restriction ("exit must be directly in IF", N);
|
||||
Check_SPARK_05_Restriction ("exit must be directly in IF", N);
|
||||
end if;
|
||||
|
||||
elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_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_SPARK_Restriction ("exit must be in IF without ELSE", N);
|
||||
Check_SPARK_05_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_SPARK_Restriction ("exit must be in IF without ELSIF", N);
|
||||
Check_SPARK_05_Restriction ("exit must be in IF without ELSIF", N);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
@ -1398,7 +1398,7 @@ package body Sem_Ch5 is
|
|||
Label_Ent : Entity_Id;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("goto statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("goto statement is not allowed", N);
|
||||
|
||||
-- Actual semantic checks
|
||||
|
||||
|
@ -2481,7 +2481,7 @@ package body Sem_Ch5 is
|
|||
-- Loop parameter specification must include subtype mark in SPARK
|
||||
|
||||
if Nkind (DS) = N_Range then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("loop parameter specification must include subtype mark", N);
|
||||
end if;
|
||||
|
||||
|
@ -3348,7 +3348,7 @@ package body Sem_Ch5 is
|
|||
-- Now issue the warning (or error in formal mode)
|
||||
|
||||
if Restriction_Check_Required (SPARK_05) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("unreachable code is not allowed", Error_Node);
|
||||
else
|
||||
Error_Msg ("??unreachable code!", Sloc (Error_Node));
|
||||
|
|
|
@ -213,7 +213,7 @@ package body Sem_Ch6 is
|
|||
Scop : constant Entity_Id := Current_Scope;
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N);
|
||||
|
||||
Generate_Definition (Designator);
|
||||
Set_Contract (Designator, Make_Contract (Sloc (Designator)));
|
||||
|
@ -882,12 +882,12 @@ package body Sem_Ch6 is
|
|||
(Nkind (Parent (Parent (N))) /= N_Subprogram_Body
|
||||
or else Present (Next (N)))
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("RETURN should be the last statement in function", N);
|
||||
end if;
|
||||
|
||||
else
|
||||
Check_SPARK_Restriction ("extended RETURN is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("extended RETURN is not allowed", N);
|
||||
|
||||
-- Analyze parts specific to extended_return_statement:
|
||||
|
||||
|
@ -1861,7 +1861,7 @@ package body Sem_Ch6 is
|
|||
|
||||
if Result_Definition (N) /= Error then
|
||||
if Nkind (Result_Definition (N)) = N_Access_Definition then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("access result is not allowed", Result_Definition (N));
|
||||
|
||||
-- Ada 2005 (AI-254): Handle anonymous access to subprograms
|
||||
|
@ -1895,7 +1895,7 @@ package body Sem_Ch6 is
|
|||
-- Unconstrained array as result is not allowed in SPARK
|
||||
|
||||
if Is_Array_Type (Typ) and then not Is_Constrained (Typ) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("returning an unconstrained array is not allowed",
|
||||
Result_Definition (N));
|
||||
end if;
|
||||
|
@ -2674,7 +2674,7 @@ package body Sem_Ch6 is
|
|||
and then not Nkind_In (Stat, N_Simple_Return_Statement,
|
||||
N_Extended_Return_Statement)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("last statement in function should be RETURN", Stat);
|
||||
end if;
|
||||
end;
|
||||
|
@ -2692,7 +2692,7 @@ package body Sem_Ch6 is
|
|||
-- borrow the Check_Returns procedure here ???
|
||||
|
||||
if Return_Present (Id) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("procedure should not have RETURN", N);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -4144,7 +4144,7 @@ package body Sem_Ch6 is
|
|||
if Nkind (Specification (N)) = N_Procedure_Specification
|
||||
and then Null_Present (Specification (N))
|
||||
then
|
||||
Check_SPARK_Restriction ("null procedure is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("null procedure is not allowed", N);
|
||||
|
||||
if Is_Protected_Type (Current_Scope) then
|
||||
Error_Msg_N ("protected operation cannot be a null procedure", N);
|
||||
|
@ -4351,7 +4351,8 @@ package body Sem_Ch6 is
|
|||
if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
|
||||
and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
|
||||
then
|
||||
Check_SPARK_Restriction ("user-defined operator is not allowed", N);
|
||||
Check_SPARK_05_Restriction
|
||||
("user-defined operator is not allowed", N);
|
||||
end if;
|
||||
|
||||
-- Proceed with analysis. Do not emit a cross-reference entry if the
|
||||
|
@ -9771,7 +9772,7 @@ package body Sem_Ch6 is
|
|||
|
||||
if Nkind (S) /= N_Defining_Operator_Symbol then
|
||||
Error_Msg_Sloc := Sloc (Homonym (S));
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("overloading not allowed with entity#", S);
|
||||
end if;
|
||||
|
||||
|
@ -10081,7 +10082,7 @@ package body Sem_Ch6 is
|
|||
Default := Expression (Param_Spec);
|
||||
|
||||
if Present (Default) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("default expression is not allowed", Default);
|
||||
|
||||
if Out_Present (Param_Spec) then
|
||||
|
|
|
@ -1093,7 +1093,7 @@ package body Sem_Ch7 is
|
|||
|
||||
else
|
||||
Error_Msg_Sloc := Sloc (Previous);
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("at most one tagged type or type extension allowed",
|
||||
"\\ previous declaration#",
|
||||
Decl);
|
||||
|
|
|
@ -552,7 +552,7 @@ package body Sem_Ch8 is
|
|||
Nam : constant Node_Id := Name (N);
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("exception renaming is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("exception renaming is not allowed", N);
|
||||
|
||||
Enter_Name (Id);
|
||||
Analyze (Nam);
|
||||
|
@ -658,7 +658,7 @@ package body Sem_Ch8 is
|
|||
return;
|
||||
end if;
|
||||
|
||||
Check_SPARK_Restriction ("generic renaming is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("generic renaming is not allowed", N);
|
||||
|
||||
Generate_Definition (New_P);
|
||||
|
||||
|
@ -836,7 +836,7 @@ package body Sem_Ch8 is
|
|||
return;
|
||||
end if;
|
||||
|
||||
Check_SPARK_Restriction ("object renaming is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("object renaming is not allowed", N);
|
||||
|
||||
Set_Is_Pure (Id, Is_Pure (Current_Scope));
|
||||
Enter_Name (Id);
|
||||
|
@ -3430,7 +3430,7 @@ package body Sem_Ch8 is
|
|||
-- Start of processing for Analyze_Use_Package
|
||||
|
||||
begin
|
||||
Check_SPARK_Restriction ("use clause is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("use clause is not allowed", N);
|
||||
|
||||
Set_Hidden_By_Use_Clause (N, No_Elist);
|
||||
|
||||
|
@ -6392,12 +6392,13 @@ package body Sem_Ch8 is
|
|||
|
||||
if Restriction_Check_Required (SPARK_05) then
|
||||
if Nkind (Selector_Name (N)) = N_Character_Literal then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_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_SPARK_Restriction ("operator symbol cannot be prefixed", N);
|
||||
Check_SPARK_05_Restriction
|
||||
("operator symbol cannot be prefixed", N);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
@ -6765,10 +6766,10 @@ package body Sem_Ch8 is
|
|||
and then Restriction_Check_Required (SPARK_05)
|
||||
then
|
||||
if Is_Subprogram (P_Name) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("prefix of expanded name cannot be a subprogram", P);
|
||||
elsif Ekind (P_Name) = E_Loop then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("prefix of expanded name cannot be a loop statement", P);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -6927,7 +6928,7 @@ package body Sem_Ch8 is
|
|||
|
||||
elsif Attribute_Name (N) = Name_Base then
|
||||
Error_Msg_Name_1 := Name_Base;
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("attribute% is only allowed as prefix of another attribute", N);
|
||||
|
||||
if Ada_Version = Ada_83 and then Comes_From_Source (N) then
|
||||
|
|
|
@ -701,7 +701,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("abort statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("abort statement is not allowed", N);
|
||||
|
||||
T_Name := First (Names (N));
|
||||
while Present (T_Name) loop
|
||||
|
@ -772,7 +772,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("accept statement is not allowed", N);
|
||||
Check_SPARK_05_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.
|
||||
|
@ -1003,7 +1003,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (Max_Asynchronous_Select_Nesting, N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
|
@ -1049,7 +1049,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
-- Ada 2005 (AI-345): The trigger may be a dispatching call
|
||||
|
@ -1146,7 +1146,7 @@ package body Sem_Ch9 is
|
|||
E : constant Node_Id := Expression (N);
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("delay statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("delay statement is not allowed", N);
|
||||
Check_Restriction (No_Relative_Delay, N);
|
||||
Check_Restriction (No_Delay, N);
|
||||
Check_Potentially_Blocking_Operation (N);
|
||||
|
@ -1164,7 +1164,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("delay statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("delay statement is not allowed", N);
|
||||
Check_Restriction (No_Delay, N);
|
||||
Check_Potentially_Blocking_Operation (N);
|
||||
Analyze (E);
|
||||
|
@ -1453,7 +1453,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("entry call is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("entry call is not allowed", N);
|
||||
|
||||
if Present (Pragmas_Before (N)) then
|
||||
Analyze_List (Pragmas_Before (N));
|
||||
|
@ -1886,7 +1886,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("protected definition is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("protected definition is not allowed", N);
|
||||
Analyze_Declarations (Visible_Declarations (N));
|
||||
|
||||
if Present (Private_Declarations (N))
|
||||
|
@ -2176,7 +2176,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("requeue statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("requeue statement is not allowed", N);
|
||||
Check_Restriction (No_Requeue_Statements, N);
|
||||
Check_Unreachable_Code (N);
|
||||
|
||||
|
@ -2471,7 +2471,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
-- Loop to analyze alternatives
|
||||
|
@ -2862,7 +2862,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("task definition is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("task definition is not allowed", N);
|
||||
|
||||
if Present (Visible_Declarations (N)) then
|
||||
Analyze_Declarations (Visible_Declarations (N));
|
||||
|
@ -3045,7 +3045,7 @@ package body Sem_Ch9 is
|
|||
|
||||
begin
|
||||
Tasking_Used := True;
|
||||
Check_SPARK_Restriction ("select statement is not allowed", N);
|
||||
Check_SPARK_05_Restriction ("select statement is not allowed", N);
|
||||
Check_Restriction (No_Select_Statements, N);
|
||||
|
||||
-- Ada 2005 (AI-345): The trigger may be a dispatching call
|
||||
|
|
|
@ -3885,7 +3885,7 @@ package body Sem_Res is
|
|||
-- conversions of objects), not general expressions.
|
||||
|
||||
if Is_Actual_Tagged_Parameter (A) then
|
||||
if Is_SPARK_Object_Reference (A) then
|
||||
if Is_SPARK_05_Object_Reference (A) then
|
||||
null;
|
||||
|
||||
elsif Nkind (A) = N_Type_Conversion then
|
||||
|
@ -3895,8 +3895,8 @@ package body Sem_Res is
|
|||
Target_Typ : constant Entity_Id := A_Typ;
|
||||
|
||||
begin
|
||||
if not Is_SPARK_Object_Reference (Operand) then
|
||||
Check_SPARK_Restriction
|
||||
if not Is_SPARK_05_Object_Reference (Operand) then
|
||||
Check_SPARK_05_Restriction
|
||||
("object required", Operand);
|
||||
|
||||
-- In formal mode, the only view conversions are those
|
||||
|
@ -3912,11 +3912,11 @@ package body Sem_Res is
|
|||
if Ekind_In
|
||||
(F, E_Out_Parameter, E_In_Out_Parameter)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("ancestor conversion is the only permitted "
|
||||
& "view conversion", A);
|
||||
else
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("ancestor conversion required", A);
|
||||
end if;
|
||||
|
||||
|
@ -3926,7 +3926,7 @@ package body Sem_Res is
|
|||
end;
|
||||
|
||||
else
|
||||
Check_SPARK_Restriction ("object required", A);
|
||||
Check_SPARK_05_Restriction ("object required", A);
|
||||
end if;
|
||||
|
||||
-- In formal mode, the only view conversions are those
|
||||
|
@ -3935,7 +3935,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("ancestor conversion is the only permitted view "
|
||||
& "conversion", A);
|
||||
end if;
|
||||
|
@ -5238,7 +5238,7 @@ package body Sem_Res is
|
|||
and then
|
||||
not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("operation should be qualified or explicitly converted", N);
|
||||
end if;
|
||||
|
||||
|
@ -5610,7 +5610,7 @@ package body Sem_Res is
|
|||
|
||||
and then Ekind (Nam) /= E_Enumeration_Literal
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("call to subprogram cannot appear before its body", N);
|
||||
end if;
|
||||
|
||||
|
@ -5780,7 +5780,7 @@ package body Sem_Res is
|
|||
if Restriction_Check_Required (SPARK_05)
|
||||
and then Same_Or_Aliased_Subprograms (Nam, Scop)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("subprogram may not contain direct call to itself", N);
|
||||
end if;
|
||||
|
||||
|
@ -6149,7 +6149,7 @@ package body Sem_Res is
|
|||
and then Is_Entity_Name (Name (N))
|
||||
and then Is_Inherited_Operation_For_Type (Entity (Name (N)), Etype (N))
|
||||
then
|
||||
Check_SPARK_Restriction ("function not inherited", N);
|
||||
Check_SPARK_05_Restriction ("function not inherited", N);
|
||||
end if;
|
||||
|
||||
-- Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is
|
||||
|
@ -6462,13 +6462,13 @@ package body Sem_Res is
|
|||
-- types or array types except String.
|
||||
|
||||
if Is_Boolean_Type (T) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("comparison is not defined on Boolean type", N);
|
||||
|
||||
elsif Is_Array_Type (T)
|
||||
and then Base_Type (T) /= Standard_String
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("comparison is not defined on array types other than String", N);
|
||||
end if;
|
||||
|
||||
|
@ -7514,7 +7514,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("array types should have matching static bounds", N);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -8272,7 +8272,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("array types should have matching static bounds", N);
|
||||
end if;
|
||||
end;
|
||||
|
@ -8571,7 +8571,7 @@ package body Sem_Res is
|
|||
end loop;
|
||||
|
||||
if Base_Type (Etype (N)) /= Standard_String then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("result of concatenation should have type String", N);
|
||||
end if;
|
||||
end Resolve_Op_Concat;
|
||||
|
@ -8706,7 +8706,7 @@ package body Sem_Res is
|
|||
|
||||
if Is_Character_Type (Etype (Arg)) then
|
||||
if not Is_OK_Static_Expression (Arg) then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("character operand for concatenation should be static", Arg);
|
||||
end if;
|
||||
|
||||
|
@ -8715,7 +8715,7 @@ package body Sem_Res is
|
|||
and then Is_Constant_Object (Entity (Arg)))
|
||||
and then not Is_OK_Static_Expression (Arg)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("string operand for concatenation should be static", Arg);
|
||||
end if;
|
||||
|
||||
|
@ -9026,7 +9026,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("array types should have matching static bounds", N);
|
||||
end if;
|
||||
|
||||
|
@ -10235,7 +10235,7 @@ package body Sem_Res is
|
|||
and then Operand_Typ /= Any_Composite -- or else Operand in error
|
||||
and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
|
||||
then
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("array types should have matching static bounds", N);
|
||||
end if;
|
||||
|
||||
|
@ -10247,9 +10247,9 @@ package body Sem_Res is
|
|||
and then Is_Tagged_Type (Operand_Typ)
|
||||
and then not Is_Class_Wide_Type (Operand_Typ)
|
||||
and then Is_Ancestor (Target_Typ, Operand_Typ)
|
||||
and then not Is_SPARK_Object_Reference (Operand)
|
||||
and then not Is_SPARK_05_Object_Reference (Operand)
|
||||
then
|
||||
Check_SPARK_Restriction ("object required", Operand);
|
||||
Check_SPARK_05_Restriction ("object required", Operand);
|
||||
end if;
|
||||
|
||||
Analyze_Dimension (N);
|
||||
|
@ -10520,7 +10520,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_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("unary operator not defined for modular type%", N);
|
||||
end if;
|
||||
|
||||
|
|
|
@ -2557,7 +2557,7 @@ package body Sem_Util is
|
|||
end if;
|
||||
else
|
||||
Error_Msg_Sloc := Body_Sloc;
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("decl cannot appear after body#", Decl);
|
||||
end if;
|
||||
end if;
|
||||
|
@ -5426,7 +5426,7 @@ package body Sem_Util is
|
|||
and then Comes_From_Source (C)
|
||||
then
|
||||
Error_Msg_Sloc := Sloc (C);
|
||||
Check_SPARK_Restriction
|
||||
Check_SPARK_05_Restriction
|
||||
("redeclaration of identifier &#", Def_Id);
|
||||
end if;
|
||||
end;
|
||||
|
@ -11459,11 +11459,11 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Is_Selector_Name;
|
||||
|
||||
----------------------------------
|
||||
-- Is_SPARK_Initialization_Expr --
|
||||
----------------------------------
|
||||
-------------------------------------
|
||||
-- Is_SPARK_05_Initialization_Expr --
|
||||
-------------------------------------
|
||||
|
||||
function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean is
|
||||
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean is
|
||||
Is_Ok : Boolean;
|
||||
Expr : Node_Id;
|
||||
Comp_Assn : Node_Id;
|
||||
|
@ -11507,27 +11507,28 @@ package body Sem_Util is
|
|||
|
||||
when N_Qualified_Expression |
|
||||
N_Type_Conversion =>
|
||||
Is_Ok := Is_SPARK_Initialization_Expr (Expression (Orig_N));
|
||||
Is_Ok := Is_SPARK_05_Initialization_Expr (Expression (Orig_N));
|
||||
|
||||
when N_Unary_Op =>
|
||||
Is_Ok := Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
|
||||
Is_Ok := Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N));
|
||||
|
||||
when N_Binary_Op |
|
||||
N_Short_Circuit |
|
||||
N_Membership_Test =>
|
||||
Is_Ok := Is_SPARK_Initialization_Expr (Left_Opnd (Orig_N))
|
||||
Is_Ok := Is_SPARK_05_Initialization_Expr (Left_Opnd (Orig_N))
|
||||
and then
|
||||
Is_SPARK_Initialization_Expr (Right_Opnd (Orig_N));
|
||||
Is_SPARK_05_Initialization_Expr (Right_Opnd (Orig_N));
|
||||
|
||||
when N_Aggregate |
|
||||
N_Extension_Aggregate =>
|
||||
if Nkind (Orig_N) = N_Extension_Aggregate then
|
||||
Is_Ok := Is_SPARK_Initialization_Expr (Ancestor_Part (Orig_N));
|
||||
Is_Ok :=
|
||||
Is_SPARK_05_Initialization_Expr (Ancestor_Part (Orig_N));
|
||||
end if;
|
||||
|
||||
Expr := First (Expressions (Orig_N));
|
||||
while Present (Expr) loop
|
||||
if not Is_SPARK_Initialization_Expr (Expr) then
|
||||
if not Is_SPARK_05_Initialization_Expr (Expr) then
|
||||
Is_Ok := False;
|
||||
goto Done;
|
||||
end if;
|
||||
|
@ -11539,7 +11540,7 @@ package body Sem_Util is
|
|||
while Present (Comp_Assn) loop
|
||||
Expr := Expression (Comp_Assn);
|
||||
if Present (Expr) -- needed for box association
|
||||
and then not Is_SPARK_Initialization_Expr (Expr)
|
||||
and then not Is_SPARK_05_Initialization_Expr (Expr)
|
||||
then
|
||||
Is_Ok := False;
|
||||
goto Done;
|
||||
|
@ -11550,12 +11551,12 @@ package body Sem_Util is
|
|||
|
||||
when N_Attribute_Reference =>
|
||||
if Nkind (Prefix (Orig_N)) in N_Subexpr then
|
||||
Is_Ok := Is_SPARK_Initialization_Expr (Prefix (Orig_N));
|
||||
Is_Ok := Is_SPARK_05_Initialization_Expr (Prefix (Orig_N));
|
||||
end if;
|
||||
|
||||
Expr := First (Expressions (Orig_N));
|
||||
while Present (Expr) loop
|
||||
if not Is_SPARK_Initialization_Expr (Expr) then
|
||||
if not Is_SPARK_05_Initialization_Expr (Expr) then
|
||||
Is_Ok := False;
|
||||
goto Done;
|
||||
end if;
|
||||
|
@ -11575,13 +11576,13 @@ package body Sem_Util is
|
|||
|
||||
<<Done>>
|
||||
return Is_Ok;
|
||||
end Is_SPARK_Initialization_Expr;
|
||||
end Is_SPARK_05_Initialization_Expr;
|
||||
|
||||
-------------------------------
|
||||
-- Is_SPARK_Object_Reference --
|
||||
-------------------------------
|
||||
----------------------------------
|
||||
-- Is_SPARK_05_Object_Reference --
|
||||
----------------------------------
|
||||
|
||||
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean is
|
||||
function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean is
|
||||
begin
|
||||
if Is_Entity_Name (N) then
|
||||
return Present (Entity (N))
|
||||
|
@ -11592,13 +11593,13 @@ package body Sem_Util is
|
|||
else
|
||||
case Nkind (N) is
|
||||
when N_Selected_Component =>
|
||||
return Is_SPARK_Object_Reference (Prefix (N));
|
||||
return Is_SPARK_05_Object_Reference (Prefix (N));
|
||||
|
||||
when others =>
|
||||
return False;
|
||||
end case;
|
||||
end if;
|
||||
end Is_SPARK_Object_Reference;
|
||||
end Is_SPARK_05_Object_Reference;
|
||||
|
||||
------------------
|
||||
-- Is_Statement --
|
||||
|
@ -15116,7 +15117,8 @@ package body Sem_Util is
|
|||
and then (Typ = 't' or else Ekind (Ent) = E_Package)
|
||||
then
|
||||
Error_Msg_Node_1 := Endl;
|
||||
Check_SPARK_Restriction ("`END &` required", Endl, Force => True);
|
||||
Check_SPARK_05_Restriction
|
||||
("`END &` required", Endl, Force => True);
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
|
@ -1312,14 +1312,16 @@ package Sem_Util is
|
|||
-- represent use of the N_Identifier node for a true identifier, when
|
||||
-- normally such nodes represent a direct name.
|
||||
|
||||
function Is_SPARK_Initialization_Expr (N : Node_Id) return Boolean;
|
||||
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
|
||||
-- Determines if the tree referenced by N represents an initialization
|
||||
-- expression in SPARK, suitable for initializing an object in an object
|
||||
-- declaration.
|
||||
-- expression in SPARK 2005, suitable for initializing an object in an
|
||||
-- object declaration.
|
||||
|
||||
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
|
||||
-- Determines if the tree referenced by N represents an object in SPARK.
|
||||
-- This differs from Is_Object_Reference in that ???
|
||||
function Is_SPARK_05_Object_Reference (N : Node_Id) return Boolean;
|
||||
-- Determines if the tree referenced by N represents an object in SPARK
|
||||
-- 2005. This differs from Is_Object_Reference in that only variables,
|
||||
-- constants, formal parameters, and selected_components of those are
|
||||
-- valid objects in SPARK 2005.
|
||||
|
||||
function Is_Statement (N : Node_Id) return Boolean;
|
||||
pragma Inline (Is_Statement);
|
||||
|
|
Loading…
Reference in New Issue