inline.adb (Has_Initialized_Type): Adapt to new names.
2015-05-26 Yannick Moy <moy@adacore.com> * inline.adb (Has_Initialized_Type): Adapt to new names. * sem_aux.adb, sem_aux.ads (Get_Low_Bound, Number_Components, Subprogram_Body, Subprogram_Body_Entity, Subprogram_Spec, Subprogram_Specification): New query functions used in GNATprove. * sem_disp.adb, sem_disp.ads (Is_Overriding_Subprogram): New query functions used in GNATprove. * sem_util.adb, sem_util.adso (Enclosing_Lib_Unit_Node, Get_Cursor_Type, Get_Return_Object, Get_User_Defined_Eq, Is_Double_Precision_Floating_Point_Type, Is_Single_Precision_Floating_Point_Type): New query functions used in GNATprove. From-SVN: r223674
This commit is contained in:
Yannick Moy
Arnaud Charlet
parent
35fd12d804
commit
90a4b33679
8 changed files with 328 additions and 40 deletions
|
|
@ -1,3 +1,17 @@
|
|||
2015-05-26 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* inline.adb (Has_Initialized_Type): Adapt to new names.
|
||||
* sem_aux.adb, sem_aux.ads (Get_Low_Bound, Number_Components,
|
||||
Subprogram_Body, Subprogram_Body_Entity, Subprogram_Spec,
|
||||
Subprogram_Specification): New query functions used in GNATprove.
|
||||
* sem_disp.adb, sem_disp.ads (Is_Overriding_Subprogram): New
|
||||
query functions used in GNATprove.
|
||||
* sem_util.adb, sem_util.adso (Enclosing_Lib_Unit_Node,
|
||||
Get_Cursor_Type, Get_Return_Object, Get_User_Defined_Eq,
|
||||
Is_Double_Precision_Floating_Point_Type,
|
||||
Is_Single_Precision_Floating_Point_Type): New query functions
|
||||
used in GNATprove.
|
||||
|
||||
2015-05-26 Bob Duff <duff@adacore.com>
|
||||
|
||||
* s-rpc.ads (Partition_ID): Increase maximum Partition_ID to
|
||||
|
|
|
|||
|
|
@ -3639,7 +3639,7 @@ package body Inline is
|
|||
--------------------------
|
||||
|
||||
function Has_Initialized_Type (E : Entity_Id) return Boolean is
|
||||
E_Body : constant Node_Id := Get_Subprogram_Body (E);
|
||||
E_Body : constant Node_Id := Subprogram_Body (E);
|
||||
Decl : Node_Id;
|
||||
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -472,6 +472,19 @@ package body Sem_Aux is
|
|||
end case;
|
||||
end Get_Binary_Nkind;
|
||||
|
||||
-------------------
|
||||
-- Get_Low_Bound --
|
||||
-------------------
|
||||
|
||||
function Get_Low_Bound (E : Entity_Id) return Node_Id is
|
||||
begin
|
||||
if Ekind (E) = E_String_Literal_Subtype then
|
||||
return String_Literal_Low_Bound (E);
|
||||
else
|
||||
return Low_Bound (Scalar_Range (E));
|
||||
end if;
|
||||
end Get_Low_Bound;
|
||||
|
||||
------------------
|
||||
-- Get_Rep_Item --
|
||||
------------------
|
||||
|
|
@ -1361,6 +1374,35 @@ package body Sem_Aux is
|
|||
return Empty;
|
||||
end Next_Tag_Component;
|
||||
|
||||
-----------------------
|
||||
-- Number_Components --
|
||||
-----------------------
|
||||
|
||||
function Number_Components (Typ : Entity_Id) return Pos is
|
||||
N : Int;
|
||||
Comp : Entity_Id;
|
||||
|
||||
begin
|
||||
N := 0;
|
||||
|
||||
-- We do not call Einfo.First_Component_Or_Discriminant, as this
|
||||
-- function does not skip completely hidden discriminants, which we
|
||||
-- want to skip here.
|
||||
|
||||
if Has_Discriminants (Typ) then
|
||||
Comp := First_Discriminant (Typ);
|
||||
else
|
||||
Comp := First_Component (Typ);
|
||||
end if;
|
||||
|
||||
while Present (Comp) loop
|
||||
N := N + 1;
|
||||
Comp := Next_Component_Or_Discriminant (Comp);
|
||||
end loop;
|
||||
|
||||
return N;
|
||||
end Number_Components;
|
||||
|
||||
--------------------------
|
||||
-- Number_Discriminants --
|
||||
--------------------------
|
||||
|
|
@ -1419,6 +1461,97 @@ package body Sem_Aux is
|
|||
return N;
|
||||
end Package_Specification;
|
||||
|
||||
---------------------
|
||||
-- Subprogram_Body --
|
||||
---------------------
|
||||
|
||||
function Subprogram_Body (E : Entity_Id) return Node_Id is
|
||||
Body_E : constant Entity_Id := Subprogram_Body_Entity (E);
|
||||
|
||||
begin
|
||||
if No (Body_E) then
|
||||
return Empty;
|
||||
else
|
||||
return Parent (Subprogram_Specification (Body_E));
|
||||
end if;
|
||||
end Subprogram_Body;
|
||||
|
||||
----------------------------
|
||||
-- Subprogram_Body_Entity --
|
||||
----------------------------
|
||||
|
||||
function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id is
|
||||
N : Node_Id;
|
||||
|
||||
begin
|
||||
-- Retrieve the declaration for E
|
||||
|
||||
N := Parent (Subprogram_Specification (E));
|
||||
|
||||
-- If this declaration is not a subprogram body, then it must be a
|
||||
-- subprogram declaration, from which we can retrieve the entity for
|
||||
-- the corresponding subprogram body if any.
|
||||
|
||||
if Nkind (N) = N_Subprogram_Body then
|
||||
return E;
|
||||
else
|
||||
return Corresponding_Body (N);
|
||||
end if;
|
||||
end Subprogram_Body_Entity;
|
||||
|
||||
---------------------
|
||||
-- Subprogram_Spec --
|
||||
---------------------
|
||||
|
||||
function Subprogram_Spec (E : Entity_Id) return Node_Id is
|
||||
N : Node_Id;
|
||||
|
||||
begin
|
||||
-- Retrieve the declaration for E
|
||||
|
||||
N := Parent (Subprogram_Specification (E));
|
||||
|
||||
-- This declaration is either subprogram declaration or a subprogram
|
||||
-- body, in which case return Empty.
|
||||
|
||||
if Nkind (N) = N_Subprogram_Declaration then
|
||||
return N;
|
||||
else
|
||||
return Empty;
|
||||
end if;
|
||||
end Subprogram_Spec;
|
||||
|
||||
------------------------------
|
||||
-- Subprogram_Specification --
|
||||
------------------------------
|
||||
|
||||
function Subprogram_Specification (E : Entity_Id) return Node_Id is
|
||||
N : Node_Id;
|
||||
|
||||
begin
|
||||
N := Parent (E);
|
||||
|
||||
if Nkind (N) = N_Defining_Program_Unit_Name then
|
||||
N := Parent (N);
|
||||
end if;
|
||||
|
||||
-- If the Parent pointer of E is not a subprogram specification node
|
||||
-- (going through an intermediate N_Defining_Program_Unit_Name node
|
||||
-- for subprogram units), then E is an inherited operation. Its parent
|
||||
-- points to the type derivation that produces the inheritance: that's
|
||||
-- the node that generates the subprogram specification. Its alias
|
||||
-- is the parent subprogram, and that one points to a subprogram
|
||||
-- declaration, or to another type declaration if this is a hierarchy
|
||||
-- of derivations.
|
||||
|
||||
if Nkind (N) not in N_Subprogram_Specification then
|
||||
pragma Assert (Present (Alias (E)));
|
||||
N := Subprogram_Specification (Alias (E));
|
||||
end if;
|
||||
|
||||
return N;
|
||||
end Subprogram_Specification;
|
||||
|
||||
---------------
|
||||
-- Tree_Read --
|
||||
---------------
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
-- --
|
||||
-- S p e c --
|
||||
-- --
|
||||
-- Copyright (C) 1992-2014, Free Software Foundation, Inc. --
|
||||
-- Copyright (C) 1992-2015, 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- --
|
||||
|
|
@ -158,6 +158,9 @@ package Sem_Aux is
|
|||
-- referencing this entity. It is an error to call this function if Ekind
|
||||
-- (Op) /= E_Operator.
|
||||
|
||||
function Get_Low_Bound (E : Entity_Id) return Node_Id;
|
||||
-- For an index subtype or string literal subtype, return its low bound
|
||||
|
||||
function Get_Unary_Nkind (Op : Entity_Id) return Node_Kind;
|
||||
-- Op must be an entity with an Ekind of E_Operator. This function returns
|
||||
-- the Nkind value that would be used to construct a unary operator node
|
||||
|
|
@ -369,6 +372,10 @@ package Sem_Aux is
|
|||
-- The result returned is the next _Tag field in this record, or Empty
|
||||
-- if this is the last such field.
|
||||
|
||||
function Number_Components (Typ : Entity_Id) return Pos;
|
||||
-- Typ is a record type, yields number of components (including
|
||||
-- discriminants) in type.
|
||||
|
||||
function Number_Discriminants (Typ : Entity_Id) return Pos;
|
||||
-- Typ is a type with discriminants, yields number of discriminants in type
|
||||
|
||||
|
|
@ -381,6 +388,30 @@ package Sem_Aux is
|
|||
-- derived type, and the subtype is not an unconstrained array subtype
|
||||
-- (RM 3.3(23.10/3)).
|
||||
|
||||
function Package_Specification (Pack_Id : Entity_Id) return Node_Id;
|
||||
-- Given an entity for a package or generic package, return corresponding
|
||||
-- package specification. Simplifies handling of child units, and better
|
||||
-- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)).
|
||||
|
||||
function Subprogram_Body (E : Entity_Id) return Node_Id;
|
||||
-- Given an entity for a subprogram (spec or body), return the
|
||||
-- corresponding subprogram body if any, or else Empty.
|
||||
|
||||
function Subprogram_Body_Entity (E : Entity_Id) return Entity_Id;
|
||||
-- Given an entity for a subprogram (spec or body), return the entity
|
||||
-- corresponding to the subprogram body, which may be the same as E or
|
||||
-- Empty if no body is available.
|
||||
|
||||
function Subprogram_Spec (E : Entity_Id) return Node_Id;
|
||||
-- Given an entity for a subprogram spec, return the corresponding
|
||||
-- subprogram spec if any, or else Empty.
|
||||
|
||||
function Subprogram_Specification (E : Entity_Id) return Node_Id;
|
||||
-- Given an entity for a subprogram, return the corresponding subprogram
|
||||
-- specification. If the entity is an inherited subprogram without
|
||||
-- specification itself, return the specification of the inherited
|
||||
-- subprogram.
|
||||
|
||||
function Ultimate_Alias (Prim : Entity_Id) return Entity_Id;
|
||||
pragma Inline (Ultimate_Alias);
|
||||
-- Return the last entity in the chain of aliased entities of Prim. If Prim
|
||||
|
|
@ -393,9 +424,4 @@ package Sem_Aux is
|
|||
-- it returns the subprogram, task or protected body node for it. The unit
|
||||
-- may be a child unit with any number of ancestors.
|
||||
|
||||
function Package_Specification (Pack_Id : Entity_Id) return Node_Id;
|
||||
-- Given an entity for a package or generic package, return corresponding
|
||||
-- package specification. Simplifies handling of child units, and better
|
||||
-- than the old idiom: Specification (Unit_Declaration_Node (Pack_Id)).
|
||||
|
||||
end Sem_Aux;
|
||||
|
|
|
|||
|
|
@ -2239,6 +2239,16 @@ package body Sem_Disp is
|
|||
end if;
|
||||
end Is_Inherited_Public_Operation;
|
||||
|
||||
------------------------------
|
||||
-- Is_Overriding_Subprogram --
|
||||
------------------------------
|
||||
|
||||
function Is_Overriding_Subprogram (E : Entity_Id) return Boolean is
|
||||
Inherited : constant Subprogram_List := Inherited_Subprograms (E);
|
||||
begin
|
||||
return Inherited'Length > 0;
|
||||
end Is_Overriding_Subprogram;
|
||||
|
||||
--------------------------
|
||||
-- Is_Tag_Indeterminate --
|
||||
--------------------------
|
||||
|
|
|
|||
|
|
@ -129,6 +129,9 @@ package Sem_Disp is
|
|||
function Is_Null_Interface_Primitive (E : Entity_Id) return Boolean;
|
||||
-- Returns True if E is a null procedure that is an interface primitive
|
||||
|
||||
function Is_Overriding_Subprogram (E : Entity_Id) return Boolean;
|
||||
-- Returns True if E is an overriding subprogram
|
||||
|
||||
function Is_Tag_Indeterminate (N : Node_Id) return Boolean;
|
||||
-- Returns true if the expression N is tag-indeterminate. An expression
|
||||
-- is tag-indeterminate if it is a call that dispatches on result, and all
|
||||
|
|
|
|||
|
|
@ -5674,6 +5674,25 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Enclosing_Comp_Unit_Node;
|
||||
|
||||
-----------------------------
|
||||
-- Enclosing_Lib_Unit_Node --
|
||||
-----------------------------
|
||||
|
||||
function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id is
|
||||
Encl_Unit : Node_Id;
|
||||
|
||||
begin
|
||||
Encl_Unit := Enclosing_Comp_Unit_Node (N);
|
||||
|
||||
while Present (Encl_Unit)
|
||||
and then Nkind (Unit (Encl_Unit)) = N_Subunit
|
||||
loop
|
||||
Encl_Unit := Library_Unit (Encl_Unit);
|
||||
end loop;
|
||||
|
||||
return Encl_Unit;
|
||||
end Enclosing_Lib_Unit_Node;
|
||||
|
||||
--------------------------
|
||||
-- Enclosing_CPP_Parent --
|
||||
--------------------------
|
||||
|
|
@ -7417,6 +7436,11 @@ package body Sem_Util is
|
|||
return Cursor;
|
||||
end Get_Cursor_Type;
|
||||
|
||||
function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id is
|
||||
begin
|
||||
return Etype (Get_Iterable_Type_Primitive (Typ, Name_First));
|
||||
end Get_Cursor_Type;
|
||||
|
||||
-------------------------------
|
||||
-- Get_Default_External_Name --
|
||||
-------------------------------
|
||||
|
|
@ -7771,34 +7795,24 @@ package body Sem_Util is
|
|||
return R;
|
||||
end Get_Renamed_Entity;
|
||||
|
||||
-------------------------
|
||||
-- Get_Subprogram_Body --
|
||||
-------------------------
|
||||
-----------------------
|
||||
-- Get_Return_Object --
|
||||
-----------------------
|
||||
|
||||
function Get_Subprogram_Body (E : Entity_Id) return Node_Id is
|
||||
function Get_Return_Object (N : Node_Id) return Entity_Id is
|
||||
Decl : Node_Id;
|
||||
|
||||
begin
|
||||
Decl := Unit_Declaration_Node (E);
|
||||
Decl := First (Return_Object_Declarations (N));
|
||||
while Present (Decl) loop
|
||||
exit when Nkind (Decl) = N_Object_Declaration
|
||||
and then Is_Return_Object (Defining_Identifier (Decl));
|
||||
Next (Decl);
|
||||
end loop;
|
||||
|
||||
if Nkind (Decl) = N_Subprogram_Body then
|
||||
return Decl;
|
||||
|
||||
-- The below comment is bad, because it is possible for
|
||||
-- Nkind (Decl) to be an N_Subprogram_Body_Stub ???
|
||||
|
||||
else -- Nkind (Decl) = N_Subprogram_Declaration
|
||||
|
||||
if Present (Corresponding_Body (Decl)) then
|
||||
return Unit_Declaration_Node (Corresponding_Body (Decl));
|
||||
|
||||
-- Imported subprogram case
|
||||
|
||||
else
|
||||
return Empty;
|
||||
end if;
|
||||
end if;
|
||||
end Get_Subprogram_Body;
|
||||
pragma Assert (Present (Decl));
|
||||
return Defining_Identifier (Decl);
|
||||
end Get_Return_Object;
|
||||
|
||||
---------------------------
|
||||
-- Get_Subprogram_Entity --
|
||||
|
|
@ -7878,6 +7892,33 @@ package body Sem_Util is
|
|||
return Task_Body_Procedure (Underlying_Type (Root_Type (E)));
|
||||
end Get_Task_Body_Procedure;
|
||||
|
||||
-------------------------
|
||||
-- Get_User_Defined_Eq --
|
||||
-------------------------
|
||||
|
||||
function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id is
|
||||
Prim : Elmt_Id;
|
||||
Op : Entity_Id;
|
||||
|
||||
begin
|
||||
Prim := First_Elmt (Collect_Primitive_Operations (E));
|
||||
while Present (Prim) loop
|
||||
Op := Node (Prim);
|
||||
|
||||
if Chars (Op) = Name_Op_Eq
|
||||
and then Etype (Op) = Standard_Boolean
|
||||
and then Etype (First_Formal (Op)) = E
|
||||
and then Etype (Next_Formal (First_Formal (Op))) = E
|
||||
then
|
||||
return Op;
|
||||
end if;
|
||||
|
||||
Next_Elmt (Prim);
|
||||
end loop;
|
||||
|
||||
return Empty;
|
||||
end Get_User_Defined_Eq;
|
||||
|
||||
-----------------------
|
||||
-- Has_Access_Values --
|
||||
-----------------------
|
||||
|
|
@ -11242,6 +11283,20 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Is_Descendent_Of;
|
||||
|
||||
---------------------------------------------
|
||||
-- Is_Double_Precision_Floating_Point_Type --
|
||||
---------------------------------------------
|
||||
|
||||
function Is_Double_Precision_Floating_Point_Type
|
||||
(E : Entity_Id) return Boolean is
|
||||
begin
|
||||
return Is_Floating_Point_Type (E)
|
||||
and then Machine_Radix_Value (E) = Uint_2
|
||||
and then Machine_Mantissa_Value (E) = UI_From_Int (53)
|
||||
and then Machine_Emax_Value (E) = Uint_2 ** Uint_10
|
||||
and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_10);
|
||||
end Is_Double_Precision_Floating_Point_Type;
|
||||
|
||||
-----------------------------
|
||||
-- Is_Effectively_Volatile --
|
||||
-----------------------------
|
||||
|
|
@ -12703,6 +12758,20 @@ package body Sem_Util is
|
|||
end if;
|
||||
end Is_Selector_Name;
|
||||
|
||||
---------------------------------------------
|
||||
-- Is_Single_Precision_Floating_Point_Type --
|
||||
---------------------------------------------
|
||||
|
||||
function Is_Single_Precision_Floating_Point_Type
|
||||
(E : Entity_Id) return Boolean is
|
||||
begin
|
||||
return Is_Floating_Point_Type (E)
|
||||
and then Machine_Radix_Value (E) = Uint_2
|
||||
and then Machine_Mantissa_Value (E) = Uint_24
|
||||
and then Machine_Emax_Value (E) = Uint_2 ** Uint_7
|
||||
and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_7);
|
||||
end Is_Single_Precision_Floating_Point_Type;
|
||||
|
||||
-------------------------------------
|
||||
-- Is_SPARK_05_Initialization_Expr --
|
||||
-------------------------------------
|
||||
|
|
|
|||
|
|
@ -529,9 +529,16 @@ package Sem_Util is
|
|||
-- related expression evaluates to True.
|
||||
|
||||
function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id;
|
||||
-- Returns the enclosing N_Compilation_Unit Node that is the root of a
|
||||
-- Returns the enclosing N_Compilation_Unit node that is the root of a
|
||||
-- subtree containing N.
|
||||
|
||||
function Enclosing_Lib_Unit_Node (N : Node_Id) return Node_Id;
|
||||
-- Returns the N_Compilation_Unit node of the library unit that is directly
|
||||
-- or indirectly (through a subunit) at the root of a subtree containing
|
||||
-- N. This may be either the same as Enclosing_Comp_Unit_Node, or if
|
||||
-- Enclosing_Comp_Unit_Node returns a subunit, then the corresponding
|
||||
-- library unit.
|
||||
|
||||
function Enclosing_CPP_Parent (Typ : Entity_Id) return Entity_Id;
|
||||
-- Returns the closest ancestor of Typ that is a CPP type.
|
||||
|
||||
|
|
@ -814,10 +821,15 @@ package Sem_Util is
|
|||
function Get_Cursor_Type
|
||||
(Aspect : Node_Id;
|
||||
Typ : Entity_Id) return Entity_Id;
|
||||
-- Find Cursor type in scope of formal container Typ, by locating primitive
|
||||
-- operation First. For use in resolving the other primitive operations
|
||||
-- of an Iterable type and expanding loops and quantified expressions
|
||||
-- over formal containers.
|
||||
-- Find Cursor type in scope of type Typ with Iterable aspect, by locating
|
||||
-- primitive operation First. For use in resolving the other primitive
|
||||
-- operations of an Iterable type and expanding loops and quantified
|
||||
-- expressions over formal containers.
|
||||
|
||||
function Get_Cursor_Type (Typ : Entity_Id) return Entity_Id;
|
||||
-- Find Cursor type in scope of type Typ with Iterable aspect, by locating
|
||||
-- primitive operation First. For use after resolving the primitive
|
||||
-- operations of an Iterable type.
|
||||
|
||||
function Get_Default_External_Name (E : Node_Or_Entity_Id) return Node_Id;
|
||||
-- This is used to construct the string literal node representing a
|
||||
|
|
@ -906,22 +918,25 @@ package Sem_Util is
|
|||
-- not a renamed entity, returns its argument. It is an error to call this
|
||||
-- with any other kind of entity.
|
||||
|
||||
function Get_Return_Object (N : Node_Id) return Entity_Id;
|
||||
-- Given an extended return statement, return the corresponding return
|
||||
-- object, identified as the one for which Is_Return_Object = True.
|
||||
|
||||
function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id;
|
||||
-- Nod is either a procedure call statement, or a function call, or an
|
||||
-- accept statement node. This procedure finds the Entity_Id of the related
|
||||
-- subprogram or entry and returns it, or if no subprogram can be found,
|
||||
-- returns Empty.
|
||||
|
||||
function Get_Subprogram_Body (E : Entity_Id) return Node_Id;
|
||||
-- Given the entity for a subprogram (E_Function or E_Procedure), return
|
||||
-- the corresponding N_Subprogram_Body node. If the corresponding body
|
||||
-- is missing (as for an imported subprogram), return Empty.
|
||||
|
||||
function Get_Task_Body_Procedure (E : Entity_Id) return Node_Id;
|
||||
pragma Inline (Get_Task_Body_Procedure);
|
||||
-- Given an entity for a task type or subtype, retrieves the
|
||||
-- Task_Body_Procedure field from the corresponding task type declaration.
|
||||
|
||||
function Get_User_Defined_Eq (E : Entity_Id) return Entity_Id;
|
||||
-- For a type entity, return the entity of the primitive equality function
|
||||
-- for the type if it exists, otherwise return Empty.
|
||||
|
||||
function Has_Access_Values (T : Entity_Id) return Boolean;
|
||||
-- Returns true if type or subtype T is an access type, or has a component
|
||||
-- (at any recursive level) that is an access type. This is a conservative
|
||||
|
|
@ -1248,6 +1263,15 @@ package Sem_Util is
|
|||
-- This is the RM definition, a type is a descendent of another type if it
|
||||
-- is the same type or is derived from a descendent of the other type.
|
||||
|
||||
function Is_Double_Precision_Floating_Point_Type
|
||||
(E : Entity_Id) return Boolean;
|
||||
-- Return whether E is a double precision floating point type,
|
||||
-- characterized by:
|
||||
-- . machine_radix = 2
|
||||
-- . machine_mantissa = 53
|
||||
-- . machine_emax = 2**10
|
||||
-- . machine_emin = 3 - machine_emax
|
||||
|
||||
function Is_Effectively_Volatile (Id : Entity_Id) return Boolean;
|
||||
-- The SPARK property "effectively volatile" applies to both types and
|
||||
-- objects. To qualify as such, an entity must be either volatile or be
|
||||
|
|
@ -1410,6 +1434,15 @@ package Sem_Util is
|
|||
-- represent use of the N_Identifier node for a true identifier, when
|
||||
-- normally such nodes represent a direct name.
|
||||
|
||||
function Is_Single_Precision_Floating_Point_Type
|
||||
(E : Entity_Id) return Boolean;
|
||||
-- Return whether E is a single precision floating point type,
|
||||
-- characterized by:
|
||||
-- . machine_radix = 2
|
||||
-- . machine_mantissa = 24
|
||||
-- . machine_emax = 2**7
|
||||
-- . machine_emin = 3 - machine_emax
|
||||
|
||||
function Is_SPARK_05_Initialization_Expr (N : Node_Id) return Boolean;
|
||||
-- Determines if the tree referenced by N represents an initialization
|
||||
-- expression in SPARK 2005, suitable for initializing an object in an
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue