This patch adds an enumeration type and a function to determine the default
initialization kind of an arbitrary type. These facilities are intended for
formal verification proofs. No applicable test.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-01-20 Hristian Kirtchev <kirtc...@adacore.com>
* sem_util.adb (Default_Initialization): New routine.
* sem_util.ads: Add new type Default_Initialization_Kind.
(Default_Initialization): New routine.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 206825)
+++ sem_util.adb (working copy)
@@ -3863,6 +3863,138 @@
end if;
end Deepest_Type_Access_Level;
+ ----------------------------
+ -- Default_Initialization --
+ ----------------------------
+
+ function Default_Initialization
+ (Typ : Entity_Id) return Default_Initialization_Kind
+ is
+ Comp : Entity_Id;
+ Init : Default_Initialization_Kind;
+
+ FDI : Boolean := False;
+ NDI : Boolean := False;
+ -- Two flags used to designate whether a record type has at least one
+ -- fully default initialized component and/or one not fully default
+ -- initialized component.
+
+ begin
+ -- Access types are always fully default initialized
+
+ if Is_Access_Type (Typ) then
+ return Full_Default_Initialization;
+
+ -- An array type subject to aspect/pragma Default_Component_Value is
+ -- fully default initialized. Otherwise its initialization status is
+ -- that of its component type.
+
+ elsif Is_Array_Type (Typ) then
+ if Present (Default_Aspect_Component_Value (Base_Type (Typ))) then
+ return Full_Default_Initialization;
+ else
+ return Default_Initialization (Component_Type (Typ));
+ end if;
+
+ -- The initialization status of a private type depends on its full view
+
+ elsif Is_Private_Type (Typ) and then Present (Full_View (Typ)) then
+ return Default_Initialization (Full_View (Typ));
+
+ -- Record and protected types offer several initialization options
+ -- depending on their components (if any).
+
+ elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
+ Comp := First_Component (Typ);
+
+ -- Inspect all components
+
+ if Present (Comp) then
+ while Present (Comp) loop
+
+ -- Do not process internally generated components except for
+ -- _parent which represents the ancestor portion of a derived
+ -- type.
+
+ if Comes_From_Source (Comp)
+ or else Chars (Comp) = Name_uParent
+ then
+ Init := Default_Initialization (Base_Type (Etype (Comp)));
+
+ -- A component with mixed initialization renders the whole
+ -- record/protected type mixed.
+
+ if Init = Mixed_Initialization then
+ return Mixed_Initialization;
+
+ -- The component is fully default initialized when its type
+ -- is fully default initialized or when the component has an
+ -- initialization expression. Note that this has precedence
+ -- given that the component type may lack initialization.
+
+ elsif Init = Full_Default_Initialization
+ or else Present (Expression (Parent (Comp)))
+ then
+ FDI := True;
+
+ -- Components with no possible initialization are ignored
+
+ elsif Init = No_Possible_Initialization then
+ null;
+
+ -- The component has no full default initialization
+
+ else
+ NDI := True;
+ end if;
+ end if;
+
+ Next_Component (Comp);
+ end loop;
+
+ -- Detect a mixed case of initialization
+
+ if FDI and NDI then
+ return Mixed_Initialization;
+
+ elsif FDI then
+ return Full_Default_Initialization;
+
+ elsif NDI then
+ return No_Default_Initialization;
+
+ -- The type either has no components or they are all internally
+ -- generated.
+
+ else
+ return No_Possible_Initialization;
+ end if;
+
+ -- The record type is null, there is nothing to initialize
+
+ else
+ return No_Possible_Initialization;
+ end if;
+
+ -- A scalar type subject to aspect/pragma Default_Value is fully default
+ -- initialized.
+
+ elsif Is_Scalar_Type (Typ)
+ and then Present (Default_Aspect_Value (Base_Type (Typ)))
+ then
+ return Full_Default_Initialization;
+
+ -- Task types are always fully default initialized
+
+ elsif Is_Task_Type (Typ) then
+ return Full_Default_Initialization;
+ end if;
+
+ -- The type has no full default initialization
+
+ return No_Default_Initialization;
+ end Default_Initialization;
+
---------------------
-- Defining_Entity --
---------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 206819)
+++ sem_util.ads (working copy)
@@ -384,6 +384,40 @@
-- Current_Scope is returned. The returned value is Empty if this is called
-- from a library package which is not within any subprogram.
+ -- The following type lists all possible forms of default initialization
+ -- that may apply to a type.
+
+ type Default_Initialization_Kind is
+ (No_Possible_Initialization,
+ -- This value signifies that a type cannot possibly be initialized
+ -- because it has no content, for example - a null record.
+
+ Full_Default_Initialization,
+ -- This value covers the following combinations of types and content:
+ -- * Access type
+ -- * Array-of-scalars with specified Default_Component_Value
+ -- * Array type with fully default initialized component type
+ -- * Record or protected type with components that either have a
+ -- default expression or their related types are fully default
+ -- initialized.
+ -- * Scalar type with specified Default_Value
+ -- * Task type
+ -- * Type extension of a type with full default initialization where
+ -- the extension components are also fully default initialized
+
+ Mixed_Initialization,
+ -- This value applies to a type where some of its internals are fully
+ -- default initialized and some are not.
+
+ No_Default_Initialization);
+ -- This value reflects a type where none of its content is fully
+ -- default initialized.
+
+ function Default_Initialization
+ (Typ : Entity_Id) return Default_Initialization_Kind;
+ -- Determine the default initialization kind that applies to a particular
+ -- type.
+
function Deepest_Type_Access_Level (Typ : Entity_Id) return Uint;
-- Same as Type_Access_Level, except that if the type is the type of an Ada
-- 2012 stand-alone object of an anonymous access type, then return the
