[multiple changes]
2016-04-18 Bob Duff <duff@adacore.com> * a-cuprqu.ads: Change the representation of List_Type from a singly-linked list to a doubly-linked list. In addition, add a pointer Next_Unequal, which points past a possibly-long chain of equal-priority items. This increases efficiency, especially in the case of many equal-priority items. * a-cuprqu.adb (Dequeue, Enqueue): Rewrite algorithms to take advantage of new data structure. (Finalize): Rewrite in terms of Dequeue, for simplicity. 2016-04-18 Yannick Moy <moy@adacore.com> * contracts.adb (Analyze_Object_Contract, Analyze_Protected_Contract): Remove tests performed in GNATprove. * sem_util.adb, sem_util.ads (Has_Full_Default_Initialization): Remove query for tests performed in GNATprove. From-SVN: r235121
This commit is contained in:
Arnaud Charlet
parent
ec3c7387ac
commit
142870f570
|
|
@ -1,3 +1,21 @@
|
|||
2016-04-18 Bob Duff <duff@adacore.com>
|
||||
|
||||
* a-cuprqu.ads: Change the representation of List_Type from a
|
||||
singly-linked list to a doubly-linked list. In addition, add a
|
||||
pointer Next_Unequal, which points past a possibly-long chain
|
||||
of equal-priority items. This increases efficiency, especially
|
||||
in the case of many equal-priority items.
|
||||
* a-cuprqu.adb (Dequeue, Enqueue): Rewrite algorithms to take
|
||||
advantage of new data structure.
|
||||
(Finalize): Rewrite in terms of Dequeue, for simplicity.
|
||||
|
||||
2016-04-18 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* contracts.adb (Analyze_Object_Contract,
|
||||
Analyze_Protected_Contract): Remove tests performed in GNATprove.
|
||||
* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization):
|
||||
Remove query for tests performed in GNATprove.
|
||||
|
||||
2016-04-18 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_aggr.adb (Resolve_Record_Aggregate): If
|
||||
|
|
|
|||
|
|
@ -37,8 +37,21 @@ package body Ada.Containers.Unbounded_Priority_Queues is
|
|||
-- Local Subprograms --
|
||||
-----------------------
|
||||
|
||||
function Before_Or_Equal (X, Y : Queue_Priority) return Boolean;
|
||||
-- True if X is before or equal to Y. Equal means both Before(X,Y) and
|
||||
-- Before(Y,X) are False.
|
||||
|
||||
procedure Free is
|
||||
new Ada.Unchecked_Deallocation (Node_Type, Node_Access);
|
||||
new Ada.Unchecked_Deallocation (Node_Type, Node_Access);
|
||||
|
||||
---------------------
|
||||
-- Before_Or_Equal --
|
||||
---------------------
|
||||
|
||||
function Before_Or_Equal (X, Y : Queue_Priority) return Boolean is
|
||||
begin
|
||||
return (if Before (X, Y) then True else not Before (Y, X));
|
||||
end Before_Or_Equal;
|
||||
|
||||
-------------
|
||||
-- Dequeue --
|
||||
|
|
@ -48,20 +61,36 @@ package body Ada.Containers.Unbounded_Priority_Queues is
|
|||
(List : in out List_Type;
|
||||
Element : out Queue_Interfaces.Element_Type)
|
||||
is
|
||||
X : Node_Access;
|
||||
H : constant Node_Access := List.Header'Unchecked_Access;
|
||||
pragma Assert (List.Length /= 0);
|
||||
pragma Assert (List.Header.Next /= H);
|
||||
-- List can't be empty; see the barrier
|
||||
|
||||
pragma Assert
|
||||
(List.Header.Next.Next = H or else
|
||||
Before_Or_Equal (Get_Priority (List.Header.Next.Element),
|
||||
Get_Priority (List.Header.Next.Next.Element)));
|
||||
-- The first item is before-or-equal to the second
|
||||
|
||||
pragma Assert
|
||||
(List.Header.Next.Next_Unequal = H or else
|
||||
Before (Get_Priority (List.Header.Next.Element),
|
||||
Get_Priority (List.Header.Next.Next_Unequal.Element)));
|
||||
-- The first item is before its Next_Unequal item
|
||||
|
||||
-- The highest-priority item is always first; just remove it and
|
||||
-- return that element.
|
||||
|
||||
X : Node_Access := List.Header.Next;
|
||||
|
||||
-- Start of processing for Dequeue
|
||||
|
||||
begin
|
||||
Element := List.First.Element;
|
||||
|
||||
X := List.First;
|
||||
List.First := List.First.Next;
|
||||
|
||||
if List.First = null then
|
||||
List.Last := null;
|
||||
end if;
|
||||
|
||||
Element := X.Element;
|
||||
X.Next.Prev := H;
|
||||
List.Header.Next := X.Next;
|
||||
List.Header.Next_Unequal := X.Next;
|
||||
List.Length := List.Length - 1;
|
||||
|
||||
Free (X);
|
||||
end Dequeue;
|
||||
|
||||
|
|
@ -93,15 +122,13 @@ package body Ada.Containers.Unbounded_Priority_Queues is
|
|||
-- dequeue an item. If it's false, it means no item is dequeued, and
|
||||
-- we return False as the Success value.
|
||||
|
||||
if List.Length = 0
|
||||
or else Before (At_Least, Get_Priority (List.First.Element))
|
||||
then
|
||||
Success := False;
|
||||
return;
|
||||
end if;
|
||||
Success := List.Length > 0
|
||||
and then
|
||||
not Before (At_Least, Get_Priority (List.Header.Next.Element));
|
||||
|
||||
List.Dequeue (Element);
|
||||
Success := True;
|
||||
if Success then
|
||||
List.Dequeue (Element);
|
||||
end if;
|
||||
end Dequeue;
|
||||
|
||||
-------------
|
||||
|
|
@ -113,41 +140,55 @@ package body Ada.Containers.Unbounded_Priority_Queues is
|
|||
New_Item : Queue_Interfaces.Element_Type)
|
||||
is
|
||||
P : constant Queue_Priority := Get_Priority (New_Item);
|
||||
H : constant Node_Access := List.Header'Unchecked_Access;
|
||||
|
||||
Node : Node_Access;
|
||||
Prev : Node_Access;
|
||||
function Next return Node_Access;
|
||||
-- The node before which we wish to insert the new node
|
||||
|
||||
----------
|
||||
-- Next --
|
||||
----------
|
||||
|
||||
function Next return Node_Access is
|
||||
begin
|
||||
return Result : Node_Access := H.Next_Unequal do
|
||||
while Result /= H
|
||||
and then not Before (P, Get_Priority (Result.Element))
|
||||
loop
|
||||
Result := Result.Next_Unequal;
|
||||
end loop;
|
||||
end return;
|
||||
end Next;
|
||||
|
||||
-- Local varaibles
|
||||
|
||||
Prev : constant Node_Access := Next.Prev;
|
||||
-- The node after which we wish to insert the new node. So Prev must
|
||||
-- be the header, or be higher or equal priority to the new item.
|
||||
-- Prev.Next must be the header, or be lower priority than the
|
||||
-- new item.
|
||||
|
||||
pragma Assert
|
||||
(Prev = H or else Before_Or_Equal (Get_Priority (Prev.Element), P));
|
||||
pragma Assert
|
||||
(Prev.Next = H
|
||||
or else Before (P, Get_Priority (Prev.Next.Element)));
|
||||
pragma Assert (Prev.Next = Prev.Next_Unequal);
|
||||
|
||||
Node : constant Node_Access :=
|
||||
new Node_Type'(New_Item,
|
||||
Prev => Prev,
|
||||
Next => Prev.Next,
|
||||
Next_Unequal => Prev.Next);
|
||||
|
||||
-- Start of processing for Enqueue
|
||||
|
||||
begin
|
||||
Node := new Node_Type'(New_Item, null);
|
||||
Prev.Next.Prev := Node;
|
||||
Prev.Next := Node;
|
||||
|
||||
if List.First = null then
|
||||
List.First := Node;
|
||||
List.Last := List.First;
|
||||
|
||||
else
|
||||
Prev := List.First;
|
||||
|
||||
if Before (P, Get_Priority (Prev.Element)) then
|
||||
Node.Next := List.First;
|
||||
List.First := Node;
|
||||
|
||||
else
|
||||
while Prev.Next /= null loop
|
||||
if Before (P, Get_Priority (Prev.Next.Element)) then
|
||||
Node.Next := Prev.Next;
|
||||
Prev.Next := Node;
|
||||
|
||||
exit;
|
||||
end if;
|
||||
|
||||
Prev := Prev.Next;
|
||||
end loop;
|
||||
|
||||
if Prev.Next = null then
|
||||
List.Last.Next := Node;
|
||||
List.Last := Node;
|
||||
end if;
|
||||
end if;
|
||||
if List.Length = 0 then
|
||||
List.Header.Next_Unequal := Node;
|
||||
end if;
|
||||
|
||||
List.Length := List.Length + 1;
|
||||
|
|
@ -162,12 +203,10 @@ package body Ada.Containers.Unbounded_Priority_Queues is
|
|||
--------------
|
||||
|
||||
procedure Finalize (List : in out List_Type) is
|
||||
X : Node_Access;
|
||||
Ignore : Queue_Interfaces.Element_Type;
|
||||
begin
|
||||
while List.First /= null loop
|
||||
X := List.First;
|
||||
List.First := List.First.Next;
|
||||
Free (X);
|
||||
while List.Length > 0 loop
|
||||
List.Dequeue (Ignore);
|
||||
end loop;
|
||||
end Finalize;
|
||||
|
||||
|
|
|
|||
|
|
@ -81,18 +81,35 @@ package Ada.Containers.Unbounded_Priority_Queues is
|
|||
|
||||
private
|
||||
|
||||
-- List_Type is implemented as a circular doubly-linked list with a
|
||||
-- dummy header node; Prev and Next are the links. The list is in
|
||||
-- decreasing priority order, so the highest-priority item is always
|
||||
-- first. (If there are multiple items with the highest priority, the
|
||||
-- oldest one is first.) Header.Element is undefined and not used.
|
||||
--
|
||||
-- In addition, Next_Unequal points to the next item with a different
|
||||
-- (i.e. strictly lower) priority. This is used to speed up the search
|
||||
-- for the next lower-priority item, in cases where there are many items
|
||||
-- with the same priority.
|
||||
--
|
||||
-- An empty list has Header.Prev, Header.Next, and Header.Next_Unequal
|
||||
-- all pointing to Header. A nonempty list has Header.Next_Unequal
|
||||
-- pointing to the first "real" item, and the last item has Next_Unequal
|
||||
-- pointing back to Header.
|
||||
|
||||
type Node_Type;
|
||||
type Node_Access is access Node_Type;
|
||||
type Node_Access is access all Node_Type;
|
||||
|
||||
type Node_Type is limited record
|
||||
Element : Queue_Interfaces.Element_Type;
|
||||
Next : Node_Access;
|
||||
Element : Queue_Interfaces.Element_Type;
|
||||
Prev, Next : Node_Access := Node_Type'Unchecked_Access;
|
||||
Next_Unequal : Node_Access := Node_Type'Unchecked_Access;
|
||||
end record;
|
||||
|
||||
type List_Type is new Ada.Finalization.Limited_Controlled with record
|
||||
First, Last : Node_Access;
|
||||
Length : Count_Type := 0;
|
||||
Max_Length : Count_Type := 0;
|
||||
Header : aliased Node_Type;
|
||||
Length : Count_Type := 0;
|
||||
Max_Length : Count_Type := 0;
|
||||
end record;
|
||||
|
||||
overriding procedure Finalize (List : in out List_Type);
|
||||
|
|
|
|||
|
|
@ -660,7 +660,6 @@ package body Contracts is
|
|||
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 @@ package body Contracts is
|
|||
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 @@ package body Contracts is
|
|||
|
||||
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 @@ package body Contracts is
|
|||
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;
|
||||
|
||||
-------------------------------------------
|
||||
|
|
|
|||
|
|
@ -9046,110 +9046,6 @@ package body Sem_Util is
|
|||
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 @@ package Sem_Util is
|
|||
-- 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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue