-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
(Related_Nod : Node_Id;
N : Node_Id) return Entity_Id
is
- Loc : constant Source_Ptr := Sloc (Related_Nod);
Anon_Type : Entity_Id;
Anon_Scope : Entity_Id;
Desig_Type : Entity_Id;
- Decl : Entity_Id;
Enclosing_Prot_Type : Entity_Id := Empty;
begin
- Check_Formal_Restriction ("access type is not allowed", N);
+ Check_SPARK_Restriction ("access type is not allowed", N);
if Is_Entry (Current_Scope)
and then Is_Task_Type (Etype (Scope (Current_Scope)))
Anon_Scope := Scope (Defining_Entity (Related_Nod));
end if;
- else
- -- For access formals, access components, and access discriminants,
- -- the scope is that of the enclosing declaration,
+ -- For an access type definition, if the current scope is a child
+ -- unit it is the scope of the type.
+
+ elsif Is_Compilation_Unit (Current_Scope) then
+ Anon_Scope := Current_Scope;
+
+ -- For access formals, access components, and access discriminants, the
+ -- scope is that of the enclosing declaration,
+ else
Anon_Scope := Scope (Current_Scope);
end if;
Anon_Type :=
Create_Itype
- (E_Anonymous_Access_Type, Related_Nod, Scope_Id => Anon_Scope);
+ (E_Anonymous_Access_Type, Related_Nod, Scope_Id => Anon_Scope);
if All_Present (N)
and then Ada_Version >= Ada_2005
-- the corresponding semantic routine
if Present (Access_To_Subprogram_Definition (N)) then
+
+ -- Compiler runtime units are compiled in Ada 2005 mode when building
+ -- the runtime library but must also be compilable in Ada 95 mode
+ -- (when bootstrapping the compiler).
+
+ Check_Compiler_Unit (N);
+
Access_Subprogram_Declaration
(T_Name => Anon_Type,
T_Def => Access_To_Subprogram_Definition (N));
Set_Can_Use_Internal_Rep
(Anon_Type, not Always_Compatible_Rep_On_Target);
- -- If the anonymous access is associated with a protected operation
+ -- If the anonymous access is associated with a protected operation,
-- create a reference to it after the enclosing protected definition
-- because the itype will be used in the subsequent bodies.
-- proper Master for the created tasks.
if Nkind (Related_Nod) = N_Object_Declaration
- and then Expander_Active
+ and then Expander_Active
then
if Is_Interface (Desig_Type)
and then Is_Limited_Record (Desig_Type)
elsif Has_Task (Desig_Type)
and then Comes_From_Source (Related_Nod)
- and then not Restriction_Active (No_Task_Hierarchy)
then
- if not Has_Master_Entity (Current_Scope) then
- Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier =>
- Make_Defining_Identifier (Loc, Name_uMaster),
- Constant_Present => True,
- Object_Definition =>
- New_Reference_To (RTE (RE_Master_Id), Loc),
- Expression =>
- Make_Explicit_Dereference (Loc,
- New_Reference_To (RTE (RE_Current_Master), Loc)));
-
- Insert_Before (Related_Nod, Decl);
- Analyze (Decl);
-
- Set_Master_Id (Anon_Type, Defining_Identifier (Decl));
- Set_Has_Master_Entity (Current_Scope);
- else
- Build_Master_Renaming (Related_Nod, Anon_Type);
- end if;
+ Build_Master_Entity (Defining_Identifier (Related_Nod));
+ Build_Master_Renaming (Anon_Type);
end if;
end if;
-- Start of processing for Access_Subprogram_Declaration
begin
- Check_Formal_Restriction ("access type is not allowed", T_Def);
+ Check_SPARK_Restriction ("access type is not allowed", T_Def);
-- Associate the Itype node with the inner full-type declaration or
-- subprogram spec or entry body. This is required to handle nested
----------------------------
procedure Access_Type_Declaration (T : Entity_Id; Def : Node_Id) is
- S : constant Node_Id := Subtype_Indication (Def);
P : constant Node_Id := Parent (Def);
+ S : constant Node_Id := Subtype_Indication (Def);
+
+ Full_Desig : Entity_Id;
+
begin
- Check_Formal_Restriction ("access type is not allowed", Def);
+ Check_SPARK_Restriction ("access type is not allowed", Def);
-- Check for permissible use of incomplete type
Set_Ekind (T, E_Access_Type);
end if;
- if Base_Type (Designated_Type (T)) = T then
+ Full_Desig := Designated_Type (T);
+
+ if Base_Type (Full_Desig) = T then
Error_Msg_N ("access type cannot designate itself", S);
-- In Ada 2005, the type may have a limited view through some unit
-- in its own context, allowing the following circularity that cannot
-- be detected earlier
- elsif Is_Class_Wide_Type (Designated_Type (T))
- and then Etype (Designated_Type (T)) = T
+ elsif Is_Class_Wide_Type (Full_Desig)
+ and then Etype (Full_Desig) = T
then
Error_Msg_N
("access type cannot designate its own classwide type", S);
Set_Has_Task (T, False);
Set_Has_Controlled_Component (T, False);
- -- Initialize Associated_Final_Chain explicitly to Empty, to avoid
+ -- Initialize field Finalization_Master explicitly to Empty, to avoid
-- problems where an incomplete view of this entity has been previously
-- established by a limited with and an overlaid version of this field
-- (Stored_Constraint) was initialized for the incomplete view.
- Set_Associated_Final_Chain (T, Empty);
+ -- This reset is performed in most cases except where the access type
+ -- has been created for the purposes of allocating or deallocating a
+ -- build-in-place object. Such access types have explicitly set pools
+ -- and finalization masters.
+
+ if No (Associated_Storage_Pool (T)) then
+ Set_Finalization_Master (T, Empty);
+ end if;
-- Ada 2005 (AI-231): Propagate the null-excluding and access-constant
-- attributes
(Tagged_Type => Tagged_Type,
Iface_Prim => Iface_Prim);
+ if No (Prim) and then Serious_Errors_Detected > 0 then
+ goto Continue;
+ end if;
+
pragma Assert (Present (Prim));
-- Ada 2012 (AI05-0197): If the name of the covering primitive
Set_Has_Delayed_Freeze (New_Subp);
end if;
+ <<Continue>>
Next_Elmt (Elmt);
end loop;
(Subtype_Indication (Component_Definition (N)), N);
if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
- Check_Formal_Restriction ("subtype mark required", Typ);
+ Check_SPARK_Restriction ("subtype mark required", Typ);
end if;
-- Ada 2005 (AI-230): Access Definition case
-- package Sem).
if Present (E) then
- Check_Formal_Restriction ("default expression is not allowed", E);
+ Check_SPARK_Restriction ("default expression is not allowed", E);
Preanalyze_Spec_Expression (E, T);
Check_Initialization (T, E);
-- Start of processing for Analyze_Declarations
begin
- if SPARK_Mode or else Restriction_Check_Required (SPARK) then
+ if Restriction_Check_Required (SPARK) then
Check_Later_Vs_Basic_Declarations (L, During_Parsing => False);
end if;
D := First (L);
while Present (D) loop
- -- Package specification cannot contain a package declaration in
- -- SPARK or ALFA.
+ -- Package spec cannot contain a package declaration in SPARK
if Nkind (D) = N_Package_Declaration
and then Nkind (Parent (L)) = N_Package_Specification
then
- Check_Formal_Restriction ("package specification cannot contain "
- & "a package declaration", D);
+ Check_SPARK_Restriction
+ ("package specification cannot contain a package declaration",
+ D);
end if;
-- Complete analysis of declaration
if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
Spec := Specification (Original_Node (Decl));
Sent := Defining_Unit_Name (Spec);
- Prag := Spec_PPC_List (Sent);
+
+ Prag := Spec_PPC_List (Contract (Sent));
while Present (Prag) loop
Analyze_PPC_In_Decl_Part (Prag, Sent);
Prag := Next_Pragma (Prag);
end loop;
+
+ Check_Subprogram_Contract (Sent);
+
+ Prag := Spec_TC_List (Contract (Sent));
+ while Present (Prag) loop
+ Analyze_TC_In_Decl_Part (Prag, Sent);
+ Prag := Next_Pragma (Prag);
+ end loop;
end if;
Next (Decl);
null;
-- For record types, discriminants are allowed, unless we are in
- -- SPARK or ALFA.
+ -- SPARK.
when N_Record_Definition =>
if Present (Discriminant_Specifications (N)) then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("discriminant type is not allowed",
Defining_Identifier
(First (Discriminant_Specifications (N))));
return;
end if;
- -- Controlled type is not allowed in SPARK and ALFA
+ -- Controlled type is not allowed in SPARK
if Is_Visibly_Controlled (T) then
- Check_Formal_Restriction ("controlled type is not allowed", N);
+ Check_SPARK_Restriction ("controlled type is not allowed", N);
end if;
-- Some common processing for all types
Set_Optimize_Alignment_Flags (Def_Id);
Check_Eliminated (Def_Id);
+ -- If the declaration is a completion and aspects are present, apply
+ -- them to the entity for the type which is currently the partial
+ -- view, but which is the one that will be frozen.
+
if Has_Aspects (N) then
- Analyze_Aspect_Specifications (N, Def_Id);
+ if Prev /= Def_Id then
+ Analyze_Aspect_Specifications (N, Prev);
+ else
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
end if;
end Analyze_Full_Type_Declaration;
T : Entity_Id;
begin
- Check_Formal_Restriction ("incomplete type is not allowed", N);
+ Check_SPARK_Restriction ("incomplete type is not allowed", N);
Generate_Definition (Defining_Identifier (N));
-- subtypes will be built after the full view of the type.
Set_Private_Dependents (T, New_Elmt_List);
- Set_Is_Pure (T, F);
+ Set_Is_Pure (T, F);
end Analyze_Incomplete_Type_Decl;
-----------------------------------
-- 2. Those generated by the Expression
- -- 3. Those used to constrained the Object Definition with the
- -- expression constraints when it is unconstrained
+ -- 3. Those used to constrain the Object Definition with the
+ -- expression constraints when the definition is unconstrained.
-- They must be generated in this order to avoid order of elaboration
-- issues. Thus the first step (after entering the name) is to analyze
if Present (Prev_Entity)
and then
+
-- If the homograph is an implicit subprogram, it is overridden
-- by the current declaration.
-- is considered, so that the Object_Definition node is still the same
-- as in source code.
- -- In SPARK or ALFA, the nominal subtype shall be given by a subtype
- -- mark and shall not be unconstrained. (The only exception to this
- -- is the admission of declarations of constants of type String.)
+ -- In SPARK, the nominal subtype shall be given by a subtype mark and
+ -- shall not be unconstrained. (The only exception to this is the
+ -- admission of declarations of constants of type String.)
if not
Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("subtype mark required", Object_Definition (N));
elsif Is_Array_Type (T)
and then not Is_Constrained (T)
and then T /= Standard_String
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("subtype mark of constrained type expected",
Object_Definition (N));
end if;
- -- There are no aliased objects in SPARK or ALFA
+ -- There are no aliased objects in SPARK
if Aliased_Present (N) then
- Check_Formal_Restriction ("aliased object is not allowed", N);
+ Check_SPARK_Restriction ("aliased object is not allowed", N);
end if;
-- Process initialization expression if present and not in error
-- Only call test if needed
- and then (Formal_Verification_Mode
- or else Restriction_Check_Required (SPARK))
+ and then Restriction_Check_Required (SPARK)
and then not Is_SPARK_Initialization_Expr (E)
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("initialization expression is not appropriate", E);
end if;
end if;
if Is_Indefinite_Subtype (T) then
+ -- In SPARK, a declaration of unconstrained type is allowed
+ -- only for constants of type string.
+
+ if Is_String_Type (T) and then not Constant_Present (N) then
+ Check_SPARK_Restriction
+ ("declaration of object of unconstrained type not allowed",
+ N);
+ end if;
+
-- Nothing to do in deferred constant case
if Constant_Present (N) and then No (E) then
-- Case of initialization present
else
- -- Not allowed in Ada 83
+ -- Check restrictions in Ada 83
if not Constant_Present (N) then
+
+ -- Unconstrained variables not allowed in Ada 83 mode
+
if Ada_Version = Ada_83
and then Comes_From_Source (Object_Definition (N))
then
-- It is unclear why this should make it acceptable to gcc. ???
Remove_Side_Effects (E);
+
+ -- If this is a constant declaration of an unconstrained type and
+ -- the initialization is an aggregate, we can use the subtype of the
+ -- aggregate for the declared entity because it is immutable.
+
+ elsif not Is_Constrained (T)
+ and then Has_Discriminants (T)
+ and then Constant_Present (N)
+ and then not Has_Unchecked_Union (T)
+ and then Nkind (E) = N_Aggregate
+ then
+ Act_T := Etype (E);
end if;
-- Check No_Wide_Characters restriction
Check_Wide_Character_Restriction (T, Object_Definition (N));
- -- Indicate this is not set in source. Certainly true for constants,
- -- and true for variables so far (will be reset for a variable if and
- -- when we encounter a modification in the source).
+ -- Indicate this is not set in source. Certainly true for constants, and
+ -- true for variables so far (will be reset for a variable if and when
+ -- we encounter a modification in the source).
Set_Never_Set_In_Source (Id, True);
Set_Ekind (Id, E_Variable);
-- A variable is set as shared passive if it appears in a shared
- -- passive package, and is at the outer level. This is not done
- -- for entities generated during expansion, because those are
- -- always manipulated locally.
+ -- passive package, and is at the outer level. This is not done for
+ -- entities generated during expansion, because those are always
+ -- manipulated locally.
if Is_Shared_Passive (Current_Scope)
and then Is_Library_Level_Entity (Id)
if Skip
or else (Present (Etype (Id))
- and then (Is_Private_Type (Etype (Id))
- or else Is_Task_Type (Etype (Id))
- or else Is_Rewrite_Substitution (N)))
+ and then (Is_Private_Type (Etype (Id))
+ or else Is_Task_Type (Etype (Id))
+ or else Is_Rewrite_Substitution (N)))
then
null;
if Has_Predicates (T)
or else (Present (Ancestor_Subtype (T))
- and then Has_Predicates (Ancestor_Subtype (T)))
+ and then Has_Predicates (Ancestor_Subtype (T)))
then
Set_Has_Predicates (Id);
Set_Has_Delayed_Freeze (Id);
end if;
- -- Subtype of Boolean cannot have a constraint in SPARK or ALFA
+ -- Subtype of Boolean cannot have a constraint in SPARK
if Is_Boolean_Type (T)
and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("subtype of Boolean cannot have constraint", N);
end if;
One_Cstr := First (Constraints (Cstr));
while Present (One_Cstr) loop
- -- Index or discriminant constraint in SPARK or ALFA must be
- -- a subtype mark.
+ -- Index or discriminant constraint in SPARK must be a
+ -- subtype mark.
if not
Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("subtype mark required", One_Cstr);
-- String subtype must have a lower bound of 1 in SPARK.
if Is_OK_Static_Expression (Low)
and then Expr_Value (Low) /= 1
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("String subtype must have lower bound of 1", N);
end if;
end if;
Set_Etype (Id, Base_Type (T));
-- Subtype of unconstrained array without constraint is not allowed
- -- in SPARK or ALFA.
+ -- in SPARK.
if Is_Array_Type (T)
and then not Is_Constrained (T)
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("subtype of unconstrained array must have constraint", N);
end if;
Set_Has_Discriminants (Id, Has_Discriminants (T));
Set_Is_Constrained (Id, Is_Constrained (T));
Set_Is_Limited_Record (Id, Is_Limited_Record (T));
+ Set_Has_Implicit_Dereference
+ (Id, Has_Implicit_Dereference (T));
Set_Has_Unknown_Discriminants
(Id, Has_Unknown_Discriminants (T));
end if;
when Private_Kind =>
- Set_Ekind (Id, Subtype_Kind (Ekind (T)));
- Set_Has_Discriminants (Id, Has_Discriminants (T));
- Set_Is_Constrained (Id, Is_Constrained (T));
- Set_First_Entity (Id, First_Entity (T));
- Set_Last_Entity (Id, Last_Entity (T));
+ Set_Ekind (Id, Subtype_Kind (Ekind (T)));
+ Set_Has_Discriminants (Id, Has_Discriminants (T));
+ Set_Is_Constrained (Id, Is_Constrained (T));
+ Set_First_Entity (Id, First_Entity (T));
+ Set_Last_Entity (Id, Last_Entity (T));
Set_Private_Dependents (Id, New_Elmt_List);
- Set_Is_Limited_Record (Id, Is_Limited_Record (T));
+ Set_Is_Limited_Record (Id, Is_Limited_Record (T));
+ Set_Has_Implicit_Dereference
+ (Id, Has_Implicit_Dereference (T));
Set_Has_Unknown_Discriminants
- (Id, Has_Unknown_Discriminants (T));
+ (Id, Has_Unknown_Discriminants (T));
Set_Known_To_Have_Preelab_Init
(Id, Known_To_Have_Preelab_Init (T));
if Is_Tagged_Type (T) then
Set_Is_Tagged_Type (Id);
Set_Is_Abstract_Type (Id, Is_Abstract_Type (T));
- Set_Class_Wide_Type (Id, Class_Wide_Type (T));
+ Set_Class_Wide_Type (Id, Class_Wide_Type (T));
Set_Direct_Primitive_Operations (Id,
Direct_Primitive_Operations (T));
end if;
if Has_Discriminants (T) then
Set_Discriminant_Constraint
- (Id, Discriminant_Constraint (T));
+ (Id, Discriminant_Constraint (T));
Set_Stored_Constraint_From_Discriminant_Constraint (Id);
elsif Present (Full_View (T))
and then Has_Discriminants (Full_View (T))
then
Set_Discriminant_Constraint
- (Id, Discriminant_Constraint (Full_View (T)));
+ (Id, Discriminant_Constraint (Full_View (T)));
Set_Stored_Constraint_From_Discriminant_Constraint (Id);
-- This would seem semantically correct, but apparently
Conditional_Delay (Id, T);
end if;
- -- Check that constraint_error is raised for a scalar subtype
- -- indication when the lower or upper bound of a non-null range
- -- lies outside the range of the type mark.
+ -- Check that Constraint_Error is raised for a scalar subtype indication
+ -- when the lower or upper bound of a non-null range lies outside the
+ -- range of the type mark.
if Nkind (Subtype_Indication (N)) = N_Subtype_Indication then
if Is_Scalar_Type (Etype (Id))
(Scalar_Range (Id),
Etype (Subtype_Mark (Subtype_Indication (N))));
+ -- In the array case, check compatibility for each index
+
elsif Is_Array_Type (Etype (Id))
and then Present (First_Index (Id))
then
-- This really should be a subprogram that finds the indications
-- to check???
- if ((Nkind (First_Index (Id)) = N_Identifier
- and then Ekind (Entity (First_Index (Id))) in Scalar_Kind)
- or else Nkind (First_Index (Id)) = N_Subtype_Indication)
- and then
- Nkind (Scalar_Range (Etype (First_Index (Id)))) = N_Range
- then
- declare
- Target_Typ : constant Entity_Id :=
- Etype
- (First_Index (Etype
- (Subtype_Mark (Subtype_Indication (N)))));
- begin
- R_Checks :=
- Get_Range_Checks
- (Scalar_Range (Etype (First_Index (Id))),
- Target_Typ,
- Etype (First_Index (Id)),
- Defining_Identifier (N));
-
- Insert_Range_Checks
- (R_Checks,
- N,
- Target_Typ,
- Sloc (Defining_Identifier (N)));
- end;
- end if;
+ declare
+ Subt_Index : Node_Id := First_Index (Id);
+ Target_Index : Node_Id :=
+ First_Index (Etype
+ (Subtype_Mark (Subtype_Indication (N))));
+ Has_Dyn_Chk : Boolean := Has_Dynamic_Range_Check (N);
+
+ begin
+ while Present (Subt_Index) loop
+ if ((Nkind (Subt_Index) = N_Identifier
+ and then Ekind (Entity (Subt_Index)) in Scalar_Kind)
+ or else Nkind (Subt_Index) = N_Subtype_Indication)
+ and then
+ Nkind (Scalar_Range (Etype (Subt_Index))) = N_Range
+ then
+ declare
+ Target_Typ : constant Entity_Id :=
+ Etype (Target_Index);
+ begin
+ R_Checks :=
+ Get_Range_Checks
+ (Scalar_Range (Etype (Subt_Index)),
+ Target_Typ,
+ Etype (Subt_Index),
+ Defining_Identifier (N));
+
+ -- Reset Has_Dynamic_Range_Check on the subtype to
+ -- prevent elision of the index check due to a dynamic
+ -- check generated for a preceding index (needed since
+ -- Insert_Range_Checks tries to avoid generating
+ -- redundant checks on a given declaration).
+
+ Set_Has_Dynamic_Range_Check (N, False);
+
+ Insert_Range_Checks
+ (R_Checks,
+ N,
+ Target_Typ,
+ Sloc (Defining_Identifier (N)));
+
+ -- Record whether this index involved a dynamic check
+
+ Has_Dyn_Chk :=
+ Has_Dyn_Chk or else Has_Dynamic_Range_Check (N);
+ end;
+ end if;
+
+ Next_Index (Subt_Index);
+ Next_Index (Target_Index);
+ end loop;
+
+ -- Finally, mark whether the subtype involves dynamic checks
+
+ Set_Has_Dynamic_Range_Check (N, Has_Dyn_Chk);
+ end;
end if;
end if;
Analyze (Index);
if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
- Check_Formal_Restriction ("subtype mark required", Index);
+ Check_SPARK_Restriction ("subtype mark required", Index);
end if;
-- Add a subtype declaration for each index of private array type
if Present (Component_Typ) then
Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+ Set_Etype (Component_Typ, Element_Type);
+
if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
- Check_Formal_Restriction ("subtype mark required", Component_Typ);
+ Check_SPARK_Restriction ("subtype mark required", Component_Typ);
end if;
-- Ada 2005 (AI-230): Access Definition case
Set_Packed_Array_Type (T, Empty);
if Aliased_Present (Component_Definition (Def)) then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("aliased is not allowed", Component_Definition (Def));
Set_Has_Aliased_Components (Etype (T));
end if;
Derived_Type : Entity_Id;
Derive_Subps : Boolean := True)
is
- Loc : constant Source_Ptr := Sloc (N);
- Parent_Base : Entity_Id;
- Type_Def : Node_Id;
- Indic : Node_Id;
- Discrim : Entity_Id;
- Last_Discrim : Entity_Id;
- Constrs : Elist_Id;
-
- Discs : Elist_Id := New_Elmt_List;
- -- An empty Discs list means that there were no constraints in the
- -- subtype indication or that there was an error processing it.
-
- Assoc_List : Elist_Id;
- New_Discrs : Elist_Id;
- New_Base : Entity_Id;
- New_Decl : Node_Id;
- New_Indic : Node_Id;
-
- Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type);
Discriminant_Specs : constant Boolean :=
Present (Discriminant_Specifications (N));
+ Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type);
+ Loc : constant Source_Ptr := Sloc (N);
Private_Extension : constant Boolean :=
Nkind (N) = N_Private_Extension_Declaration;
-
+ Assoc_List : Elist_Id;
Constraint_Present : Boolean;
+ Constrs : Elist_Id;
+ Discrim : Entity_Id;
+ Indic : Node_Id;
Inherit_Discrims : Boolean := False;
+ Last_Discrim : Entity_Id;
+ New_Base : Entity_Id;
+ New_Decl : Node_Id;
+ New_Discrs : Elist_Id;
+ New_Indic : Node_Id;
+ Parent_Base : Entity_Id;
Save_Etype : Entity_Id;
Save_Discr_Constr : Elist_Id;
Save_Next_Entity : Entity_Id;
+ Type_Def : Node_Id;
+
+ Discs : Elist_Id := New_Elmt_List;
+ -- An empty Discs list means that there were no constraints in the
+ -- subtype indication or that there was an error processing it.
begin
if Ekind (Parent_Type) = E_Record_Type_With_Private
Parent_Base := Base_Type (Parent_Type);
end if;
+ -- AI05-0115 : if this is a derivation from a private type in some
+ -- other scope that may lead to invisible components for the derived
+ -- type, mark it accordingly.
+
+ if Is_Private_Type (Parent_Type) then
+ if Scope (Parent_Type) = Scope (Derived_Type) then
+ null;
+
+ elsif In_Open_Scopes (Scope (Parent_Type))
+ and then In_Private_Part (Scope (Parent_Type))
+ then
+ null;
+
+ else
+ Set_Has_Private_Ancestor (Derived_Type);
+ end if;
+
+ else
+ Set_Has_Private_Ancestor
+ (Derived_Type, Has_Private_Ancestor (Parent_Type));
+ end if;
+
-- Before we start the previously documented transformations, here is
-- little fix for size and alignment of tagged types. Normally when we
-- derive type D from type P, we copy the size and alignment of P as the
Analyze (N);
-- Derivation of subprograms must be delayed until the full subtype
- -- has been established to ensure proper overriding of subprograms
+ -- has been established, to ensure proper overriding of subprograms
-- inherited by full types. If the derivations occurred as part of
-- the call to Build_Derived_Type above, then the check for type
-- conformance would fail because earlier primitive subprograms
-- could still refer to the full type prior the change to the new
-- subtype and hence would not match the new base type created here.
+ -- Subprograms are not derived, however, when Derive_Subps is False
+ -- (since otherwise there could be redundant derivations).
- Derive_Subprograms (Parent_Type, Derived_Type);
+ if Derive_Subps then
+ Derive_Subprograms (Parent_Type, Derived_Type);
+ end if;
-- For tagged types the Discriminant_Constraint of the new base itype
-- is inherited from the first subtype so that no subtype conformance
Set_Stored_Constraint
(Derived_Type, Expand_To_Stored_Constraint (Parent_Type, Discs));
Replace_Components (Derived_Type, New_Decl);
+ Set_Has_Implicit_Dereference
+ (Derived_Type, Has_Implicit_Dereference (Parent_Type));
end if;
-- Insert the new derived type declaration
Set_Last_Entity
(Class_Wide_Type (Derived_Type), Last_Entity (Derived_Type));
end if;
-
- -- Update the scope of anonymous access types of discriminants and other
- -- components, to prevent scope anomalies in gigi, when the derivation
- -- appears in a scope nested within that of the parent.
-
- declare
- D : Entity_Id;
-
- begin
- D := First_Entity (Derived_Type);
- while Present (D) loop
- if Ekind_In (D, E_Discriminant, E_Component) then
- if Is_Itype (Etype (D))
- and then Ekind (Etype (D)) = E_Anonymous_Access_Type
- then
- Set_Scope (Etype (D), Current_Scope);
- end if;
- end if;
-
- Next_Entity (D);
- end loop;
- end;
end Build_Derived_Record_Type;
------------------------
begin
-- Set common attributes
- Set_Scope (Derived_Type, Current_Scope);
+ Set_Scope (Derived_Type, Current_Scope);
- Set_Ekind (Derived_Type, Ekind (Parent_Base));
- Set_Etype (Derived_Type, Parent_Base);
- Set_Has_Task (Derived_Type, Has_Task (Parent_Base));
+ Set_Ekind (Derived_Type, Ekind (Parent_Base));
+ Set_Etype (Derived_Type, Parent_Base);
+ Set_Has_Task (Derived_Type, Has_Task (Parent_Base));
Set_Size_Info (Derived_Type, Parent_Type);
Set_RM_Size (Derived_Type, RM_Size (Parent_Type));
-- the point of instantiation, we want to find the discriminant
-- that corresponds to D in Rec, i.e. X.
- if Present (Original_Discriminant (Id)) then
+ if Present (Original_Discriminant (Id))
+ and then In_Instance
+ then
Discr := Find_Corresponding_Discriminant (Id, T);
Found := True;
Error_Msg_N ("& does not match any discriminant", Id);
return New_Elmt_List;
- -- The following is only useful for the benefit of generic
- -- instances but it does not interfere with other
- -- processing for the non-generic case so we do it in all
- -- cases (for generics this statement is executed when
- -- processing the generic definition, see comment at the
- -- beginning of this if statement).
+ -- If the parent type is a generic formal, preserve the
+ -- name of the discriminant for subsequent instances.
+ -- see comment at the beginning of this if statement.
- else
+ elsif Is_Generic_Type (Root_Type (T)) then
Set_Original_Discriminant (Id, Discr);
end if;
end if;
Set_First_Entity (Def_Id, First_Entity (T));
Set_Last_Entity (Def_Id, Last_Entity (T));
+ Set_Has_Implicit_Dereference
+ (Def_Id, Has_Implicit_Dereference (T));
-- If the subtype is the completion of a private declaration, there may
-- have been representation clauses for the partial view, and they must
end if;
if Is_Tagged_Type (T) then
- Set_Is_Tagged_Type (Def_Id);
+ Set_Is_Tagged_Type (Def_Id);
Make_Class_Wide_Type (Def_Id);
end if;
is
IR : constant Node_Id := Make_Itype_Reference (Sloc (Nod));
begin
- Set_Itype (IR, Ityp);
- Insert_After (Nod, IR);
+
+ -- Itype references are only created for use by the back-end
+
+ if Inside_A_Generic then
+ return;
+ else
+ Set_Itype (IR, Ityp);
+ Insert_After (Nod, IR);
+ end if;
end Build_Itype_Reference;
------------------------
-- The partial view of T may have been a private extension, for
-- which inherited functions dispatching on result are abstract.
-- If the full view is a null extension, there is no need for
- -- overriding in Ada2005, but wrappers need to be built for them
+ -- overriding in Ada 2005, but wrappers need to be built for them
-- (see exp_ch3, Build_Controlling_Function_Wrappers).
if Is_Null_Extension (T)
begin
E := Subp;
while Present (Alias (E)) loop
- Error_Msg_Sloc := Sloc (E);
- Error_Msg_NE
- ("\& has been inherited #", T, Subp);
+
+ -- Avoid reporting redundant errors on entities
+ -- inherited from interfaces
+
+ if Sloc (E) /= Sloc (T) then
+ Error_Msg_Sloc := Sloc (E);
+ Error_Msg_NE
+ ("\& has been inherited #", T, Subp);
+ end if;
+
E := Alias (E);
end loop;
Error_Msg_Sloc := Sloc (E);
- Error_Msg_NE
- ("\& has been inherited from subprogram #",
- T, Subp);
+
+ -- AI05-0068: report if there is an overriding
+ -- non-abstract subprogram that is invisible.
+
+ if Is_Hidden (E)
+ and then not Is_Abstract_Subprogram (E)
+ then
+ Error_Msg_NE
+ ("\& subprogram# is not visible",
+ T, Subp);
+
+ else
+ Error_Msg_NE
+ ("\& has been inherited from subprogram #",
+ T, Subp);
+ end if;
end;
end if;
end if;
-- The controlling formal of Subp must be of mode "out",
-- "in out" or an access-to-variable to be overridden.
- -- Error message below needs rewording (remember comma
- -- in -gnatj mode) ???
-
if Ekind (First_Formal (Subp)) = E_In_Parameter
and then Ekind (Subp) /= E_Function
then
- if not Is_Predefined_Dispatching_Operation (Subp) then
- Error_Msg_NE
- ("first formal of & must be of mode `OUT`, " &
- "`IN OUT` or access-to-variable", T, Subp);
- Error_Msg_N
- ("\to be overridden by protected procedure or " &
- "entry (RM 9.4(11.9/2))", T);
+ if not Is_Predefined_Dispatching_Operation (Subp)
+ and then Is_Protected_Type
+ (Corresponding_Concurrent_Type (T))
+ then
+ Error_Msg_PT (T, Subp);
end if;
-- Some other kind of overriding failure
-- type, so we must be sure not to overwrite these entries.
declare
+ Append : Boolean;
Item : Node_Id;
Next_Item : Node_Id;
-- is not done, as that would create a circularity.
elsif Item /= First_Rep_Item (Priv) then
+ Append := True;
+
loop
Next_Item := Next_Rep_Item (Item);
exit when No (Next_Item);
Item := Next_Item;
+
+ -- If the private view has aspect specifications, the full view
+ -- inherits them. Since these aspects may already have been
+ -- attached to the full view during derivation, do not append
+ -- them if already present.
+
+ if Item = First_Rep_Item (Priv) then
+ Append := False;
+ exit;
+ end if;
end loop;
-- And link the private type items at the end of the chain
- Set_Next_Rep_Item (Item, First_Rep_Item (Priv));
+ if Append then
+ Set_Next_Rep_Item (Item, First_Rep_Item (Priv));
+ end if;
end if;
end;
Related_Id : Entity_Id;
Suffix : Character)
is
- T_Ent : Entity_Id := Entity (Subtype_Mark (SI));
+ -- Retrieve Base_Type to ensure getting to the concurrent type in the
+ -- case of a private subtype (needed when only doing semantic analysis).
+
+ T_Ent : Entity_Id := Base_Type (Entity (Subtype_Mark (SI)));
T_Val : Entity_Id;
begin
else
pragma Assert (Nkind (C) = N_Digits_Constraint);
- Check_Formal_Restriction ("digits constraint is not allowed", S);
+ Check_SPARK_Restriction ("digits constraint is not allowed", S);
Digits_Expr := Digits_Expression (C);
Analyze_And_Resolve (Digits_Expr, Any_Integer);
if Nkind (C) = N_Digits_Constraint then
- Check_Formal_Restriction ("digits constraint is not allowed", S);
+ Check_SPARK_Restriction ("digits constraint is not allowed", S);
Check_Restriction (No_Obsolescent_Features, C);
if Warn_On_Obsolescent_Feature then
if Nkind (C) = N_Delta_Constraint then
- Check_Formal_Restriction ("delta constraint is not allowed", S);
+ Check_SPARK_Restriction ("delta constraint is not allowed", S);
Check_Restriction (No_Obsolescent_Features, C);
if Warn_On_Obsolescent_Feature then
Next_Discriminant (Old_C);
end loop;
- -- The tag, and the possible parent and controller components
- -- are unconditionally in the subtype.
+ -- The tag and the possible parent component are unconditionally in
+ -- the subtype.
if Is_Tagged_Type (Typ)
or else Has_Controlled_Component (Typ)
while Present (Old_C) loop
if Chars ((Old_C)) = Name_uTag
or else Chars ((Old_C)) = Name_uParent
- or else Chars ((Old_C)) = Name_uController
then
Append_Elmt (Old_C, Comp_List);
end if;
if Original_Record_Component (Old_C) = Old_C
and then Chars (Old_C) /= Name_uTag
and then Chars (Old_C) /= Name_uParent
- and then Chars (Old_C) /= Name_uController
then
Append_Elmt (Old_C, Comp_List);
end if;
Bound_Val : Ureal;
begin
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("decimal fixed point type is not allowed", Def);
Check_Restriction (No_Fixed_Point, Def);
New_Subp :=
New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type));
Set_Ekind (New_Subp, Ekind (Parent_Subp));
+ Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp)));
-- Check whether the inherited subprogram is a private operation that
-- should be inherited but not yet made visible. Such subprograms can
Type_Conformant (Subp, Act_Subp,
Skip_Controlling_Formals => True)))
then
- pragma Assert (not Is_Ancestor (Parent_Base, Generic_Actual));
+ pragma Assert (not Is_Ancestor (Parent_Base, Generic_Actual,
+ Use_Full_View => True));
-- Remember that we need searching for all pending primitives
-- parent is also an interface.
if Interface_Present (Def) then
- Check_Formal_Restriction ("interface is not allowed", Def);
+ Check_SPARK_Restriction ("interface is not allowed", Def);
if not Is_Interface (Parent_Type) then
Diagnose_Interface (Indic, Parent_Type);
end if;
-- Only composite types other than array types are allowed to have
- -- discriminants. In SPARK and in ALFA, no types are allowed to have
- -- discriminants.
+ -- discriminants. In SPARK, no types are allowed to have discriminants.
if Present (Discriminant_Specifications (N)) then
if (Is_Elementary_Type (Parent_Type)
Defining_Identifier (First (Discriminant_Specifications (N))));
Set_Has_Discriminants (T, False);
else
- Check_Formal_Restriction ("discriminant type is not allowed", N);
+ Check_SPARK_Restriction ("discriminant type is not allowed", N);
end if;
end if;
end if;
end if;
- -- In SPARK or ALFA, there are no derived type definitions other than
- -- type extensions of tagged record types.
+ -- In SPARK, there are no derived type definitions other than type
+ -- extensions of tagged record types.
if No (Extension) then
- Check_Formal_Restriction ("derived type is not allowed", N);
+ Check_SPARK_Restriction ("derived type is not allowed", N);
end if;
end Derived_Type_Declaration;
Error_Msg_NE ("invalid redeclaration of }", Id, Prev);
end if;
- Set_Full_View (Prev, Id);
+ Set_Full_View (Prev, Id);
Append_Entity (Id, Current_Scope);
Set_Is_Public (Id, Is_Public (Prev));
Set_Is_Internal (Id);
Set_Has_Private_Declaration (Prev);
Set_Has_Private_Declaration (Id);
+ -- Preserve aspect and iterator flags that may have been set on
+ -- the partial view.
+
+ Set_Has_Delayed_Aspects (Prev, Has_Delayed_Aspects (Id));
+ Set_Has_Implicit_Dereference (Prev, Has_Implicit_Dereference (Id));
+
-- If no error, propagate freeze_node from private to full view.
-- It may have been generated for an early operational item.
end if;
end if;
+ if Present (Prev)
+ and then Nkind (Parent (Prev)) = N_Incomplete_Type_Declaration
+ and then Present (Premature_Use (Parent (Prev)))
+ then
+ Error_Msg_Sloc := Sloc (N);
+ Error_Msg_N
+ ("\full declaration #", Premature_Use (Parent (Prev)));
+ end if;
+
return New_Id;
end if;
end Find_Type_Name;
elsif Def_Kind = N_Access_Definition then
T := Access_Definition (Related_Nod, Obj_Def);
- Set_Is_Local_Anonymous_Access (T);
+
+ Set_Is_Local_Anonymous_Access
+ (T,
+ V => (Ada_Version < Ada_2012)
+ or else (Nkind (P) /= N_Object_Declaration)
+ or else Is_Library_Level_Entity (Defining_Identifier (P)));
-- Otherwise, the object definition is just a subtype_mark
elsif No (Real_Range_Specification (Def)) then
Error_Msg_Uint_1 := Max_Digs_Val;
Error_Msg_N ("types with more than ^ digits need range spec "
- & "('R'M 3.5.7(6))", Digs);
+ & "(RM 3.5.7(6))", Digs);
end if;
end;
end if;
Plain_Discrim : Boolean := False;
Stored_Discrim : Boolean := False)
is
+ procedure Set_Anonymous_Type (Id : Entity_Id);
+ -- Id denotes the entity of an access discriminant or anonymous
+ -- access component. Set the type of Id to either the same type of
+ -- Old_C or create a new one depending on whether the parent and
+ -- the child types are in the same scope.
+
+ ------------------------
+ -- Set_Anonymous_Type --
+ ------------------------
+
+ procedure Set_Anonymous_Type (Id : Entity_Id) is
+ Old_Typ : constant Entity_Id := Etype (Old_C);
+
+ begin
+ if Scope (Parent_Base) = Scope (Derived_Base) then
+ Set_Etype (Id, Old_Typ);
+
+ -- The parent and the derived type are in two different scopes.
+ -- Reuse the type of the original discriminant / component by
+ -- copying it in order to preserve all attributes.
+
+ else
+ declare
+ Typ : constant Entity_Id := New_Copy (Old_Typ);
+
+ begin
+ Set_Etype (Id, Typ);
+
+ -- Since we do not generate component declarations for
+ -- inherited components, associate the itype with the
+ -- derived type.
+
+ Set_Associated_Node_For_Itype (Typ, Parent (Derived_Base));
+ Set_Scope (Typ, Derived_Base);
+ end;
+ end if;
+ end Set_Anonymous_Type;
+
+ -- Local variables and constants
+
New_C : constant Entity_Id := New_Copy (Old_C);
- Discrim : Entity_Id;
Corr_Discrim : Entity_Id;
+ Discrim : Entity_Id;
+
+ -- Start of processing for Inherit_Component
begin
pragma Assert (not Is_Tagged or else not Stored_Discrim);
Set_Original_Record_Component (New_C, New_C);
end if;
+ -- Set the proper type of an access discriminant
+
+ if Ekind (New_C) = E_Discriminant
+ and then Ekind (Etype (New_C)) = E_Anonymous_Access_Type
+ then
+ Set_Anonymous_Type (New_C);
+ end if;
+
-- If we have inherited a component then see if its Etype contains
-- references to Parent_Base discriminants. In this case, replace
-- these references with the constraints given in Discs. We do not
-- transformation in some error situations.
if Ekind (New_C) = E_Component then
- if (Is_Private_Type (Derived_Base)
- and then not Is_Generic_Type (Derived_Base))
+
+ -- Set the proper type of an anonymous access component
+
+ if Ekind (Etype (New_C)) = E_Anonymous_Access_Type then
+ Set_Anonymous_Type (New_C);
+
+ elsif (Is_Private_Type (Derived_Base)
+ and then not Is_Generic_Type (Derived_Base))
or else (Is_Empty_Elmt_List (Discs)
- and then not Expander_Active)
+ and then not Expander_Active)
then
Set_Etype (New_C, Etype (Old_C));
Set_Etype
(New_C,
Constrain_Component_Type
- (Old_C, Derived_Base, N, Parent_Base, Discs));
+ (Old_C, Derived_Base, N, Parent_Base, Discs));
end if;
end if;
Next_E : Entity_Id;
begin
- -- The class wide type can have been defined by the partial view, in
- -- which case everything is already done.
-
if Present (Class_Wide_Type (T)) then
- return;
- end if;
- CW_Type :=
- New_External_Entity (E_Void, Scope (T), Sloc (T), T, 'C', 0, 'T');
+ -- The class-wide type is a partially decorated entity created for a
+ -- unanalyzed tagged type referenced through a limited with clause.
+ -- When the tagged type is analyzed, its class-wide type needs to be
+ -- redecorated. Note that we reuse the entity created by Decorate_
+ -- Tagged_Type in order to preserve all links.
+
+ if Materialize_Entity (Class_Wide_Type (T)) then
+ CW_Type := Class_Wide_Type (T);
+ Set_Materialize_Entity (CW_Type, False);
+
+ -- The class wide type can have been defined by the partial view, in
+ -- which case everything is already done.
+
+ else
+ return;
+ end if;
+
+ -- Default case, we need to create a new class-wide type
+
+ else
+ CW_Type :=
+ New_External_Entity (E_Void, Scope (T), Sloc (T), T, 'C', 0, 'T');
+ end if;
-- Inherit root type characteristics
-- Non-binary case
elsif M_Val < 2 ** Bits then
- Check_Formal_Restriction ("modulus should be a power of 2", T);
+ Check_SPARK_Restriction ("modulus should be a power of 2", T);
Set_Non_Binary_Modulus (T);
if Bits > System_Max_Nonbinary_Modulus_Power then
-- function calls. The function call may have been given in prefixed
-- notation, in which case the original node is an indexed component.
-- If the function is parameterless, the original node was an explicit
- -- dereference.
+ -- dereference. The function may also be parameterless, in which case
+ -- the source node is just an identifier.
case Nkind (Original_Node (Exp)) is
when N_Aggregate | N_Extension_Aggregate | N_Function_Call | N_Op =>
return True;
+ when N_Identifier =>
+ return Present (Entity (Original_Node (Exp)))
+ and then Ekind (Entity (Original_Node (Exp))) = E_Function;
+
when N_Qualified_Expression =>
return
OK_For_Limited_Init_In_05
when N_Attribute_Reference =>
return Attribute_Name (Original_Node (Exp)) = Name_Input;
+ -- For a conditional expression, all dependent expressions must be
+ -- legal constructs.
+
+ when N_Conditional_Expression =>
+ declare
+ Then_Expr : constant Node_Id :=
+ Next (First (Expressions (Original_Node (Exp))));
+ Else_Expr : constant Node_Id := Next (Then_Expr);
+ begin
+ return OK_For_Limited_Init_In_05 (Typ, Then_Expr)
+ and then OK_For_Limited_Init_In_05 (Typ, Else_Expr);
+ end;
+
+ when N_Case_Expression =>
+ declare
+ Alt : Node_Id;
+
+ begin
+ Alt := First (Alternatives (Original_Node (Exp)));
+ while Present (Alt) loop
+ if not OK_For_Limited_Init_In_05 (Typ, Expression (Alt)) then
+ return False;
+ end if;
+
+ Next (Alt);
+ end loop;
+
+ return True;
+ end;
+
when others =>
return False;
end case;
-- worst, and therefore defaults are not allowed if the parent is
-- a generic formal private type (see ACATS B370001).
- if Is_Access_Type (Discr_Type) then
+ if Is_Access_Type (Discr_Type) and then Default_Present then
if Ekind (Discr_Type) /= E_Anonymous_Access_Type
- or else not Default_Present
or else Is_Limited_Record (Current_Scope)
or else Is_Concurrent_Type (Current_Scope)
or else Is_Concurrent_Record_Type (Current_Scope)
and then (Is_Limited_Type (Full_T)
or else Is_Limited_Composite (Full_T))
then
- Error_Msg_N
- ("completion of nonlimited type cannot be limited", Full_T);
- Explain_Limited_Type (Full_T, Full_T);
+ if In_Instance then
+ null;
+ else
+ Error_Msg_N
+ ("completion of nonlimited type cannot be limited", Full_T);
+ Explain_Limited_Type (Full_T, Full_T);
+ end if;
elsif Is_Abstract_Type (Full_T)
and then not Is_Abstract_Type (Priv_T)
Set_Is_Limited_Record (Full_T);
-- GNAT allow its own definition of Limited_Controlled to disobey
- -- this rule in order in ease the implementation. The next test is
- -- safe because Root_Controlled is defined in a private system child
+ -- this rule in order in ease the implementation. This test is safe
+ -- because Root_Controlled is defined in a child of System that
+ -- normal programs are not supposed to use.
- elsif Etype (Full_T) = Full_View (RTE (RE_Root_Controlled)) then
+ elsif Is_RTE (Etype (Full_T), RE_Root_Controlled) then
Set_Is_Limited_Composite (Full_T);
else
Error_Msg_N
-- Ada 2005 (AI-251): The partial view shall be a descendant of
-- an interface type if and only if the full type is descendant
- -- of the interface type (AARM 7.3 (7.3/2).
+ -- of the interface type (AARM 7.3 (7.3/2)).
Iface := Find_Hidden_Interface (Priv_T_Ifaces, Full_T_Ifaces);
if Priv_Parent /= Full_Parent then
Error_Msg_Name_1 := Chars (Priv_Parent);
- Check_Formal_Restriction ("% expected", Full_Indic);
+ Check_SPARK_Restriction ("% expected", Full_Indic);
end if;
-- Check the rules of 7.3(10): if the private extension inherits
if Nkind (R) = N_Range then
- -- In SPARK/ALFA, all ranges should be static, with the exception of
- -- the discrete type definition of a loop parameter specification.
+ -- In SPARK, all ranges should be static, with the exception of the
+ -- discrete type definition of a loop parameter specification.
if not In_Iter_Schm
and then not Is_Static_Range (R)
then
- Check_Formal_Restriction ("range should be static", R);
+ Check_SPARK_Restriction ("range should be static", R);
end if;
Lo := Low_Bound (R);
-- Look up tree to find an appropriate insertion point. We
-- can't just use insert_actions because later processing
- -- depends on the insertion node. Prior to Ada2012 the
+ -- depends on the insertion node. Prior to Ada 2012 the
-- insertion point could only be a declaration or a loop, but
-- quantified expressions can appear within any context in an
-- expression, and the insertion point can be any statement,
return Process_Subtype (S, Related_Nod, Related_Id, Suffix);
end if;
- -- Remaining processing depends on type
+ -- Remaining processing depends on type. Select on Base_Type kind to
+ -- ensure getting to the concrete type kind in the case of a private
+ -- subtype (needed when only doing semantic analysis).
- case Ekind (Subtype_Mark_Id) is
+ case Ekind (Base_Type (Subtype_Mark_Id)) is
when Access_Kind =>
Constrain_Access (Def_Id, S, Related_Nod);
or else not Interface_Present (Def)
then
if Limited_Present (Def) then
- Check_Formal_Restriction ("limited is not allowed", N);
+ Check_SPARK_Restriction ("limited is not allowed", N);
end if;
if Abstract_Present (Def) then
- Check_Formal_Restriction ("abstract is not allowed", N);
+ Check_SPARK_Restriction ("abstract is not allowed", N);
end if;
-- The flag Is_Tagged_Type might have already been set by
or else Abstract_Present (Def));
else
- Check_Formal_Restriction ("interface is not allowed", N);
+ Check_SPARK_Restriction ("interface is not allowed", N);
Is_Tagged := True;
Analyze_Interface_Declaration (T, Def);
T := Prev_T;
end if;
- -- In SPARK or ALFA, tagged types and type extensions may only be
- -- declared in the specification of library unit packages.
+ -- In SPARK, tagged types and type extensions may only be declared in
+ -- the specification of library unit packages.
if Present (Def) and then Is_Tagged_Type (T) then
declare
if Nkind (Ctxt) = N_Package_Body
and then Nkind (Parent (Ctxt)) = N_Compilation_Unit
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("type should be defined in package specification", Typ);
elsif Nkind (Ctxt) /= N_Package_Specification
or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit
then
- Check_Formal_Restriction
+ Check_SPARK_Restriction
("type should be defined in library unit package", Typ);
end if;
end;
or else Null_Present (Component_List (Def))
then
if not Is_Tagged_Type (T) then
- Check_Formal_Restriction ("non-tagged record cannot be null", Def);
+ Check_SPARK_Restriction ("non-tagged record cannot be null", Def);
end if;
else
Analyze_Declarations (Component_Items (Component_List (Def)));
if Present (Variant_Part (Component_List (Def))) then
- Check_Formal_Restriction ("variant part is not allowed", Def);
+ Check_SPARK_Restriction ("variant part is not allowed", Def);
Analyze (Variant_Part (Component_List (Def)));
end if;
end if;
-- Complete both implicit base and declared first subtype entities
Set_Etype (Implicit_Base, Base_Typ);
- Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
Set_Size_Info (Implicit_Base, (Base_Typ));
Set_RM_Size (Implicit_Base, RM_Size (Base_Typ));
Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Base_Typ));
Set_Ekind (T, E_Signed_Integer_Subtype);
Set_Etype (T, Implicit_Base);
+ -- In formal verification mode, restrict the base type's range to the
+ -- minimum allowed by RM 3.5.4, namely the smallest symmetric range
+ -- around zero with a possible extra negative value that contains the
+ -- subtype range. Keep Size, RM_Size and First_Rep_Item info, which
+ -- should not be relied upon in formal verification.
+
+ if Strict_Alfa_Mode then
+ declare
+ Sym_Hi_Val : Uint;
+ Sym_Lo_Val : Uint;
+ Dloc : constant Source_Ptr := Sloc (Def);
+ Lbound : Node_Id;
+ Ubound : Node_Id;
+ Bounds : Node_Id;
+
+ begin
+ -- If the subtype range is empty, the smallest base type range
+ -- is the symmetric range around zero containing Lo_Val and
+ -- Hi_Val.
+
+ if UI_Gt (Lo_Val, Hi_Val) then
+ Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val));
+ Sym_Lo_Val := UI_Negate (Sym_Hi_Val);
+
+ -- Otherwise, if the subtype range is not empty and Hi_Val has
+ -- the largest absolute value, Hi_Val is non negative and the
+ -- smallest base type range is the symmetric range around zero
+ -- containing Hi_Val.
+
+ elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then
+ Sym_Hi_Val := Hi_Val;
+ Sym_Lo_Val := UI_Negate (Hi_Val);
+
+ -- Otherwise, the subtype range is not empty, Lo_Val has the
+ -- strictly largest absolute value, Lo_Val is negative and the
+ -- smallest base type range is the symmetric range around zero
+ -- with an extra negative value Lo_Val.
+
+ else
+ Sym_Lo_Val := Lo_Val;
+ Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1);
+ end if;
+
+ Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val);
+ Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val);
+ Set_Is_Static_Expression (Lbound);
+ Set_Is_Static_Expression (Ubound);
+ Analyze_And_Resolve (Lbound, Any_Integer);
+ Analyze_And_Resolve (Ubound, Any_Integer);
+
+ Bounds := Make_Range (Dloc, Lbound, Ubound);
+ Set_Etype (Bounds, Base_Typ);
+
+ Set_Scalar_Range (Implicit_Base, Bounds);
+ end;
+
+ else
+ Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ));
+ end if;
+
Set_Size_Info (T, (Implicit_Base));
Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
Set_Scalar_Range (T, Def);
OSDN Git Service
