From 6c2e4047faa9d9165fd5a1df47aae79175fdf8f7 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 11 Apr 2013 14:13:49 +0200 Subject: [PATCH] [multiple changes] 2013-04-11 Matthew Heaney * 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 * 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. From-SVN: r197771 --- gcc/ada/ChangeLog | 17 ++ gcc/ada/a-cbdlli.adb | 432 ++++++++++++++++++++++++++++++++++------- gcc/ada/a-cdlili.adb | 453 +++++++++++++++++++++++++++++++------------ gcc/ada/a-cidlli.adb | 450 ++++++++++++++++++++++++++++++------------ gcc/ada/adabkend.adb | 4 +- gcc/ada/gnat1drv.adb | 5 +- gcc/ada/opt.ads | 2 +- 7 files changed, 1056 insertions(+), 307 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 051a222b3f0..0d54e5e135c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2013-04-11 Matthew Heaney + + * 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 + + * 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 * sem_res.adb: Minor code reorganization and comment fixes. diff --git a/gcc/ada/a-cbdlli.adb b/gcc/ada/a-cbdlli.adb index 5db2d58f3d7..1c250223010 100644 --- a/gcc/ada/a-cbdlli.adb +++ b/gcc/ada/a-cbdlli.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -80,6 +80,18 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is 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 @@ -92,10 +104,19 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is --------- 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 @@ -106,18 +127,44 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is 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 "="; -------------- @@ -570,15 +617,43 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is 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; ----------- @@ -753,19 +828,41 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is --------------- 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; ----------- @@ -776,12 +873,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is (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 @@ -799,6 +891,14 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is "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)"; @@ -809,34 +909,69 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is "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; ---------- @@ -926,7 +1061,27 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is "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); @@ -1733,15 +1888,43 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is 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; --------------------- @@ -1800,9 +1983,6 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is 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; @@ -1821,10 +2001,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is "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 @@ -1937,7 +2114,7 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is Source : in out List; Position : in out Cursor) is - Target_Position : Cursor; + Target_Position : Count_Type; begin if Target'Address = Source'Address then @@ -1979,16 +2156,139 @@ package body Ada.Containers.Bounded_Doubly_Linked_Lists is "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 -- ---------- diff --git a/gcc/ada/a-cdlili.adb b/gcc/ada/a-cdlili.adb index 8234f327eb1..2fedd3c3b64 100644 --- a/gcc/ada/a-cdlili.adb +++ b/gcc/ada/a-cdlili.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -64,6 +64,17 @@ package body Ada.Containers.Doubly_Linked_Lists is 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 @@ -76,8 +87,15 @@ package body Ada.Containers.Doubly_Linked_Lists is --------- 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 @@ -88,16 +106,44 @@ package body Ada.Containers.Doubly_Linked_Lists is 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 "="; ------------ @@ -508,15 +554,43 @@ package body Ada.Containers.Doubly_Linked_Lists is 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; ----------- @@ -606,18 +680,39 @@ package body Ada.Containers.Doubly_Linked_Lists is --------------- 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; ----------- @@ -628,10 +723,7 @@ package body Ada.Containers.Doubly_Linked_Lists is (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 @@ -649,6 +741,10 @@ package body Ada.Containers.Doubly_Linked_Lists is "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)"; @@ -659,35 +755,64 @@ package body Ada.Containers.Doubly_Linked_Lists is "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; ---------- @@ -773,7 +898,27 @@ package body Ada.Containers.Doubly_Linked_Lists is "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); @@ -1533,15 +1678,43 @@ package body Ada.Containers.Doubly_Linked_Lists is 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; --------------------- @@ -1600,9 +1773,6 @@ package body Ada.Containers.Doubly_Linked_Lists is 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; @@ -1617,45 +1787,7 @@ package body Ada.Containers.Doubly_Linked_Lists is "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 @@ -1806,10 +1938,95 @@ package body Ada.Containers.Doubly_Linked_Lists is "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; @@ -1818,58 +2035,56 @@ package body Ada.Containers.Doubly_Linked_Lists is 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 -- diff --git a/gcc/ada/a-cidlli.adb b/gcc/ada/a-cidlli.adb index 7d5e22ee80e..458df261c06 100644 --- a/gcc/ada/a-cidlli.adb +++ b/gcc/ada/a-cidlli.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -67,6 +67,17 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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 @@ -79,8 +90,15 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is --------- 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 @@ -91,18 +109,44 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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 "="; ------------ @@ -549,15 +593,43 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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; ----------- @@ -660,18 +732,39 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is --------------- 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; ----------- @@ -682,10 +775,7 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is (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 @@ -703,6 +793,10 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is "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)"; @@ -713,35 +807,63 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is "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; ---------- @@ -825,7 +947,27 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is "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); @@ -1600,15 +1742,43 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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; --------------------- @@ -1673,9 +1843,6 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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; @@ -1690,44 +1857,7 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is "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 @@ -1901,10 +2031,94 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is "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; @@ -1913,58 +2127,56 @@ package body Ada.Containers.Indefinite_Doubly_Linked_Lists is 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 -- diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb index 96bd00d99df..e8087623681 100644 --- a/gcc/ada/adabkend.adb +++ b/gcc/ada/adabkend.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -234,6 +234,8 @@ package body Adabkend is 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; diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index cd0d6504d2b..69d37ad0f4f 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -293,7 +293,10 @@ procedure Gnat1drv is 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 diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index 5e80dc76fe1..5653c762fe3 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1982,7 +1982,7 @@ package Opt is 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 -- 2.30.2