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
to True during analysis of a default component expression.
(Semantics): Save and restore In_Default_Expr around analysis.
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))
null;
else
- Check_SPARK_Restriction
+ Check_SPARK_05_Restriction
("subprogram declaration is not allowed here", N);
end if;
end if;
-- 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
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)
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;
Error_Msg_F (Msg2, N);
end if;
end if;
- end Check_SPARK_Restriction;
+ end Check_SPARK_05_Restriction;
----------------------------------
-- Suppress_Restriction_Message --
-- 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);
-- 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
-- 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.
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
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,
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;
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.
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;
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;
-- 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;
-- 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
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 --
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
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;
when Attribute_Image => Image :
begin
- Check_SPARK_Restriction_On_Attribute;
+ Check_SPARK_05_Restriction_On_Attribute;
Check_Scalar_Type;
Set_Etype (N, Standard_String);
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;
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);
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);
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;
when Attribute_Value => Value :
begin
- Check_SPARK_Restriction_On_Attribute;
+ Check_SPARK_05_Restriction_On_Attribute;
Check_E1;
Check_Scalar_Type;
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;
when Attribute_Wide_Value => Wide_Value :
begin
- Check_SPARK_Restriction_On_Attribute;
+ Check_SPARK_05_Restriction_On_Attribute;
Check_E1;
Check_Scalar_Type;
----------------
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);
-----------
when Attribute_Width =>
- Check_SPARK_Restriction_On_Attribute;
+ Check_SPARK_05_Restriction_On_Attribute;
Check_E0;
Check_Scalar_Type;
Set_Etype (N, Universal_Integer);
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
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);
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
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
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
-- 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.
-- 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
if No (A) then
Error_Msg_N
("missing Import/Export for Link/External name",
- Aspect);
+ Aspect);
end if;
end;
end Analyze_Aspect_External_Or_Link_Name;
-- 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);
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)))
-- 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
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
(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
-- 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);
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;
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))));
-- 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
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));
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;
-- 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
-- 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;
-- 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;
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;
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.
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;
-- 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;
-- 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
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
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;
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);
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
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
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);
-- 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);
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;
-- 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;
-- 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
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
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);
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
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);
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;
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;
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
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;
-- 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
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);
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;
-- 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
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);
-- 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
-- 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;
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;
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;
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
-- 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;
-- 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));
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)));
(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:
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
-- 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;
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;
-- 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;
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);
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
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;
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
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);
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);
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);
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);
-- 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);
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;
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;
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
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
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.
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);
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
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);
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);
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));
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))
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);
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
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));
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
-- 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
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
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;
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
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;
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;
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;
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;
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
-- 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;
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;
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;
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;
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;
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;
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;
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;
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);
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;
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;
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;
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;
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;
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;
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;
<<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))
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 --
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;
-- 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.
-
- 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 ???
+ -- expression in SPARK 2005, suitable for initializing an object in an
+ -- object declaration.
+
+ 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);
projects / platform / upstream / linaro-gcc.git / commitdiff