-- 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_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
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;
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
-- 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 (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);
OSDN Git Service
