-- 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.
+ -- 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_SPARK_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;
+
+ 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);
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;
Act_T := T;
- -- The object is in ALFA if-and-only-if its type is in ALFA and it is
- -- not aliased.
-
- if not Is_In_ALFA (T) then
- Mark_Non_ALFA_Subprogram ("object type is not in 'A'L'F'A", N);
- elsif Aliased_Present (N) then
- Mark_Non_ALFA_Subprogram ("ALIASED is not in 'A'L'F'A", N);
- else
- Set_Is_In_ALFA (Id);
- end if;
-
-- These checks should be performed before the initialization expression
-- is considered, so that the Object_Definition node is still the same
-- as in source code.
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));
Set_Last_Entity (Id, Last_Entity (T));
Set_Private_Dependents (Id, New_Elmt_List);
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));
Set_Known_To_Have_Preelab_Init
Nb_Index : Nat;
P : constant Node_Id := Parent (Def);
Priv : Entity_Id;
- T_In_ALFA : Boolean := True;
begin
if Nkind (Def) = N_Constrained_Array_Definition then
Make_Index (Index, P, Related_Id, Nb_Index);
- if Present (Etype (Index))
- and then not Is_In_ALFA (Etype (Index))
- then
- T_In_ALFA := False;
- end if;
-
-- Check error of subtype with predicate for index type
Bad_Predicated_Subtype_Use
Check_SPARK_Restriction ("subtype mark required", Component_Typ);
end if;
- if Present (Element_Type)
- and then not Is_In_ALFA (Element_Type)
- then
- T_In_ALFA := False;
- end if;
-
-- Ada 2005 (AI-230): Access Definition case
else pragma Assert (Present (Access_Definition (Component_Def)));
- T_In_ALFA := False;
-
-- Indicate that the anonymous access type is created by the
-- array type declaration.
(Implicit_Base, Finalize_Storage_Only
(Element_Type));
- -- Final check for static bounds on array
-
- if not Has_Static_Array_Bounds (T) then
- T_In_ALFA := False;
- end if;
-
-- Unconstrained array case
else
Set_Component_Type (Base_Type (T), Element_Type);
Set_Packed_Array_Type (T, Empty);
- Set_Is_In_ALFA (T, T_In_ALFA);
- Set_Is_In_ALFA (Base_Type (T), T_In_ALFA);
if Aliased_Present (Component_Definition (Def)) then
Check_SPARK_Restriction
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
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_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 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;
C : constant Node_Id := Constraint (S);
begin
- -- By default, consider that the enumeration subtype is in ALFA if the
- -- entity of its subtype mark is in ALFA. This is reversed later if the
- -- range of the subtype is not static.
-
- if Is_In_ALFA (T) then
- Set_Is_In_ALFA (Def_Id);
- end if;
-
Set_Ekind (Def_Id, E_Enumeration_Subtype);
Set_First_Literal (Def_Id, First_Literal (Base_Type (T)));
C : constant Node_Id := Constraint (S);
begin
- -- By default, consider that the integer subtype is in ALFA if the
- -- entity of its subtype mark is in ALFA. This is reversed later if the
- -- range of the subtype is not static.
-
- if Is_In_ALFA (T) then
- Set_Is_In_ALFA (Def_Id);
- end if;
-
Set_Scalar_Range_For_Subtype (Def_Id, Range_Expression (C), T);
if Is_Modular_Integer_Type (T) then
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
Set_Enum_Esize (T);
Set_Enum_Pos_To_Rep (T, Empty);
- -- Enumeration type is in ALFA only if it is not a character type
-
- if not Is_Character_Type (T) then
- Set_Is_In_ALFA (T);
- end if;
-
-- Set Discard_Names if configuration pragma set, or if there is
-- a parameterless pragma in the current declarative region
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;
then
Set_Is_Non_Static_Subtype (Def_Id);
end if;
-
- -- By default, consider that the subtype is in ALFA if its base type
- -- is in ALFA.
-
- Set_Is_In_ALFA (Def_Id, Is_In_ALFA (Base_Type (Def_Id)));
-
- -- In ALFA, all subtypes should have a static range
-
- if Nkind (R) = N_Range
- and then not Is_Static_Range (R)
- then
- Set_Is_In_ALFA (Def_Id, False);
- end if;
end if;
-- Final step is to label the index with this constructed type
-- GNAT allow its own definition of Limited_Controlled to disobey
-- this rule in order in ease the implementation. This test is safe
- -- because Root_Controlled is defined in a private system child.
+ -- because Root_Controlled is defined in a child of System that
+ -- normal programs are not supposed to use.
elsif Is_RTE (Etype (Full_T), RE_Root_Controlled) then
Set_Is_Limited_Composite (Full_T);
Set_Ekind (Def_Id, E_Void);
Process_Range_Expr_In_Decl (R, Subt);
Set_Ekind (Def_Id, Kind);
-
- -- In ALFA, all subtypes should have a static range
-
- if Nkind (R) = N_Range
- and then not Is_Static_Range (R)
- then
- Set_Is_In_ALFA (Def_Id, False);
- end if;
end Set_Scalar_Range_For_Subtype;
--------------------------------------------------------
Set_Ekind (T, E_Signed_Integer_Subtype);
Set_Etype (T, Implicit_Base);
+ -- In formal verification mode, override partially the decisions above
+ -- to restrict 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 ALFA_Mode then
+
+ -- If the range of the type is already symmetric with a possible
+ -- extra negative value, just make the type its own base type.
+
+ if UI_Le (Lo_Val, Hi_Val)
+ and then (UI_Eq (Lo_Val, UI_Negate (Hi_Val))
+ or else
+ UI_Eq (Lo_Val, UI_Sub (UI_Negate (Hi_Val), Uint_1)))
+ then
+ Set_Etype (T, T);
+
+ else
+ declare
+ Sym_Hi_Val : Uint;
+ Sym_Lo_Val : Uint;
+ Decl : Node_Id;
+ Dloc : constant Source_Ptr := Sloc (Def);
+ Lbound : Node_Id;
+ Ubound : 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);
+
+ Decl := Make_Full_Type_Declaration (Dloc,
+ Defining_Identifier => Implicit_Base,
+ Type_Definition =>
+ Make_Signed_Integer_Type_Definition (Dloc,
+ Low_Bound => Lbound,
+ High_Bound => Ubound));
+
+ Analyze (Decl);
+ Set_Etype (Implicit_Base, Implicit_Base);
+ Insert_Before (Parent (Def), Decl);
+ end;
+ end if;
+ end if;
+
Set_Size_Info (T, (Implicit_Base));
Set_First_Rep_Item (T, First_Rep_Item (Implicit_Base));
Set_Scalar_Range (T, Def);
Set_RM_Size (T, UI_From_Int (Minimum_Size (T)));
Set_Is_Constrained (T);
- Set_Is_In_ALFA (T);
end Signed_Integer_Type_Declaration;
end Sem_Ch3;
OSDN Git Service
