===================================================================
@@ -9046,110 +9046,6 @@
end if;
end Has_Enabled_Property;
- -------------------------------------
- -- Has_Full_Default_Initialization --
- -------------------------------------
-
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
- Arg : Node_Id;
- Comp : Entity_Id;
- Prag : Node_Id;
-
- begin
- -- A private type and its full view is fully default initialized when it
- -- is subject to pragma Default_Initial_Condition without an argument or
- -- with a non-null argument. Since any type may act as the full view of
- -- a private type, this check must be performed prior to the specialized
- -- tests below.
-
- if Has_Default_Init_Cond (Typ)
- or else Has_Inherited_Default_Init_Cond (Typ)
- then
- Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-
- -- Pragma Default_Initial_Condition must be present if one of the
- -- related entity flags is set.
-
- pragma Assert (Present (Prag));
- Arg := First (Pragma_Argument_Associations (Prag));
-
- -- A non-null argument guarantees full default initialization
-
- if Present (Arg) then
- return Nkind (Arg) /= N_Null;
-
- -- Otherwise the missing argument defaults the pragma to "True" which
- -- is considered a non-null argument (see above).
-
- else
- return True;
- end if;
- end if;
-
- -- A scalar type is fully default initialized if it is subject to aspect
- -- Default_Value.
-
- if Is_Scalar_Type (Typ) then
- return Has_Default_Aspect (Typ);
-
- -- An array type is fully default initialized if its element type is
- -- scalar and the array type carries aspect Default_Component_Value or
- -- the element type is fully default initialized.
-
- elsif Is_Array_Type (Typ) then
- return
- Has_Default_Aspect (Typ)
- or else Has_Full_Default_Initialization (Component_Type (Typ));
-
- -- A protected type, record type or type extension is fully default
- -- initialized if all its components either carry an initialization
- -- expression or have a type that is fully default initialized. The
- -- parent type of a type extension must be fully default initialized.
-
- elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
-
- -- Inspect all entities defined in the scope of the type, looking for
- -- uninitialized components.
-
- Comp := First_Entity (Typ);
- while Present (Comp) loop
- if Ekind (Comp) = E_Component
- and then Comes_From_Source (Comp)
- and then No (Expression (Parent (Comp)))
- and then not Has_Full_Default_Initialization (Etype (Comp))
- then
- return False;
- end if;
-
- Next_Entity (Comp);
- end loop;
-
- -- Ensure that the parent type of a type extension is fully default
- -- initialized.
-
- if Etype (Typ) /= Typ
- and then not Has_Full_Default_Initialization (Etype (Typ))
- then
- return False;
- end if;
-
- -- If we get here, then all components and parent portion are fully
- -- default initialized.
-
- return True;
-
- -- A task type is fully default initialized by default
-
- elsif Is_Task_Type (Typ) then
- return True;
-
- -- Otherwise the type is not fully default initialized
-
- else
- return False;
- end if;
- end Has_Full_Default_Initialization;
-
--------------------
-- Has_Infinities --
--------------------
===================================================================
@@ -1034,19 +1034,6 @@
-- Determine whether subprogram Subp_Id has an effectively volatile formal
-- parameter or returns an effectively volatile value.
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ defines "full default initialization" as
- -- specified by SPARK RM 3.1. To qualify as such, the type must be
- -- * A scalar type with specified Default_Value
- -- * An array-of-scalar type with specified Default_Component_Value
- -- * An array type whose element type defines full default initialization
- -- * A protected type, record type or type extension whose components
- -- either include a default expression or have a type which defines
- -- full default initialization. In the case of type extensions, the
- -- parent type defines full default initialization.
- -- * A task type
- -- * A private type whose Default_Initial_Condition is non-null
-
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
===================================================================
@@ -660,7 +660,6 @@
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
AR_Val : Boolean := False;
AW_Val : Boolean := False;
- Encap_Id : Entity_Id;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
Items : Node_Id;
@@ -872,28 +871,6 @@
Obj_Id);
end if;
end if;
-
- -- A variable whose Part_Of pragma specifies a single concurrent
- -- type as encapsulator must be (SPARK RM 9.4):
- -- * Of a type that defines full default initialization, or
- -- * Declared with a default value, or
- -- * Imported
-
- Encap_Id := Encapsulating_State (Obj_Id);
-
- if Present (Encap_Id)
- and then Is_Single_Concurrent_Object (Encap_Id)
- and then not Has_Full_Default_Initialization (Etype (Obj_Id))
- and then not Has_Initial_Value (Obj_Id)
- and then not Is_Imported (Obj_Id)
- then
- Error_Msg_N ("& requires full default initialization", Obj_Id);
-
- Error_Msg_Name_1 := Chars (Encap_Id);
- Error_Msg_N
- (Fix_Msg (Encap_Id, "\object acts as constituent of single "
- & "protected type %"), Obj_Id);
- end if;
end if;
end if;
@@ -1137,7 +1114,6 @@
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
Items : constant Node_Id := Contract (Prot_Id);
- Mode : SPARK_Mode_Type;
begin
-- Do not analyze a contract multiple times
@@ -1149,30 +1125,6 @@
Set_Analyzed (Items);
end if;
end if;
-
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related protected unit.
-
- Save_SPARK_Mode_And_Set (Prot_Id, Mode);
-
- -- A protected type must define full default initialization
- -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as
- -- it is not a standard Ada legality rule.
-
- if SPARK_Mode = On
- and then not Has_Full_Default_Initialization (Prot_Id)
- then
- Error_Msg_N
- ("protected type & must define full default initialization",
- Prot_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
end Analyze_Protected_Contract;
-------------------------------------------