+2013-04-11 Matthew Heaney <heaney@adacore.com>
+
+ * a-cdlili.adb, a-cidlli.adb, a-cbdlli.adb ("="): Increment
+ lock counts before entering loop.
+ (Find): Ditto.
+ (Is_Sorted, Merge, Sort): Ditto.
+ (Reverse_Find): Ditto.
+ (Splice_Internal): Internal operation to refactor splicing logic.
+ (Splice): Some logic moved into Splice_Internal.
+
+2013-04-11 Johannes Kanig <kanig@adacore.com>
+
+ * adabkend.adb (Scan_Compiler_Arguments): Do not call
+ Set_Output_Object_File_Name in Alfa_Mode
+ * gnat1drv.adb (Adjust_Global_Switches): Take Alfa_Mode into account.
+ * opt.ads: Fix documentation.
+
2013-04-11 Robert Dewar <dewar@adacore.com>
* sem_res.adb: Minor code reorganization and comment fixes.
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, 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- --
Before : Count_Type;
New_Node : Count_Type);
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Count_Type;
+ Source : in out List);
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Count_Type;
+ Source : in out List;
+ Src_Pos : Count_Type;
+ Tgt_Pos : out Count_Type);
+
function Vet (Position : Cursor) return Boolean;
-- Checks invariants of the cursor and its designated container, as a
-- simple way of detecting dangling references (see operation Free for a
---------
function "=" (Left, Right : List) return Boolean is
+ BL : Natural renames Left'Unrestricted_Access.Busy;
+ LL : Natural renames Left'Unrestricted_Access.Lock;
+
+ BR : Natural renames Right'Unrestricted_Access.Busy;
+ LR : Natural renames Right'Unrestricted_Access.Lock;
+
LN : Node_Array renames Left.Nodes;
RN : Node_Array renames Right.Nodes;
- LI, RI : Count_Type;
+ LI : Count_Type;
+ RI : Count_Type;
+
+ Result : Boolean;
begin
if Left'Address = Right'Address then
return False;
end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ BL := BL + 1;
+ LL := LL + 1;
+
+ BR := BR + 1;
+ LR := LR + 1;
+
LI := Left.First;
RI := Right.First;
+ Result := True;
for J in 1 .. Left.Length loop
if LN (LI).Element /= RN (RI).Element then
- return False;
+ Result := False;
+ exit;
end if;
LI := LN (LI).Next;
RI := RN (RI).Next;
end loop;
- return True;
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ return Result;
+ exception
+ when others =>
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ raise;
end "=";
--------------
pragma Assert (Vet (Position), "bad cursor in Find");
end if;
- while Node /= 0 loop
- if Nodes (Node).Element = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Nodes (Node).Next;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Count_Type;
+
+ begin
+ B := B + 1;
+ L := L + 1;
- return No_Element;
+ Result := 0;
+ while Node /= 0 loop
+ if Nodes (Node).Element = Item then
+ Result := Node;
+ exit;
+ end if;
+
+ Node := Nodes (Node).Next;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
+
+ if Result = 0 then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Find;
-----------
---------------
function Is_Sorted (Container : List) return Boolean is
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
Nodes : Node_Array renames Container.Nodes;
- Node : Count_Type := Container.First;
+ Node : Count_Type;
+
+ Result : Boolean;
begin
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ B := B + 1;
+ L := L + 1;
+
+ Node := Container.First;
+ Result := True;
for J in 2 .. Container.Length loop
if Nodes (Nodes (Node).Next).Element < Nodes (Node).Element then
- return False;
+ Result := False;
+ exit;
end if;
Node := Nodes (Node).Next;
end loop;
- return True;
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
end Is_Sorted;
-----------
(Target : in out List;
Source : in out List)
is
- LN : Node_Array renames Target.Nodes;
- RN : Node_Array renames Source.Nodes;
- LI, RI : Cursor;
-
begin
-
-- The semantics of Merge changed slightly per AI05-0021. It was
-- originally the case that if Target and Source denoted the same
-- container object, then the GNAT implementation of Merge did
"Target and Source denote same non-empty container";
end if;
+ if Target.Length > Count_Type'Last - Source.Length then
+ raise Constraint_Error with "new length exceeds maximum";
+ end if;
+
+ if Target.Length + Source.Length > Target.Capacity then
+ raise Capacity_Error with "new length exceeds target capacity";
+ end if;
+
if Target.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors of Target (list is busy)";
"attempt to tamper with cursors of Source (list is busy)";
end if;
- LI := First (Target);
- RI := First (Source);
- while RI.Node /= 0 loop
- pragma Assert (RN (RI.Node).Next = 0
- or else not (RN (RN (RI.Node).Next).Element <
- RN (RI.Node).Element));
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- if LI.Node = 0 then
- Splice (Target, No_Element, Source);
- return;
- end if;
+ declare
+ TB : Natural renames Target.Busy;
+ TL : Natural renames Target.Lock;
- pragma Assert (LN (LI.Node).Next = 0
- or else not (LN (LN (LI.Node).Next).Element <
- LN (LI.Node).Element));
+ SB : Natural renames Source.Busy;
+ SL : Natural renames Source.Lock;
- if RN (RI.Node).Element < LN (LI.Node).Element then
- declare
- RJ : Cursor := RI;
- begin
- RI.Node := RN (RI.Node).Next;
- Splice (Target, LI, Source, RJ);
- end;
+ LN : Node_Array renames Target.Nodes;
+ RN : Node_Array renames Source.Nodes;
- else
- LI.Node := LN (LI.Node).Next;
- end if;
- end loop;
+ LI, LJ, RI, RJ : Count_Type;
+
+ begin
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ LI := Target.First;
+ RI := Source.First;
+ while RI /= 0 loop
+ pragma Assert (RN (RI).Next = 0
+ or else not (RN (RN (RI).Next).Element <
+ RN (RI).Element));
+
+ if LI = 0 then
+ Splice_Internal (Target, 0, Source);
+ exit;
+ end if;
+
+ pragma Assert (LN (LI).Next = 0
+ or else not (LN (LN (LI).Next).Element <
+ LN (LI).Element));
+
+ if RN (RI).Element < LN (LI).Element then
+ RJ := RI;
+ RI := RN (RI).Next;
+ Splice_Internal (Target, LI, Source, RJ, LJ);
+
+ else
+ LI := LN (LI).Next;
+ end if;
+ end loop;
+
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+ exception
+ when others =>
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+
+ raise;
+ end;
end Merge;
----------
"attempt to tamper with cursors (list is busy)";
end if;
- Sort (Front => 0, Back => 0);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ declare
+ B : Natural renames Container.Busy;
+ L : Natural renames Container.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Sort (Front => 0, Back => 0);
+
+ B := B - 1;
+ L := L - 1;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
pragma Assert (N (Container.First).Prev = 0);
pragma Assert (N (Container.Last).Next = 0);
pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
end if;
- while Node /= 0 loop
- if Container.Nodes (Node).Element = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Container.Nodes (Node).Prev;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Count_Type;
- return No_Element;
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := 0;
+ while Node /= 0 loop
+ if Container.Nodes (Node).Element = Item then
+ Result := Node;
+ exit;
+ end if;
+
+ Node := Container.Nodes (Node).Prev;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
+
+ if Result = 0 then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Reverse_Find;
---------------------
return;
end if;
- pragma Assert (Source.Nodes (Source.First).Prev = 0);
- pragma Assert (Source.Nodes (Source.Last).Next = 0);
-
if Target.Length > Count_Type'Last - Source.Length then
raise Constraint_Error with "new length exceeds maximum";
end if;
"attempt to tamper with cursors of Source (list is busy)";
end if;
- while not Is_Empty (Source) loop
- Insert (Target, Before, Source.Nodes (Source.First).Element);
- Delete_First (Source);
- end loop;
+ Splice_Internal (Target, Before.Node, Source);
end Splice;
procedure Splice
Source : in out List;
Position : in out Cursor)
is
- Target_Position : Cursor;
+ Target_Position : Count_Type;
begin
if Target'Address = Source'Address then
"attempt to tamper with cursors of Source (list is busy)";
end if;
- Insert
- (Container => Target,
- Before => Before,
- New_Item => Source.Nodes (Position.Node).Element,
- Position => Target_Position);
+ Splice_Internal
+ (Target => Target,
+ Before => Before.Node,
+ Source => Source,
+ Src_Pos => Position.Node,
+ Tgt_Pos => Target_Position);
- Delete (Source, Position);
- Position := Target_Position;
+ Position := Cursor'(Target'Unrestricted_Access, Target_Position);
end Splice;
+ ---------------------
+ -- Splice_Internal --
+ ---------------------
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Count_Type;
+ Source : in out List)
+ is
+ N : Node_Array renames Source.Nodes;
+ X : Count_Type;
+
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted, and corner-cases disposed of.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= 0);
+ pragma Assert (N (Source.First).Prev = 0);
+ pragma Assert (Source.Last /= 0);
+ pragma Assert (N (Source.Last).Next = 0);
+ pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+ pragma Assert (Target.Length + Source.Length <= Target.Capacity);
+
+ while Source.Length > 1 loop
+ -- Copy first element of Source onto Target
+
+ Allocate (Target, N (Source.First).Element, New_Node => X);
+ Insert_Internal (Target, Before => Before, New_Node => X);
+
+ -- Unlink the first node from Source
+
+ X := Source.First;
+ pragma Assert (N (N (X).Next).Prev = X);
+
+ Source.First := N (X).Next;
+ N (Source.First).Prev := 0;
+
+ Source.Length := Source.Length - 1;
+
+ -- Return the Source node to its free store
+
+ Free (Source, X);
+ end loop;
+
+ -- Copy first (and only remaining) element of Source onto Target
+
+ Allocate (Target, N (Source.First).Element, New_Node => X);
+ Insert_Internal (Target, Before => Before, New_Node => X);
+
+ -- Unlink the node from Source
+
+ X := Source.First;
+ pragma Assert (X = Source.Last);
+
+ Source.First := 0;
+ Source.Last := 0;
+
+ Source.Length := 0;
+
+ -- Return the Source node to its free store
+
+ Free (Source, X);
+ end Splice_Internal;
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Count_Type; -- node of Target
+ Source : in out List;
+ Src_Pos : Count_Type; -- node of Source
+ Tgt_Pos : out Count_Type)
+ is
+ N : Node_Array renames Source.Nodes;
+
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted, and corner-cases handled.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Target.Length < Target.Capacity);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= 0);
+ pragma Assert (N (Source.First).Prev = 0);
+ pragma Assert (Source.Last /= 0);
+ pragma Assert (N (Source.Last).Next = 0);
+ pragma Assert (Src_Pos /= 0);
+
+ Allocate (Target, N (Src_Pos).Element, New_Node => Tgt_Pos);
+ Insert_Internal (Target, Before => Before, New_Node => Tgt_Pos);
+
+ if Source.Length = 1 then
+ pragma Assert (Source.First = Source.Last);
+ pragma Assert (Src_Pos = Source.First);
+
+ Source.First := 0;
+ Source.Last := 0;
+
+ elsif Src_Pos = Source.First then
+ pragma Assert (N (N (Src_Pos).Next).Prev = Src_Pos);
+
+ Source.First := N (Src_Pos).Next;
+ N (Source.First).Prev := 0;
+
+ elsif Src_Pos = Source.Last then
+ pragma Assert (N (N (Src_Pos).Prev).Next = Src_Pos);
+
+ Source.Last := N (Src_Pos).Prev;
+ N (Source.Last).Next := 0;
+
+ else
+ pragma Assert (Source.Length >= 3);
+ pragma Assert (N (N (Src_Pos).Next).Prev = Src_Pos);
+ pragma Assert (N (N (Src_Pos).Prev).Next = Src_Pos);
+
+ N (N (Src_Pos).Next).Prev := N (Src_Pos).Prev;
+ N (N (Src_Pos).Prev).Next := N (Src_Pos).Next;
+ end if;
+
+ Source.Length := Source.Length - 1;
+ Free (Source, Src_Pos);
+ end Splice_Internal;
+
----------
-- Swap --
----------
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, 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- --
Before : Node_Access;
New_Node : Node_Access);
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List);
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List;
+ Position : Node_Access);
+
function Vet (Position : Cursor) return Boolean;
-- Checks invariants of the cursor and its designated container, as a
-- simple way of detecting dangling references (see operation Free for a
---------
function "=" (Left, Right : List) return Boolean is
- L : Node_Access := Left.First;
- R : Node_Access := Right.First;
+ BL : Natural renames Left'Unrestricted_Access.Busy;
+ LL : Natural renames Left'Unrestricted_Access.Lock;
+
+ BR : Natural renames Right'Unrestricted_Access.Busy;
+ LR : Natural renames Right'Unrestricted_Access.Lock;
+
+ L : Node_Access;
+ R : Node_Access;
+ Result : Boolean;
begin
if Left'Address = Right'Address then
return False;
end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ BL := BL + 1;
+ LL := LL + 1;
+
+ BR := BR + 1;
+ LR := LR + 1;
+
+ L := Left.First;
+ R := Right.First;
+ Result := True;
for J in 1 .. Left.Length loop
if L.Element /= R.Element then
- return False;
+ Result := False;
+ exit;
end if;
L := L.Next;
R := R.Next;
end loop;
- return True;
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ return Result;
+ exception
+ when others =>
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ raise;
end "=";
------------
pragma Assert (Vet (Position), "bad cursor in Find");
end if;
- while Node /= null loop
- if Node.Element = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Node.Next;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Node_Access;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := null;
+ while Node /= null loop
+ if Node.Element = Item then
+ Result := Node;
+ exit;
+ end if;
+
+ Node := Node.Next;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
- return No_Element;
+ if Result = null then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Find;
-----------
---------------
function Is_Sorted (Container : List) return Boolean is
- Node : Node_Access := Container.First;
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Node : Node_Access;
+ Result : Boolean;
begin
- for I in 2 .. Container.Length loop
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ B := B + 1;
+ L := L + 1;
+
+ Node := Container.First;
+ Result := True;
+ for Idx in 2 .. Container.Length loop
if Node.Next.Element < Node.Element then
- return False;
+ Result := False;
+ exit;
end if;
Node := Node.Next;
end loop;
- return True;
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
end Is_Sorted;
-----------
(Target : in out List;
Source : in out List)
is
- LI, RI : Cursor;
-
begin
-
-- The semantics of Merge changed slightly per AI05-0021. It was
-- originally the case that if Target and Source denoted the same
-- container object, then the GNAT implementation of Merge did
"Target and Source denote same non-empty container";
end if;
+ if Target.Length > Count_Type'Last - Source.Length then
+ raise Constraint_Error with "new length exceeds maximum";
+ end if;
+
if Target.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors of Target (list is busy)";
"attempt to tamper with cursors of Source (list is busy)";
end if;
- LI := First (Target);
- RI := First (Source);
- while RI.Node /= null loop
- pragma Assert (RI.Node.Next = null
- or else not (RI.Node.Next.Element <
- RI.Node.Element));
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- if LI.Node = null then
- Splice (Target, No_Element, Source);
- return;
- end if;
+ declare
+ TB : Natural renames Target.Busy;
+ TL : Natural renames Target.Lock;
- pragma Assert (LI.Node.Next = null
- or else not (LI.Node.Next.Element <
- LI.Node.Element));
+ SB : Natural renames Source.Busy;
+ SL : Natural renames Source.Lock;
- if RI.Node.Element < LI.Node.Element then
- declare
- RJ : Cursor := RI;
- pragma Warnings (Off, RJ);
- begin
- RI.Node := RI.Node.Next;
- Splice (Target, LI, Source, RJ);
- end;
+ LI, RI, RJ : Node_Access;
- else
- LI.Node := LI.Node.Next;
- end if;
- end loop;
+ begin
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ LI := Target.First;
+ RI := Source.First;
+ while RI /= null loop
+ pragma Assert (RI.Next = null
+ or else not (RI.Next.Element < RI.Element));
+
+ if LI = null then
+ Splice_Internal (Target, null, Source);
+ exit;
+ end if;
+
+ pragma Assert (LI.Next = null
+ or else not (LI.Next.Element < LI.Element));
+
+ if RI.Element < LI.Element then
+ RJ := RI;
+ RI := RI.Next;
+ Splice_Internal (Target, LI, Source, RJ);
+
+ else
+ LI := LI.Next;
+ end if;
+ end loop;
+
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+ exception
+ when others =>
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+
+ raise;
+ end;
end Merge;
----------
"attempt to tamper with cursors (list is busy)";
end if;
- Sort (Front => null, Back => null);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ declare
+ B : Natural renames Container.Busy;
+ L : Natural renames Container.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Sort (Front => null, Back => null);
+
+ B := B - 1;
+ L := L - 1;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
pragma Assert (Container.First.Prev = null);
pragma Assert (Container.Last.Next = null);
pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
end if;
- while Node /= null loop
- if Node.Element = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Node.Prev;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Node_Access;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := null;
+ while Node /= null loop
+ if Node.Element = Item then
+ Result := Node;
+ exit;
+ end if;
- return No_Element;
+ Node := Node.Prev;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
+
+ if Result = null then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Reverse_Find;
---------------------
return;
end if;
- pragma Assert (Source.First.Prev = null);
- pragma Assert (Source.Last.Next = null);
-
if Target.Length > Count_Type'Last - Source.Length then
raise Constraint_Error with "new length exceeds maximum";
end if;
"attempt to tamper with cursors of Source (list is busy)";
end if;
- if Target.Length = 0 then
- pragma Assert (Target.First = null);
- pragma Assert (Target.Last = null);
- pragma Assert (Before = No_Element);
-
- Target.First := Source.First;
- Target.Last := Source.Last;
-
- elsif Before.Node = null then
- pragma Assert (Target.Last.Next = null);
-
- Target.Last.Next := Source.First;
- Source.First.Prev := Target.Last;
-
- Target.Last := Source.Last;
-
- elsif Before.Node = Target.First then
- pragma Assert (Target.First.Prev = null);
-
- Source.Last.Next := Target.First;
- Target.First.Prev := Source.Last;
-
- Target.First := Source.First;
-
- else
- pragma Assert (Target.Length >= 2);
-
- Before.Node.Prev.Next := Source.First;
- Source.First.Prev := Before.Node.Prev;
-
- Before.Node.Prev := Source.Last;
- Source.Last.Next := Before.Node;
- end if;
-
- Source.First := null;
- Source.Last := null;
-
- Target.Length := Target.Length + Source.Length;
- Source.Length := 0;
+ Splice_Internal (Target, Before.Node, Source);
end Splice;
procedure Splice
"attempt to tamper with cursors of Source (list is busy)";
end if;
- if Position.Node = Source.First then
- Source.First := Position.Node.Next;
+ Splice_Internal (Target, Before.Node, Source, Position.Node);
+ Position.Container := Target'Unchecked_Access;
+ end Splice;
+
+ ---------------------
+ -- Splice_Internal --
+ ---------------------
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List)
+ is
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted, and corner-cases disposed of.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= null);
+ pragma Assert (Source.First.Prev = null);
+ pragma Assert (Source.Last /= null);
+ pragma Assert (Source.Last.Next = null);
+ pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+
+ if Target.Length = 0 then
+ pragma Assert (Target.First = null);
+ pragma Assert (Target.Last = null);
+ pragma Assert (Before = null);
+
+ Target.First := Source.First;
+ Target.Last := Source.Last;
+
+ elsif Before = null then
+ pragma Assert (Target.Last.Next = null);
+
+ Target.Last.Next := Source.First;
+ Source.First.Prev := Target.Last;
+
+ Target.Last := Source.Last;
+
+ elsif Before = Target.First then
+ pragma Assert (Target.First.Prev = null);
+
+ Source.Last.Next := Target.First;
+ Target.First.Prev := Source.Last;
+
+ Target.First := Source.First;
+
+ else
+ pragma Assert (Target.Length >= 2);
+
+ Before.Prev.Next := Source.First;
+ Source.First.Prev := Before.Prev;
+
+ Before.Prev := Source.Last;
+ Source.Last.Next := Before;
+ end if;
+
+ Source.First := null;
+ Source.Last := null;
+
+ Target.Length := Target.Length + Source.Length;
+ Source.Length := 0;
+ end Splice_Internal;
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access; -- node of Target
+ Source : in out List;
+ Position : Node_Access) -- node of Source
+ is
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Target.Length < Count_Type'Last);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= null);
+ pragma Assert (Source.First.Prev = null);
+ pragma Assert (Source.Last /= null);
+ pragma Assert (Source.Last.Next = null);
+ pragma Assert (Position /= null);
+
+ if Position = Source.First then
+ Source.First := Position.Next;
- if Position.Node = Source.Last then
+ if Position = Source.Last then
pragma Assert (Source.First = null);
pragma Assert (Source.Length = 1);
Source.Last := null;
Source.First.Prev := null;
end if;
- elsif Position.Node = Source.Last then
+ elsif Position = Source.Last then
pragma Assert (Source.Length >= 2);
- Source.Last := Position.Node.Prev;
+ Source.Last := Position.Prev;
Source.Last.Next := null;
else
pragma Assert (Source.Length >= 3);
- Position.Node.Prev.Next := Position.Node.Next;
- Position.Node.Next.Prev := Position.Node.Prev;
+ Position.Prev.Next := Position.Next;
+ Position.Next.Prev := Position.Prev;
end if;
if Target.Length = 0 then
pragma Assert (Target.First = null);
pragma Assert (Target.Last = null);
- pragma Assert (Before = No_Element);
+ pragma Assert (Before = null);
- Target.First := Position.Node;
- Target.Last := Position.Node;
+ Target.First := Position;
+ Target.Last := Position;
Target.First.Prev := null;
Target.Last.Next := null;
- elsif Before.Node = null then
+ elsif Before = null then
pragma Assert (Target.Last.Next = null);
- Target.Last.Next := Position.Node;
- Position.Node.Prev := Target.Last;
+ Target.Last.Next := Position;
+ Position.Prev := Target.Last;
- Target.Last := Position.Node;
+ Target.Last := Position;
Target.Last.Next := null;
- elsif Before.Node = Target.First then
+ elsif Before = Target.First then
pragma Assert (Target.First.Prev = null);
- Target.First.Prev := Position.Node;
- Position.Node.Next := Target.First;
+ Target.First.Prev := Position;
+ Position.Next := Target.First;
- Target.First := Position.Node;
+ Target.First := Position;
Target.First.Prev := null;
else
pragma Assert (Target.Length >= 2);
- Before.Node.Prev.Next := Position.Node;
- Position.Node.Prev := Before.Node.Prev;
+ Before.Prev.Next := Position;
+ Position.Prev := Before.Prev;
- Before.Node.Prev := Position.Node;
- Position.Node.Next := Before.Node;
+ Before.Prev := Position;
+ Position.Next := Before;
end if;
Target.Length := Target.Length + 1;
Source.Length := Source.Length - 1;
-
- Position.Container := Target'Unchecked_Access;
- end Splice;
+ end Splice_Internal;
----------
-- Swap --
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, 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- --
Before : Node_Access;
New_Node : Node_Access);
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List);
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List;
+ Position : Node_Access);
+
function Vet (Position : Cursor) return Boolean;
-- Checks invariants of the cursor and its designated container, as a
-- simple way of detecting dangling references (see operation Free for a
---------
function "=" (Left, Right : List) return Boolean is
- L : Node_Access;
- R : Node_Access;
+ BL : Natural renames Left'Unrestricted_Access.Busy;
+ LL : Natural renames Left'Unrestricted_Access.Lock;
+
+ BR : Natural renames Right'Unrestricted_Access.Busy;
+ LR : Natural renames Right'Unrestricted_Access.Lock;
+
+ L : Node_Access;
+ R : Node_Access;
+ Result : Boolean;
begin
if Left'Address = Right'Address then
return False;
end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ BL := BL + 1;
+ LL := LL + 1;
+
+ BR := BR + 1;
+ LR := LR + 1;
+
L := Left.First;
R := Right.First;
+ Result := True;
for J in 1 .. Left.Length loop
if L.Element.all /= R.Element.all then
- return False;
+ Result := False;
+ exit;
end if;
L := L.Next;
R := R.Next;
end loop;
- return True;
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ return Result;
+ exception
+ when others =>
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ raise;
end "=";
------------
pragma Assert (Vet (Position), "bad cursor in Find");
end if;
- while Node /= null loop
- if Node.Element.all = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Node.Next;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Node_Access;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := null;
+ while Node /= null loop
+ if Node.Element.all = Item then
+ Result := Node;
+ exit;
+ end if;
- return No_Element;
+ Node := Node.Next;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
+
+ if Result = null then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Find;
-----------
---------------
function Is_Sorted (Container : List) return Boolean is
- Node : Node_Access := Container.First;
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Node : Node_Access;
+ Result : Boolean;
begin
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ B := B + 1;
+ L := L + 1;
+
+ Node := Container.First;
+ Result := True;
for I in 2 .. Container.Length loop
if Node.Next.Element.all < Node.Element.all then
- return False;
+ Result := False;
+ exit;
end if;
Node := Node.Next;
end loop;
- return True;
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
end Is_Sorted;
-----------
(Target : in out List;
Source : in out List)
is
- LI, RI : Cursor;
-
begin
-
-- The semantics of Merge changed slightly per AI05-0021. It was
-- originally the case that if Target and Source denoted the same
-- container object, then the GNAT implementation of Merge did
"Target and Source denote same non-empty container";
end if;
+ if Target.Length > Count_Type'Last - Source.Length then
+ raise Constraint_Error with "new length exceeds maximum";
+ end if;
+
if Target.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors of Target (list is busy)";
"attempt to tamper with cursors of Source (list is busy)";
end if;
- LI := First (Target);
- RI := First (Source);
- while RI.Node /= null loop
- pragma Assert (RI.Node.Next = null
- or else not (RI.Node.Next.Element.all <
- RI.Node.Element.all));
+ declare
+ TB : Natural renames Target.Busy;
+ TL : Natural renames Target.Lock;
- if LI.Node = null then
- Splice (Target, No_Element, Source);
- return;
- end if;
+ SB : Natural renames Source.Busy;
+ SL : Natural renames Source.Lock;
- pragma Assert (LI.Node.Next = null
- or else not (LI.Node.Next.Element.all <
- LI.Node.Element.all));
-
- if RI.Node.Element.all < LI.Node.Element.all then
- declare
- RJ : Cursor := RI;
- pragma Warnings (Off, RJ);
- begin
- RI.Node := RI.Node.Next;
- Splice (Target, LI, Source, RJ);
- end;
-
- else
- LI.Node := LI.Node.Next;
- end if;
- end loop;
+ LI, RI, RJ : Node_Access;
+
+ begin
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ LI := Target.First;
+ RI := Source.First;
+ while RI /= null loop
+ pragma Assert (RI.Next = null
+ or else not (RI.Next.Element.all <
+ RI.Element.all));
+
+ if LI = null then
+ Splice_Internal (Target, null, Source);
+ exit;
+ end if;
+
+ pragma Assert (LI.Next = null
+ or else not (LI.Next.Element.all <
+ LI.Element.all));
+
+ if RI.Element.all < LI.Element.all then
+ RJ := RI;
+ RI := RI.Next;
+ Splice_Internal (Target, LI, Source, RJ);
+
+ else
+ LI := LI.Next;
+ end if;
+ end loop;
+
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+ exception
+ when others =>
+ TB := TB - 1;
+ TL := TL - 1;
+
+ SB := SB - 1;
+ SL := SL - 1;
+
+ raise;
+ end;
end Merge;
----------
"attempt to tamper with cursors (list is busy)";
end if;
- Sort (Front => null, Back => null);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ declare
+ B : Natural renames Container.Busy;
+ L : Natural renames Container.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Sort (Front => null, Back => null);
+
+ B := B - 1;
+ L := L - 1;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
pragma Assert (Container.First.Prev = null);
pragma Assert (Container.Last.Next = null);
pragma Assert (Vet (Position), "bad cursor in Reverse_Find");
end if;
- while Node /= null loop
- if Node.Element.all = Item then
- return Cursor'(Container'Unrestricted_Access, Node);
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
- Node := Node.Prev;
- end loop;
+ declare
+ B : Natural renames Container'Unrestricted_Access.Busy;
+ L : Natural renames Container'Unrestricted_Access.Lock;
+
+ Result : Node_Access;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := null;
+ while Node /= null loop
+ if Node.Element.all = Item then
+ Result := Node;
+ exit;
+ end if;
- return No_Element;
+ Node := Node.Prev;
+ end loop;
+
+ B := B - 1;
+ L := L - 1;
+
+ if Result = null then
+ return No_Element;
+ else
+ return Cursor'(Container'Unrestricted_Access, Result);
+ end if;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+ raise;
+ end;
end Reverse_Find;
---------------------
return;
end if;
- pragma Assert (Source.First.Prev = null);
- pragma Assert (Source.Last.Next = null);
-
if Target.Length > Count_Type'Last - Source.Length then
raise Constraint_Error with "new length exceeds maximum";
end if;
"attempt to tamper with cursors of Source (list is busy)";
end if;
- if Target.Length = 0 then
- pragma Assert (Before = No_Element);
- pragma Assert (Target.First = null);
- pragma Assert (Target.Last = null);
-
- Target.First := Source.First;
- Target.Last := Source.Last;
-
- elsif Before.Node = null then
- pragma Assert (Target.Last.Next = null);
-
- Target.Last.Next := Source.First;
- Source.First.Prev := Target.Last;
-
- Target.Last := Source.Last;
-
- elsif Before.Node = Target.First then
- pragma Assert (Target.First.Prev = null);
-
- Source.Last.Next := Target.First;
- Target.First.Prev := Source.Last;
-
- Target.First := Source.First;
-
- else
- pragma Assert (Target.Length >= 2);
- Before.Node.Prev.Next := Source.First;
- Source.First.Prev := Before.Node.Prev;
-
- Before.Node.Prev := Source.Last;
- Source.Last.Next := Before.Node;
- end if;
-
- Source.First := null;
- Source.Last := null;
-
- Target.Length := Target.Length + Source.Length;
- Source.Length := 0;
+ Splice_Internal (Target, Before.Node, Source);
end Splice;
procedure Splice
"attempt to tamper with cursors of Source (list is busy)";
end if;
- if Position.Node = Source.First then
- Source.First := Position.Node.Next;
+ Splice_Internal (Target, Before.Node, Source, Position.Node);
+ Position.Container := Target'Unchecked_Access;
+ end Splice;
+
+ ---------------------
+ -- Splice_Internal --
+ ---------------------
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access;
+ Source : in out List)
+ is
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted, and corner-cases disposed of.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= null);
+ pragma Assert (Source.First.Prev = null);
+ pragma Assert (Source.Last /= null);
+ pragma Assert (Source.Last.Next = null);
+ pragma Assert (Target.Length <= Count_Type'Last - Source.Length);
+
+ if Target.Length = 0 then
+ pragma Assert (Before = null);
+ pragma Assert (Target.First = null);
+ pragma Assert (Target.Last = null);
+
+ Target.First := Source.First;
+ Target.Last := Source.Last;
+
+ elsif Before = null then
+ pragma Assert (Target.Last.Next = null);
+
+ Target.Last.Next := Source.First;
+ Source.First.Prev := Target.Last;
+
+ Target.Last := Source.Last;
+
+ elsif Before = Target.First then
+ pragma Assert (Target.First.Prev = null);
+
+ Source.Last.Next := Target.First;
+ Target.First.Prev := Source.Last;
+
+ Target.First := Source.First;
+
+ else
+ pragma Assert (Target.Length >= 2);
+ Before.Prev.Next := Source.First;
+ Source.First.Prev := Before.Prev;
+
+ Before.Prev := Source.Last;
+ Source.Last.Next := Before;
+ end if;
+
+ Source.First := null;
+ Source.Last := null;
+
+ Target.Length := Target.Length + Source.Length;
+ Source.Length := 0;
+ end Splice_Internal;
+
+ procedure Splice_Internal
+ (Target : in out List;
+ Before : Node_Access; -- node of Target
+ Source : in out List;
+ Position : Node_Access) -- node of Source
+ is
+ begin
+ -- This implements the corresponding Splice operation, after the
+ -- parameters have been vetted.
+
+ pragma Assert (Target'Address /= Source'Address);
+ pragma Assert (Target.Length < Count_Type'Last);
+ pragma Assert (Source.Length > 0);
+ pragma Assert (Source.First /= null);
+ pragma Assert (Source.First.Prev = null);
+ pragma Assert (Source.Last /= null);
+ pragma Assert (Source.Last.Next = null);
+ pragma Assert (Position /= null);
+
+ if Position = Source.First then
+ Source.First := Position.Next;
- if Position.Node = Source.Last then
+ if Position = Source.Last then
pragma Assert (Source.First = null);
pragma Assert (Source.Length = 1);
Source.Last := null;
Source.First.Prev := null;
end if;
- elsif Position.Node = Source.Last then
+ elsif Position = Source.Last then
pragma Assert (Source.Length >= 2);
- Source.Last := Position.Node.Prev;
+ Source.Last := Position.Prev;
Source.Last.Next := null;
else
pragma Assert (Source.Length >= 3);
- Position.Node.Prev.Next := Position.Node.Next;
- Position.Node.Next.Prev := Position.Node.Prev;
+ Position.Prev.Next := Position.Next;
+ Position.Next.Prev := Position.Prev;
end if;
if Target.Length = 0 then
- pragma Assert (Before = No_Element);
+ pragma Assert (Before = null);
pragma Assert (Target.First = null);
pragma Assert (Target.Last = null);
- Target.First := Position.Node;
- Target.Last := Position.Node;
+ Target.First := Position;
+ Target.Last := Position;
Target.First.Prev := null;
Target.Last.Next := null;
- elsif Before.Node = null then
+ elsif Before = null then
pragma Assert (Target.Last.Next = null);
- Target.Last.Next := Position.Node;
- Position.Node.Prev := Target.Last;
+ Target.Last.Next := Position;
+ Position.Prev := Target.Last;
- Target.Last := Position.Node;
+ Target.Last := Position;
Target.Last.Next := null;
- elsif Before.Node = Target.First then
+ elsif Before = Target.First then
pragma Assert (Target.First.Prev = null);
- Target.First.Prev := Position.Node;
- Position.Node.Next := Target.First;
+ Target.First.Prev := Position;
+ Position.Next := Target.First;
- Target.First := Position.Node;
+ Target.First := Position;
Target.First.Prev := null;
else
pragma Assert (Target.Length >= 2);
- Before.Node.Prev.Next := Position.Node;
- Position.Node.Prev := Before.Node.Prev;
+ Before.Prev.Next := Position;
+ Position.Prev := Before.Prev;
- Before.Node.Prev := Position.Node;
- Position.Node.Next := Before.Node;
+ Before.Prev := Position;
+ Position.Next := Before;
end if;
Target.Length := Target.Length + 1;
Source.Length := Source.Length - 1;
-
- Position.Container := Target'Unchecked_Access;
- end Splice;
+ end Splice_Internal;
----------
-- Swap --
-- --
-- B o d y --
-- --
--- Copyright (C) 2001-2011, AdaCore --
+-- Copyright (C) 2001-2013, AdaCore --
-- --
-- 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- --
then
if Is_Switch (Argv) then
Fail ("Object file name missing after -gnatO");
+ elsif Alfa_Mode then
+ Output_File_Name_Seen := True;
else
Set_Output_Object_File_Name (Argv);
Output_File_Name_Seen := True;
Formal_Extensions := True;
end if;
- if Debug_Flag_Dot_FF then
+ -- Alfa_Mode is activated by default in the gnat2why executable, but
+ -- can also be activated using the -gnatd.F switch.
+
+ if Debug_Flag_Dot_FF or else Alfa_Mode then
Alfa_Mode := True;
-- Set strict standard interpretation of compiler permissions
Alfa_Mode : Boolean := False;
-- Specific compiling mode targeting formal verification through the
-- generation of Why code for those parts of the input code that belong to
- -- the Alfa subset of Ada. Set by debug flag -gnatd.F.
+ -- the Alfa subset of Ada. Set by the gnat2why executable.
Frame_Condition_Mode : Boolean := False;
-- Specific mode to be used in combination with Alfa_Mode. If set to