+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cfdlli.adb, a-cfdlli.ads (Formal_Model): Adapt to
+ modifications in functional containers.
+ * a-cofuba.ads, a-cofuma.ads, a-cofuse.ads, a-cofuve.ads Reformat
+ to improve readablity. Subprograms are separated between basic
+ operations, constructors and properties. Universally quantified
+ formulas in contracts are factorized in independant functions
+ with a name and a comment. Names of parameters are improved.
+
+2017-04-27 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_spark.adb, sem_elab.adb: Minor reformatting and typo fix.
+
+2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_res.adb (Resolve_Type_Conversion): Do not
+ install a predicate check here since this is already done during
+ the expansion phase. Verify whether the operand satisfies the
+ static predicate (if any) of the target type.
+ * sem_ch3.adb (Analyze_Object_Declaration): Do
+ not install a predicate check if the object is initialized by
+ means of a type conversion because the conversion is subjected
+ to the same check.
+
+2017-04-27 Tristan Gingold <gingold@adacore.com>
+
+ * raise.c (__gnat_builtin_longjmp): Remove.
+ (__gnat_bracktrace):
+ Add a dummy definition for the compiler (__gnat_eh_personality,
+ __gnat_rcheck_04, __gnat_rcheck_10) (__gnat_rcheck_19,
+ __gnat_rcheck_20, __gnat_rcheck_21) (__gnat_rcheck_30,
+ __gnat_rcheck_31, __gnat_rcheck_32): Likewise.
+ * a-exexpr.adb: Renamed from a-exexpr-gcc.adb
+ * a-except.ads, a-except.adb: Renamed from a-except-2005.ads
+ and a-except-2005.adb.
+ * raise-gcc.c: Allow build in compiler, compiled as a C++
+ file.
+ (__gnat_Unwind_ForcedUnwind): Adjust prototype.
+ (db): Constify msg_format.
+ (get_call_site_action_for): Don't use void arithmetic.
+ * system.ads (Frontend_Exceptions): Set to False.
+ (ZCX_By_Default): Set to True.
+ (GCC_ZC_Support): Set to True.
+ * gcc-interface/Makefile.in: No more variants for a-exexpr.adb and
+ a-except.ad[sb].
+ * gcc-interface/Make-lang.in: Add support for backend zcx exceptions
+ in gnat1 and gnatbind.
+ * gnat1, gnatbind: link with raise-gcc.o, a-exctra.o, s-addima.o,
+ s-excmac.o, s-imgint.o, s-traceb.o, s-trasym.o, s-wchstw.o
+ * s-excmac.ads, s-excmac.adb: Copy of variants.
+ * a-except.o: Adjust preequisites.
+ Add handling of s-excmac-arm.adb and s-excmac-gcc.adb.
+
+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cfdlli.adb, a-cfdlli.ads (Formal_Model): Adapt to
+ modifications in functional containers.
+ * a-cofuba.ads, a-cofuma.ads, a-cofuse.ads, a-cofuve.ads Reformat
+ to improve readablity. Subprograms are separated between basic
+ operations, constructors and properties. Universally quantified
+ formulas in contracts are factorized in independant functions
+ with a name and a comment. Names of parameters are improved.
+
+2017-04-27 Gary Dismukes <dismukes@adacore.com>
+
+ * exp_spark.adb, sem_elab.adb: Minor reformatting and typo fix.
+
+2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_res.adb (Resolve_Type_Conversion): Do not
+ install a predicate check here since this is already done during
+ the expansion phase. Verify whether the operand satisfies the
+ static predicate (if any) of the target type.
+ * sem_ch3.adb (Analyze_Object_Declaration): Do
+ not install a predicate check if the object is initialized by
+ means of a type conversion because the conversion is subjected
+ to the same check.
+
+2017-04-27 Tristan Gingold <gingold@adacore.com>
+
+ * a-except.ads, a-except.adb, a-exexpr.adb: Removed (will be
+ replaced by their variants).
+
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_prag.adb, a-cofuse.adb, a-cofuse.ads, einfo.adb, sem_prag.adb,
procedure Lift_Abstraction_Level (Container : List) is null;
- -------------------------
- -- M_Elements_Contains --
- -------------------------
-
- function M_Elements_Contains
- (S : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- E : Element_Type)
- return Boolean
- is
- begin
- for I in Fst .. Lst loop
- if Element (S, I) = E then
- return True;
- end if;
- end loop;
- return False;
- end M_Elements_Contains;
-
- --------------------
- -- M_Elements_Cst --
- --------------------
-
- function M_Elements_Cst
- (S : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- E : Element_Type)
- return Boolean
- is
- begin
- for I in Fst .. Lst loop
- if Element (S, I) /= E then
- return False;
- end if;
- end loop;
- return True;
- end M_Elements_Cst;
-
- ----------------------
- -- M_Elements_Equal --
- ----------------------
-
- function M_Elements_Equal
- (S1, S2 : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type)
- return Boolean
- is
- begin
- return M_Elements_Shifted (S1, S2, Fst, Lst, 0);
- end M_Elements_Equal;
-
-------------------------
-- M_Elements_Reversed --
-------------------------
- function M_Elements_Reversed (S1, S2 : M.Sequence) return Boolean is
- L : constant Count_Type := M.Length (S1);
+ function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is
+ L : constant Count_Type := M.Length (Left);
begin
- if L /= M.Length (S2) then
+ if L /= M.Length (Right) then
return False;
end if;
for I in 1 .. L loop
- if Element (S1, I) /= Element (S2, L - I + 1)
+ if Element (Left, I) /= Element (Right, L - I + 1)
then
return False;
end if;
return True;
end M_Elements_Reversed;
- ------------------------
- -- M_Elements_Shifted --
- ------------------------
-
- function M_Elements_Shifted
- (S1, S2 : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- Offset : Count_Type'Base := 1)
- return Boolean
- is
- begin
- for I in Fst .. Lst loop
- if Element (S1, I) /= Element (S2, I + Offset) then
- return False;
- end if;
- end loop;
- return True;
- end M_Elements_Shifted;
-
-------------------------
-- M_Elements_Shuffled --
-------------------------
function M_Elements_Shuffle
- (S1, S2 : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- Offset : Count_Type'Base)
- return Boolean
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Offset : Count_Type'Base) return Boolean
is
begin
for I in Fst .. Lst loop
J : Count_Type := Fst;
begin
while not Found and J <= Lst loop
- if Element (S1, I) = Element (S2, J + Offset) then
+ if Element (Left, I) = Element (Right, J + Offset) then
Found := True;
end if;
J := J + 1;
------------------------
function M_Elements_Swapped
- (S1, S2 : M.Sequence;
- X, Y : Positive_Count_Type)
- return Boolean
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ X, Y : Positive_Count_Type) return Boolean
is
begin
- if M.Length (S1) /= M.Length (S2)
- or else Element (S1, X) /= Element (S2, Y)
- or else Element (S1, Y) /= Element (S2, X)
+ if M.Length (Left) /= M.Length (Right)
+ or else Element (Left, X) /= Element (Right, Y)
+ or else Element (Left, Y) /= Element (Right, X)
then
return False;
end if;
- for I in 1 .. M.Length (S1) loop
+ for I in 1 .. M.Length (Left) loop
if I /= X and then I /= Y
- and then Element (S1, I) /= Element (S2, I)
+ and then Element (Left, I) /= Element (Right, I)
then
return False;
end if;
-----------------------
function Mapping_Preserved
- (S1, S2 : M.Sequence;
- M1, M2 : P.Map) return Boolean is
-
+ (M_Left : M.Sequence;
+ M_Right : M.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
begin
- for C of M1 loop
- if not P.Mem (M2, C)
- or else P.Get (M1, C) > M.Length (S1)
- or else P.Get (M2, C) > M.Length (S2)
- or else M.Get (S1, P.Get (M1, C)) /= M.Get (S2, P.Get (M2, C))
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > M.Length (M_Left)
+ or else P.Get (P_Right, C) > M.Length (M_Right)
+ or else M.Get (M_Left, P.Get (P_Left, C))
+ /= M.Get (M_Right, P.Get (P_Right, C))
then
return False;
end if;
end loop;
- for C of M2 loop
- if not P.Mem (M1, C) then
+ for C of P_Right loop
+ if not P.Has_Key (P_Left, C) then
return False;
end if;
end loop;
is
begin
for Cu of Small loop
- if not P.Mem (Big, Cu) then
+ if not P.Has_Key (Big, Cu) then
return False;
end if;
end loop;
Pos : constant Positive_Count_Type := P.Get (Big, Cu);
begin
if Pos < Cut then
- if not P.Mem (Small, Cu) or else Pos /= P.Get (Small, Cu)
+ if not P.Has_Key (Small, Cu) or else Pos /= P.Get (Small, Cu)
then
return False;
end if;
elsif Pos >= Cut + Count then
- if not P.Mem (Small, Cu)
+ if not P.Has_Key (Small, Cu)
or else Pos /= P.Get (Small, Cu) + Count
then
return False;
end if;
else
- if P.Mem (Small, Cu) then
+ if P.Has_Key (Small, Cu) then
return False;
end if;
end if;
-------------------------
function P_Positions_Swapped
- (M1, M2 : P.Map;
- C1, C2 : Cursor) return Boolean
+ (Left : P.Map;
+ Right : P.Map;
+ X, Y : Cursor) return Boolean
is
begin
- if not P.Mem (M1, C1) or not P.Mem (M1, C2)
- or not P.Mem (M2, C1) or not P.Mem (M2, C2)
+ if not P.Has_Key (Left, X) or not P.Has_Key (Left, Y)
+ or not P.Has_Key (Right, X) or not P.Has_Key (Right, Y)
then
return False;
end if;
- if P.Get (M1, C1) /= P.Get (M2, C2)
- or P.Get (M1, C2) /= P.Get (M2, C1)
+ if P.Get (Left, X) /= P.Get (Right, Y)
+ or P.Get (Left, Y) /= P.Get (Right, X)
then
return False;
end if;
- for C of M1 loop
- if not P.Mem (M2, C) then
+ for C of Left loop
+ if not P.Has_Key (Right, C) then
return False;
end if;
end loop;
- for C of M2 loop
- if not P.Mem (M1, C)
- or else (C /= C1 and C /= C2 and P.Get (M1, C) /= P.Get (M2, C))
+ for C of Right loop
+ if not P.Has_Key (Left, C)
+ or else (C /= X and C /= Y
+ and P.Get (Left, C) /= P.Get (Right, C))
then
return False;
end if;
is
begin
for Cu of Small loop
- if not P.Mem (Big, Cu) then
+ if not P.Has_Key (Big, Cu) then
return False;
end if;
end loop;
Pos : constant Positive_Count_Type := P.Get (Big, Cu);
begin
if Pos < Cut then
- if not P.Mem (Small, Cu) or else Pos /= P.Get (Small, Cu)
+ if not P.Has_Key (Small, Cu) or else Pos /= P.Get (Small, Cu)
then
return False;
end if;
elsif Pos >= Cut + Count then
return False;
- elsif P.Mem (Small, Cu) then
+ elsif P.Has_Key (Small, Cu) then
return False;
end if;
end;
-- M_Elements_Sorted --
-----------------------
- function M_Elements_Sorted (S : M.Sequence) return Boolean is
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
begin
- if M.Length (S) = 0 then
+ if M.Length (Container) = 0 then
return True;
end if;
declare
- E1 : Element_Type := Element (S, 1);
+ E1 : Element_Type := Element (Container, 1);
begin
- for I in 2 .. M.Length (S) loop
+ for I in 2 .. M.Length (Container) loop
declare
- E2 : constant Element_Type := Element (S, I);
+ E2 : constant Element_Type := Element (Container, I);
begin
if E2 < E1 then
return False;
function "<" (Left, Right : M.Sequence) return Boolean renames M."<";
function "<=" (Left, Right : M.Sequence) return Boolean renames M."<=";
- function M_Elements_Contains
- (S : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- E : Element_Type)
- return Boolean
- -- E appears in the slice from Fst to Lst in S
- with
- Global => null,
- Pre => Lst <= M.Length (S),
- Post =>
- M_Elements_Contains'Result =
- (for some I in Fst .. Lst => Element (S, I) = E);
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Contains);
-
- function M_Elements_Cst
- (S : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- E : Element_Type)
- return Boolean
- -- Every element of the slice from Fst to Lst in S is E.
- with
- Global => null,
- Pre => Lst <= M.Length (S),
- Post =>
- M_Elements_Cst'Result =
- (for all I in Fst .. Lst => Element (S, I) = E);
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Cst);
-
- function M_Elements_Equal
- (S1, S2 : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type)
- return Boolean
- -- The slice from Fst to Lst is the same in S1 and S2
- with
- Global => null,
- Pre => Lst <= M.Length (S1) and Lst <= M.Length (S2),
- Post =>
- M_Elements_Equal'Result =
- (for all I in Fst .. Lst => Element (S1, I) = Element (S2, I));
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Equal);
-
function M_Elements_Shuffle
- (S1, S2 : M.Sequence;
+ (Left : M.Sequence;
+ Right : M.Sequence;
Fst : Positive_Count_Type;
Lst : Count_Type;
Offset : Count_Type'Base)
return Boolean
- -- The slice from Fst to Lst in S1 contains the same elements than the
- -- same slide shifted by Offset in S2
+ -- The slice from Fst to Lst in Left contains the same elements than the
+ -- same slide shifted by Offset in Right
with
Global => null,
Pre =>
- Lst <= M.Length (S1)
- and Offset in 1 - Fst .. M.Length (S2) - Lst,
+ Lst <= M.Length (Left)
+ and Offset in 1 - Fst .. M.Length (Right) - Lst,
Post =>
M_Elements_Shuffle'Result =
(for all J in Fst + Offset .. Lst + Offset =>
(for some I in Fst .. Lst =>
- Element (S1, I) = Element (S2, J)));
+ Element (Left, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shuffle);
- function M_Elements_Reversed (S1, S2 : M.Sequence) return Boolean
- -- S2 is S1 in reverse order
+ function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean
+ -- Right is Left in reverse order
with
Global => null,
Post =>
M_Elements_Reversed'Result =
- (M.Length (S1) = M.Length (S2)
- and (for all I in 1 .. M.Length (S1) =>
- Element (S1, I) = Element (S2, M.Length (S1) - I + 1))
- and (for all I in 1 .. M.Length (S1) =>
- Element (S2, I) = Element (S1, M.Length (S1) - I + 1)));
+ (M.Length (Left) = M.Length (Right)
+ and
+ (for all I in 1 .. M.Length (Left) =>
+ Element (Left, I)
+ = Element (Right, M.Length (Left) - I + 1))
+ and
+ (for all I in 1 .. M.Length (Left) =>
+ Element (Right, I)
+ = Element (Left, M.Length (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
- function M_Elements_Shifted
- (S1, S2 : M.Sequence;
- Fst : Positive_Count_Type;
- Lst : Count_Type;
- Offset : Count_Type'Base := 1)
- return Boolean
- -- The slice from Fst to Lst in S1 has been shifted by Offset in S2.
- with
- Global => null,
- Pre =>
- Lst <= M.Length (S1)
- and Offset in 1 - Fst .. M.Length (S2) - Lst,
- Post =>
- M_Elements_Shifted'Result =
- ((for all I in Fst .. Lst =>
- Element (S1, I) = Element (S2, I + Offset))
- and (for all I in Fst + Offset .. Lst + Offset =>
- Element (S1, I - Offset) = Element (S2, I)));
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shifted);
-
function M_Elements_Swapped
- (S1, S2 : M.Sequence;
- X, Y : Positive_Count_Type)
+ (Left : M.Sequence;
+ Right : M.Sequence;
+ X, Y : Positive_Count_Type)
return Boolean
- -- Elements stored at X and Y are reversed in S1 and S2
+ -- Elements stored at X and Y are reversed in Left and Right
with
Global => null,
- Pre => X <= M.Length (S1) and Y <= M.Length (S1),
+ Pre => X <= M.Length (Left) and Y <= M.Length (Left),
Post =>
M_Elements_Swapped'Result =
- (M.Length (S1) = M.Length (S2)
- and Element (S1, X) = Element (S2, Y)
- and Element (S1, Y) = Element (S2, X)
- and
- (for all I in 1 .. M.Length (S1) =>
- (if I /= X and I /= Y
- then Element (S1, I) = Element (S2, I))));
+ (M.Length (Left) = M.Length (Right)
+ and Element (Left, X) = Element (Right, Y)
+ and Element (Left, Y) = Element (Right, X)
+ and M.Equal_Except (Left, Right, X, Y));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
package P is new Ada.Containers.Functional_Maps
P_Positions_Shifted'Result =
-- Big contains all cursors of Small
- ((for all I of Small => P.Mem (Big, I))
+ (P.Keys_Included (Small, Big)
-- Cursors located before Cut are not moved, cursors located after
-- are shifted by Count.
-- New cursors of Big (if any) are between Cut and Cut - 1 + Count
and
(for all I of Big =>
- P.Mem (Small, I)
+ P.Has_Key (Small, I)
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
function P_Positions_Swapped
- (M1, M2 : P.Map;
- C1, C2 : Cursor) return Boolean
- -- M1 and M2 contain the same cursors, but the positions of C1 and C2
+ (Left : P.Map;
+ Right : P.Map;
+ X, Y : Cursor) return Boolean
+ -- Left and Right contain the same cursors, but the positions of X and Y
-- are reversed.
with
Ghost,
Global => null,
Post =>
P_Positions_Swapped'Result =
- ((for all C of M1 => P.Mem (M2, C))
- and (for all C of M2 => P.Mem (M1, C))
- and
- (for all C of M1 =>
- (if C /= C1 and C /= C2
- then P.Get (M1, C) = P.Get (M2, C)))
- and P.Mem (M1, C1) and P.Mem (M1, C2)
- and P.Get (M1, C1) = P.Get (M2, C2)
- and P.Get (M1, C2) = P.Get (M2, C1));
+ (P.Same_Keys (Left, Right)
+ and P.Elements_Equal_Except (Left, Right, X, Y)
+ and P.Has_Key (Left, X) and P.Has_Key (Left, Y)
+ and P.Get (Left, X) = P.Get (Right, Y)
+ and P.Get (Left, Y) = P.Get (Right, X));
function P_Positions_Truncated
(Small : P.Map;
Post =>
P_Positions_Truncated'Result =
- -- Big contains all cursors of Small
- ((for all I of Small => P.Mem (Big, I))
-
- -- The cursors of Small are all bellow Cut
- and (for all I of Small => P.Get (Small, I) < Cut)
-
- -- The cursors have the same position in Big and Small
- and (for all I of Small => P.Get (Big, I) = P.Get (Small, I))
+ -- Big contains all cursors of Small at the same position
+ (Small <= Big
-- New cursors of Big (if any) are between Cut and Cut - 1 + Count
and
(for all I of Big =>
- P.Mem (Small, I)
+ P.Has_Key (Small, I)
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
function Mapping_Preserved
- (S1, S2 : M.Sequence;
- M1, M2 : P.Map) return Boolean
+ (M_Left : M.Sequence;
+ M_Right : M.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
with
Ghost,
Global => null,
Post =>
(if Mapping_Preserved'Result then
- -- M1 contains all cursors of M2
- (for all I of M2 => P.Mem (M1, I))
-
- -- M2 contains all cursors of M1
- and (for all I of M1 => P.Mem (M2, I))
+ -- Left and Right contain the same cursors
+ P.Same_Keys (P_Left, P_Right)
- -- Mappings from cursors to elements induced by S1, M1 and S2, M2
- -- are the same.
- and (for all I of M1 =>
- M.Get (S1, P.Get (M1, I)) = M.Get (S2, P.Get (M2, I))));
+ -- Mappings from cursors to elements induced by M_Left, P_Left
+ -- and M_Right, P_Right are the same.
+ and (for all C of P_Left =>
+ M.Get (M_Left, P.Get (P_Left, C))
+ = M.Get (M_Right, P.Get (P_Right, C))));
function Model (Container : List) return M.Sequence with
-- The highlevel model of a list is a sequence of elements. Cursors are
Ghost,
Global => null,
- Post => not P.Mem (Positions'Result, No_Element)
+ Post => not P.Has_Key (Positions'Result, No_Element)
-- Positions of cursors are smaller than the container's length.
and then
(for all I of Positions'Result =>
-- Cursors are preserved.
and Positions (Container)'Old = Positions (Container)
- -- The element at the position of Position in Container is replaced by
- -- New_Item.
- and M.Is_Set (Model (Container)'Old,
- P.Get (Positions (Container), Position),
- New_Item,
- Model (Container));
+ -- The element at the position of Position in Container is New_Item
+ and Element (Model (Container), P.Get (Positions (Container), Position))
+ = New_Item
+
+ -- Other elements are preserved
+ and M.Equal_Except (Model (Container)'Old,
+ Model (Container),
+ P.Get (Positions (Container), Position));
procedure Move (Target : in out List; Source : in out List) with
Global => null,
-- Positions contains a new mapping from the last cursor of
-- Container to its length.
- P.Is_Add
- (Positions (Container)'Old, Last (Container), Length (Container),
- Result => Positions (Container))
+ P.Get (Positions (Container), Last (Container)) = Length (Container)
+
+ -- Other cursors come from Container'Old
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
+
+ -- Cursors of Container'Old keep the same position
+ and Positions (Container)'Old <= Positions (Container)
-- Model contains a new element New_Item at the end
- and M.Is_Add (Model (Container)'Old, New_Item, Model (Container)),
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+ and Model (Container)'Old <= Model (Container),
others =>
-- The elements of Container located before Before are preserved.
- M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Before) - 1)
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
-- Other elements are shifted by 1.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Before),
Lst => Length (Container)'Old,
Offset => 1)
(Before = No_Element =>
-- The elements of Container are preserved
- M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => Length (Container)'Old)
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Length (Container)'Old)
-- Container contains Count times New_Item at the end
- and M_Elements_Cst
- (S => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- E => New_Item)
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item)
-- A Count cursors have been inserted at the end of Container
and P_Positions_Truncated
others =>
-- The elements of Container located before Before are preserved
- M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Before) - 1)
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Before) - 1)
-- Other elements are shifted by Count.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Before),
Lst => Length (Container)'Old,
Offset => Count)
-- Container contains Count times New_Item after position Before
- and M_Elements_Cst
- (S => Model (Container),
- Fst => P.Get (Positions (Container)'Old, Before),
- Lst => P.Get (Positions (Container)'Old, Before) - 1 + Count,
- E => New_Item)
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container)'Old, Before),
+ Lst =>
+ P.Get (Positions (Container)'Old, Before) - 1 + Count,
+ Item => New_Item)
-- Count cursors have been inserted at position Before in Container
and P_Positions_Shifted
-- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is
-- No_Element.
- and P.Mem (Positions (Container), Position)
+ and P.Has_Key (Positions (Container), Position)
and (if Before = No_Element
then P.Get (Positions (Container), Position)
= Length (Container)
= P.Get (Positions (Container)'Old, Before))
-- The elements of Container located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container), Position) - 1)
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
-- Other elements are shifted by 1.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst => Length (Container)'Old,
Offset => 1)
-- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is
-- No_Element.
- P.Mem (Positions (Container), Position)
+ P.Has_Key (Positions (Container), Position)
and (if Before = No_Element
then P.Get (Positions (Container), Position)
= Length (Container)'Old + 1
= P.Get (Positions (Container)'Old, Before))
-- The elements of Container located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container), Position) - 1)
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
-- Other elements are shifted by Count.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst => Length (Container)'Old,
Offset => Count)
-- Container contains Count times New_Item after position Position
- and M_Elements_Cst
- (S => Model (Container),
- Fst => P.Get (Positions (Container), Position),
- Lst => P.Get (Positions (Container), Position) - 1 + Count,
- E => New_Item)
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => P.Get (Positions (Container), Position) - 1 + Count,
+ Item => New_Item)
-- Count cursor have been inserted at Position in Container
and P_Positions_Shifted
Length (Container) = Length (Container)'Old + 1
-- Elements are shifted by 1
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old,
Offset => 1)
Length (Container) = Length (Container)'Old + Count
-- Elements are shifted by Count.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old,
Offset => Count)
-- Container starts with Count times New_Item
- and M_Elements_Cst
- (S => Model (Container),
- Fst => 1,
- Lst => Count,
- E => New_Item)
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => 1,
+ Lst => Count,
+ Item => New_Item)
-- Count cursors have been inserted at the beginning of Container
and P_Positions_Shifted
-- Positions contains a new mapping from the last cursor of
-- Container to its length.
- and P.Is_Add
- (Positions (Container)'Old, Last (Container), Length (Container),
- Result => Positions (Container))
+ and P.Get (Positions (Container), Last (Container))
+ = Length (Container)
+
+ -- Other cursors come from Container'Old
+ and P.Keys_Included_Except
+ (Left => Positions (Container),
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container))
+
+ -- Cursors of Container'Old keep the same position
+ and Positions (Container)'Old <= Positions (Container)
-- Model contains a new element New_Item at the end
- and M.Is_Add (Model (Container)'Old, New_Item, Model (Container));
+ and Element (Model (Container), Length (Container)) = New_Item
+
+ -- Elements of Container'Old are preserved
+ and Model (Container)'Old <= Model (Container);
procedure Append
(Container : in out List;
and Model (Container)'Old <= Model (Container)
-- Container contains Count times New_Item at the end
- and M_Elements_Cst
- (S => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- E => New_Item)
+ and M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item)
-- Count cursors have been inserted at the end of Container
and P_Positions_Truncated
and Position = No_Element
-- The elements of Container located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
-- The elements located after Position are shifted by 1
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
Lst => Length (Container)'Old,
Offset => -1)
and Position = No_Element
-- The elements of Container located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
Contract_Cases =>
-- All the elements after Position have been erased
Length (Container) = Length (Container)'Old - Count
-- Other elements are shifted by Count
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst =>
P.Get (Positions (Container)'Old, Position'Old) + Count,
Lst => Length (Container)'Old,
Length (Container) = Length (Container)'Old - 1
-- The elements of Container are shifted by 1
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => 2,
Lst => Length (Container)'Old,
Offset => -1)
Length (Container) = Length (Container)'Old - Count
-- Elements of Container are shifted by Count
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => Count + 1,
Lst => Length (Container)'Old,
Offset => -Count)
and Model (Container) <= Model (Container)'Old
-- The last cursor of Container has been removed
- and P.Is_Add (Positions (Container), Last (Container)'Old,
- Length (Container)'Old, Positions (Container)'Old);
+ and not P.Has_Key (Positions (Container), Last (Container)'Old)
+
+ -- Other cursors are still valid
+ and P.Keys_Included_Except
+ (Left => Positions (Container)'Old,
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container)'Old)
+
+ -- The positions of other cursors are preserved
+ and Positions (Container) <= Positions (Container)'Old;
procedure Delete_Last
(Container : in out List;
(Before = No_Element =>
-- The elements of Target are preserved
- M_Elements_Equal
- (S1 => Model (Target)'Old,
- S2 => Model (Target),
- Fst => 1,
- Lst => Length (Target)'Old)
+ M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => Length (Target)'Old)
-- The elements of Source are appended to target, the order is not
-- specified.
and M_Elements_Shuffle
- (S1 => Model (Source)'Old,
- S2 => Model (Target),
+ (Left => Model (Source)'Old,
+ Right => Model (Target),
Fst => 1,
Lst => Length (Source)'Old,
Offset => Length (Target)'Old)
others =>
-- The elements of Target located before Before are preserved
- M_Elements_Equal
- (S1 => Model (Target)'Old,
- S2 => Model (Target),
- Fst => 1,
- Lst => P.Get (Positions (Target)'Old, Before) - 1)
+ M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target)'Old, Before) - 1)
-- The elements of Source are inserted before Before, the order is
-- not specified.
and M_Elements_Shuffle
- (S1 => Model (Source)'Old,
- S2 => Model (Target),
+ (Left => Model (Source)'Old,
+ Right => Model (Target),
Fst => 1,
Lst => Length (Source)'Old,
Offset => P.Get (Positions (Target)'Old, Before) - 1)
-- Other elements are shifted by the length of Source
- and M_Elements_Shifted
- (S1 => Model (Target)'Old,
- S2 => Model (Target),
+ and M.Range_Shifted
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
Fst => P.Get (Positions (Target)'Old, Before),
Lst => Length (Target)'Old,
Offset => Length (Source)'Old)
and Length (Source) = Length (Source)'Old - 1
-- The elements of Source located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Source)'Old,
- S2 => Model (Source),
- Fst => 1,
- Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
+ and M.Range_Equal
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
+ Fst => 1,
+ Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
-- The elements located after Position are shifted by 1
- and M_Elements_Shifted
- (S1 => Model (Source)'Old,
- S2 => Model (Source),
+ and M.Range_Shifted
+ (Left => Model (Source)'Old,
+ Right => Model (Source),
Fst => P.Get (Positions (Source)'Old, Position'Old) + 1,
Lst => Length (Source)'Old,
Offset => -1)
-- Positions is valid in Target and it is located either before
-- Before if it is valid in Target or at the end if it is
-- No_Element.
- and P.Mem (Positions (Target), Position)
+ and P.Has_Key (Positions (Target), Position)
and (if Before = No_Element
then P.Get (Positions (Target), Position)
= Length (Target)
= P.Get (Positions (Target)'Old, Before))
-- The elements of Target located before Position are preserved.
- and M_Elements_Equal
- (S1 => Model (Target)'Old,
- S2 => Model (Target),
- Fst => 1,
- Lst => P.Get (Positions (Target), Position) - 1)
+ and M.Range_Equal
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
+ Fst => 1,
+ Lst => P.Get (Positions (Target), Position) - 1)
-- Other elements are shifted by 1.
- and M_Elements_Shifted
- (S1 => Model (Target)'Old,
- S2 => Model (Target),
+ and M.Range_Shifted
+ (Left => Model (Target)'Old,
+ Right => Model (Target),
Fst => P.Get (Positions (Target), Position),
Lst => Length (Target)'Old,
Offset => 1)
Before = No_Element =>
-- The elements located before Position are preserved
- M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => P.Get (Positions (Container)'Old, Position) - 1)
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position) - 1)
-- The elements located after Position are shifted by 1
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position) + 1,
Lst => Length (Container)'Old,
Offset => -1)
-- Cursors from Container continue designating the same elements
and Mapping_Preserved
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- M1 => Positions (Container)'Old,
- M2 => Positions (Container)),
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)),
others =>
-- The elements located before Position and Before are preserved
- M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => 1,
- Lst => Count_Type'Min
- (P.Get (Positions (Container)'Old, Position) - 1,
- P.Get (Positions (Container)'Old, Before) - 1))
+ M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => 1,
+ Lst => Count_Type'Min
+ (P.Get (Positions (Container)'Old, Position) - 1,
+ P.Get (Positions (Container)'Old, Before) - 1))
-- The elements located after Position and Before are preserved
- and M_Elements_Equal
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- Fst => Count_Type'Max
- (P.Get (Positions (Container)'Old, Position) + 1,
- P.Get (Positions (Container)'Old, Before) + 1),
- Lst => Length (Container))
+ and M.Range_Equal
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
+ Fst => Count_Type'Max
+ (P.Get (Positions (Container)'Old, Position) + 1,
+ P.Get (Positions (Container)'Old, Before) + 1),
+ Lst => Length (Container))
-- The elements located after Before and before Position are shifted
-- by 1 to the right.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Before) + 1,
Lst => P.Get (Positions (Container)'Old, Position) - 1,
Offset => 1)
-- The elements located after Position and before Before are shifted
-- by 1 to the left.
- and M_Elements_Shifted
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
+ and M.Range_Shifted
+ (Left => Model (Container)'Old,
+ Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position) + 1,
Lst => P.Get (Positions (Container)'Old, Before) - 1,
Offset => -1)
-- Cursors from Container continue designating the same elements
and Mapping_Preserved
- (S1 => Model (Container)'Old,
- S2 => Model (Container),
- M1 => Positions (Container)'Old,
- M2 => Positions (Container)));
+ (M_Left => Model (Container)'Old,
+ M_Right => Model (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container)));
function First (Container : List) return Cursor with
Global => null,
-- If Item is not is not contained in Container after Position, Find
-- returns No_Element.
- (not M_Elements_Contains
- (S => Model (Container),
- Fst => (if Position = No_Element then 1
- else P.Get (Positions (Container), Position)),
- Lst => Length (Container),
- E => Item)
+ (not M.Contains
+ (Container => Model (Container),
+ Fst => (if Position = No_Element then 1
+ else P.Get (Positions (Container), Position)),
+ Lst => Length (Container),
+ Item => Item)
=>
Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container
others =>
- P.Mem (Positions (Container), Find'Result)
+ P.Has_Key (Positions (Container), Find'Result)
-- The element designated by the result of Find is Item
and Element (Model (Container),
>= P.Get (Positions (Container), Position))
-- It is the first occurence of Item in this slice
- and not M_Elements_Contains
- (S => Model (Container),
- Fst => (if Position = No_Element then 1
- else P.Get (Positions (Container), Position)),
- Lst => P.Get (Positions (Container), Find'Result) - 1,
- E => Item));
+ and not M.Contains
+ (Container => Model (Container),
+ Fst => (if Position = No_Element then 1
+ else P.Get (Positions (Container), Position)),
+ Lst => P.Get (Positions (Container), Find'Result) - 1,
+ Item => Item));
function Reverse_Find
(Container : List;
-- If Item is not is not contained in Container before Position, Find
-- returns No_Element.
- (not M_Elements_Contains
- (S => Model (Container),
- Fst => 1,
- Lst => (if Position = No_Element then Length (Container)
- else P.Get (Positions (Container), Position)),
- E => Item)
+ (not M.Contains
+ (Container => Model (Container),
+ Fst => 1,
+ Lst => (if Position = No_Element then Length (Container)
+ else P.Get (Positions (Container), Position)),
+ Item => Item)
=>
Reverse_Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container
others =>
- P.Mem (Positions (Container), Reverse_Find'Result)
+ P.Has_Key (Positions (Container), Reverse_Find'Result)
-- The element designated by the result of Find is Item
and Element (Model (Container),
<= P.Get (Positions (Container), Position))
-- It is the last occurence of Item in this slice
- and not M_Elements_Contains
- (S => Model (Container),
- Fst => P.Get (Positions (Container), Reverse_Find'Result) + 1,
- Lst => (if Position = No_Element then Length (Container)
- else P.Get (Positions (Container), Position)),
- E => Item));
+ and not M.Contains
+ (Container => Model (Container),
+ Fst => P.Get (Positions (Container), Reverse_Find'Result) + 1,
+ Lst => (if Position = No_Element then Length (Container)
+ else P.Get (Positions (Container), Position)),
+ Item => Item));
function Contains
(Container : List;
Item : Element_Type) return Boolean
with
Global => null,
- Post => Contains'Result =
- M_Elements_Contains
- (S => Model (Container),
- Fst => 1,
- Lst => Length (Container),
- E => Item);
+ Post =>
+ Contains'Result = M.Contains (Container => Model (Container),
+ Fst => 1,
+ Lst => Length (Container),
+ Item => Item);
function Has_Element (Container : List; Position : Cursor) return Boolean
with
Global => null,
- Post => Has_Element'Result = P.Mem (Positions (Container), Position);
+ Post =>
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode is
- function M_Elements_Sorted (S : M.Sequence) return Boolean with
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean with
Ghost,
Global => null,
Post => M_Elements_Sorted'Result =
- (for all I in 1 .. M.Length (S) =>
- (for all J in I + 1 .. M.Length (S) =>
- Element (S, I) = Element (S, J)
- or Element (S, I) < Element (S, J)));
+ (for all I in 1 .. M.Length (Container) =>
+ (for all J in I + 1 .. M.Length (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : List) return Boolean with
-- "=" --
---------
- function "=" (M1 : Map; M2 : Map) return Boolean is
- (M1.Keys <= M2.Keys and M2 <= M1);
+ function "=" (Left : Map; Right : Map) return Boolean is
+ (Left.Keys <= Right.Keys and Right <= Left);
----------
-- "<=" --
----------
- function "<=" (M1 : Map; M2 : Map) return Boolean is
+ function "<=" (Left : Map; Right : Map) return Boolean is
I2 : Count_Type;
begin
- for I1 in 1 .. Length (M1.Keys) loop
- I2 := Find (M2.Keys, Get (M1.Keys, I1));
+ for I1 in 1 .. Length (Left.Keys) loop
+ I2 := Find (Right.Keys, Get (Left.Keys, I1));
if I2 = 0
- or else Get (M2.Elements, I2) /= Get (M1.Elements, I1)
+ or else Get (Right.Elements, I2) /= Get (Left.Elements, I1)
then
return False;
end if;
-- Add --
---------
- function Add (M : Map; K : Key_Type; E : Element_Type) return Map is
+ function Add
+ (Container : Map;
+ New_Key : Key_Type;
+ New_Item : Element_Type) return Map
+ is
begin
return
- (Keys => Add (M.Keys, Length (M.Keys) + 1, K),
- Elements => Add (M.Elements, Length (M.Elements) + 1, E));
+ (Keys =>
+ Add (Container.Keys, Length (Container.Keys) + 1, New_Key),
+ Elements =>
+ Add
+ (Container.Elements, Length (Container.Elements) + 1, New_Item));
end Add;
+ ---------------------------
+ -- Elements_Equal_Except --
+ ---------------------------
+
+ function Elements_Equal_Except
+ (Left : Map;
+ Right : Map;
+ New_Key : Key_Type) return Boolean
+ is
+ begin
+ for I in 1 .. Length (Left.Keys) loop
+ declare
+ K : constant Key_Type := Get (Left.Keys, I);
+ begin
+ if not Equivalent_Keys (K, New_Key)
+ and then Get (Right.Elements, Find (Right.Keys, K))
+ /= Get (Left.Elements, I)
+ then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end Elements_Equal_Except;
+
+ function Elements_Equal_Except
+ (Left : Map;
+ Right : Map;
+ X, Y : Key_Type) return Boolean
+ is
+ begin
+ for I in 1 .. Length (Left.Keys) loop
+ declare
+ K : constant Key_Type := Get (Left.Keys, I);
+ begin
+ if not Equivalent_Keys (K, X)
+ and then not Equivalent_Keys (K, Y)
+ and then Get (Right.Elements, Find (Right.Keys, K))
+ /= Get (Left.Elements, I)
+ then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end Elements_Equal_Except;
+
---------
-- Get --
---------
- function Get (M : Map; K : Key_Type) return Element_Type is
+ function Get (Container : Map; Key : Key_Type) return Element_Type is
begin
- return Get (M.Elements, Find (M.Keys, K));
+ return Get (Container.Elements, Find (Container.Keys, Key));
end Get;
- ------------
- -- Is_Add --
- ------------
+ -------------
+ -- Has_Key --
+ -------------
- function Is_Add
- (M : Map;
- K : Key_Type;
- E : Element_Type;
- Result : Map) return Boolean
- is
+ function Has_Key (Container : Map; Key : Key_Type) return Boolean is
begin
- if Mem (M, K) or not Mem (Result, K) or Get (Result, K) /= E then
- return False;
- end if;
-
- for K of M loop
- if not Mem (Result, K) or else Get (Result, K) /= Get (M, K) then
- return False;
- end if;
- end loop;
-
- for KK of Result loop
- if KK /= K and not Mem (M, KK) then
- return False;
- end if;
- end loop;
-
- return True;
- end Is_Add;
+ return Find (Container.Keys, Key) > 0;
+ end Has_Key;
--------------
-- Is_Empty --
--------------
- function Is_Empty (M : Map) return Boolean is
+ function Is_Empty (Container : Map) return Boolean is
begin
- return Length (M.Keys) = 0;
+ return Length (Container.Keys) = 0;
end Is_Empty;
- ------------
- -- Is_Set --
- ------------
+ -------------------
+ -- Keys_Included --
+ -------------------
+
+ function Keys_Included (Left : Map; Right : Map) return Boolean is
+ begin
+ for I in 1 .. Length (Left.Keys) loop
+ declare
+ K : constant Key_Type := Get (Left.Keys, I);
+ begin
+ if Find (Right.Keys, K) = 0 then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end Keys_Included;
+
+ --------------------------
+ -- Keys_Included_Except --
+ --------------------------
+
+ function Keys_Included_Except
+ (Left : Map;
+ Right : Map;
+ New_Key : Key_Type) return Boolean
+ is
+ begin
+ for I in 1 .. Length (Left.Keys) loop
+ declare
+ K : constant Key_Type := Get (Left.Keys, I);
+ begin
+ if not Equivalent_Keys (K, New_Key)
+ and then Find (Right.Keys, K) = 0
+ then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end Keys_Included_Except;
- function Is_Set
- (M : Map;
- K : Key_Type;
- E : Element_Type;
- Result : Map) return Boolean
+ function Keys_Included_Except
+ (Left : Map;
+ Right : Map;
+ X, Y : Key_Type) return Boolean
is
- (Mem (M, K)
- and then Mem (Result, K)
- and then Get (Result, K) = E
- and then (for all KK of M =>
- Mem (Result, KK)
- and then
- (if K /= KK then Get (Result, KK) = Get (M, KK)))
- and then (for all K of Result => Mem (M, K)));
+ begin
+ for I in 1 .. Length (Left.Keys) loop
+ declare
+ K : constant Key_Type := Get (Left.Keys, I);
+ begin
+ if not Equivalent_Keys (K, X)
+ and then not Equivalent_Keys (K, Y)
+ and then Find (Right.Keys, K) = 0
+ then
+ return False;
+ end if;
+ end;
+ end loop;
+ return True;
+ end Keys_Included_Except;
------------
-- Length --
------------
- function Length (M : Map) return Count_Type is
+ function Length (Container : Map) return Count_Type is
begin
- return Length (M.Elements);
+ return Length (Container.Elements);
end Length;
- ---------
- -- Mem --
- ---------
+ ---------------
+ -- Same_Keys --
+ ---------------
- function Mem (M : Map; K : Key_Type) return Boolean is
- begin
- return Find (M.Keys, K) > 0;
- end Mem;
+ function Same_Keys (Left : Map; Right : Map) return Boolean is
+ (Keys_Included (Left, Right)
+ and Keys_Included (Left => Right, Right => Left));
---------
-- Set --
---------
- function Set (M : Map; K : Key_Type; E : Element_Type) return Map is
- (Keys => M.Keys, Elements => Set (M.Elements, Find (M.Keys, K), E));
+ function Set
+ (Container : Map;
+ Key : Key_Type;
+ New_Item : Element_Type) return Map
+ is
+ (Keys => Container.Keys,
+ Elements =>
+ Set (Container.Elements, Find (Container.Keys, Key), New_Item));
end Ada.Containers.Functional_Maps;
type Key_Type (<>) is private;
type Element_Type (<>) is private;
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
-
package Ada.Containers.Functional_Maps with SPARK_Mode is
- pragma Assertion_Policy (Post => Ignore);
-
type Map is private with
Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
Iterable => (First => Iter_First,
-- "For in" quantification over maps should not be used.
-- "For of" quantification over maps iterates over keys.
- -- Maps are axiomatized using Mem and Get, encoding respectively the
+ -----------------------
+ -- Basic operations --
+ -----------------------
+
+ -- Maps are axiomatized using Has_Key and Get, encoding respectively the
-- presence of a key in a map and an accessor to elements associated to its
-- keys. The length of a map is also added to protect Add against overflows
-- but it is not actually modeled.
- function Mem (M : Map; K : Key_Type) return Boolean with
+ function Has_Key (Container : Map; Key : Key_Type) return Boolean with
Global => null;
+ -- Return True if Key is present in Container
- function Get (M : Map; K : Key_Type) return Element_Type with
+ function Get (Container : Map; Key : Key_Type) return Element_Type with
Global => null,
- Pre => Mem (M, K);
+ Pre => Has_Key (Container, Key);
+ -- Return the element associated to Key is present in Container
- function Length (M : Map) return Count_Type with
+ function Length (Container : Map) return Count_Type with
Global => null;
+ -- Return the number of mappings in Container
- function "<=" (M1 : Map; M2 : Map) return Boolean with
+ ------------------------
+ -- Property Functions --
+ ------------------------
+
+ function "<=" (Left : Map; Right : Map) return Boolean with
-- Map inclusion
Global => null,
- Post => "<="'Result =
- (for all K of M1 =>
- Mem (M2, K) and then Get (M2, K) = Get (M1, K));
+ Post =>
+ "<="'Result =
+ (for all Key of Left =>
+ Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
- function "=" (M1 : Map; M2 : Map) return Boolean with
+ function "=" (Left : Map; Right : Map) return Boolean with
-- Extensional equality over maps
Global => null,
- Post => "="'Result =
- ((for all K of M1 => Mem (M2, K) and then Get (M2, K) = Get (M1, K))
- and (for all K of M2 => Mem (M1, K)));
-
- pragma Warnings (Off, "unused variable ""K""");
- function Is_Empty (M : Map) return Boolean with
+ Post =>
+ "="'Result =
+ ((for all Key of Left =>
+ Has_Key (Right, Key)
+ and then Get (Right, Key) = Get (Left, Key))
+ and (for all Key of Right => Has_Key (Left, Key)));
+
+ pragma Warnings (Off, "unused variable ""Key""");
+ function Is_Empty (Container : Map) return Boolean with
-- A map is empty if it contains no key
+
+ Global => null,
+ Post => Is_Empty'Result = (for all Key of Container => False);
+ pragma Warnings (On, "unused variable ""Key""");
+
+ function Keys_Included (Left : Map; Right : Map) return Boolean
+ -- Returns True if every Key of Left is in Right
+
+ with
+ Global => null,
+ Post =>
+ Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
+
+ function Same_Keys (Left : Map; Right : Map) return Boolean
+ -- Returns True if Left and Right have the same keys
+
+ with
+ Global => null,
+ Post =>
+ Same_Keys'Result =
+ (Keys_Included (Left, Right)
+ and Keys_Included (Left => Right, Right => Left));
+ pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
+
+ function Keys_Included_Except
+ (Left : Map;
+ Right : Map;
+ New_Key : Key_Type) return Boolean
+ -- Returns True if Left contains only keys of Right and possibly New_Key
+
+ with
Global => null,
- Post => Is_Empty'Result = (for all K of M => False);
- pragma Warnings (On, "unused variable ""K""");
+ Post =>
+ Keys_Included_Except'Result =
+ (for all Key of Left =>
+ (if not Equivalent_Keys (Key, New_Key)
+ then Has_Key (Right, Key)));
- function Is_Add
- (M : Map;
- K : Key_Type;
- E : Element_Type;
- Result : Map) return Boolean
- -- Returns True if Result is M augmented with the mapping K -> E
+ function Keys_Included_Except
+ (Left : Map;
+ Right : Map;
+ X, Y : Key_Type) return Boolean
+ -- Returns True if Left contains only keys of Right and possibly X and Y
+
+ with
+ Global => null,
+ Post =>
+ Keys_Included_Except'Result =
+ (for all Key of Left =>
+ (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y)
+ then Has_Key (Right, Key)));
+
+ function Elements_Equal_Except
+ (Left : Map;
+ Right : Map;
+ New_Key : Key_Type) return Boolean
+ -- Returns True if all the keys of Left are mapped to the same elements in
+ -- Left and Right except New_Key.
with
Global => null,
+ Pre => Keys_Included_Except (Left, Right, New_Key),
Post =>
- Is_Add'Result =
- (not Mem (M, K)
- and then Mem (Result, K)
- and then Get (Result, K) = E
- and then (for all K of M =>
- Mem (Result, K) and then Get (Result, K) = Get (M, K))
- and then (for all KK of Result =>
- Equivalent_Keys (KK, K) or Mem (M, KK)));
-
- function Add (M : Map; K : Key_Type; E : Element_Type) return Map with
- -- Returns M augmented with the mapping K -> E.
- -- Is_Add (M, K, E, Result) should be used instead of
- -- Result = Add (M, K, E) whenever possible both for execution and for
- -- proof.
+ Elements_Equal_Except'Result =
+ (for all Key of Left =>
+ (if not Equivalent_Keys (Key, New_Key)
+ then Get (Left, Key) = Get (Right, Key)));
+
+ function Elements_Equal_Except
+ (Left : Map;
+ Right : Map;
+ X, Y : Key_Type) return Boolean
+ -- Returns True if all the keys of Left are mapped to the same elements in
+ -- Left and Right except X and Y.
+ with
Global => null,
- Pre => not Mem (M, K) and Length (M) < Count_Type'Last,
- Post => Length (M) + 1 = Length (Add'Result)
- and Is_Add (M, K, E, Add'Result);
+ Pre => Keys_Included_Except (Left, Right, X, Y),
+ Post =>
+ Elements_Equal_Except'Result =
+ (for all Key of Left =>
+ (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y)
+ then Get (Left, Key) = Get (Right, Key)));
+
+ ----------------------------
+ -- Construction Functions --
+ ----------------------------
- function Is_Set
- (M : Map; K : Key_Type; E : Element_Type; Result : Map) return Boolean
- -- Returns True if Result is M, where the element associated to K has been
- -- replaced by E.
+ -- For better efficiency of both proofs and execution, avoid using
+ -- construction functions in annotations and rather use property functions.
+
+ function Add
+ (Container : Map;
+ New_Key : Key_Type;
+ New_Item : Element_Type) return Map
+ -- Returns Container augmented with the mapping Key -> New_Item.
with
Global => null,
- Post => Is_Set'Result =
- (Mem (M, K)
- and then Mem (Result, K)
- and then Get (Result, K) = E
- and then (for all KK of M => Mem (Result, KK)
- and then (if not Equivalent_Keys (K, KK)
- then Get (Result, KK) = Get (M, KK)))
- and then (for all K of Result => Mem (M, K)));
-
- function Set (M : Map; K : Key_Type; E : Element_Type) return Map with
- -- Returns M, where the element associated to K has been replaced by E.
- -- Is_Set (M, K, E, Result) should be used instead of
- -- Result = Set (M, K, E) whenever possible both for execution and for
- -- proof.
+ Pre =>
+ not Has_Key (Container, New_Key)
+ and Length (Container) < Count_Type'Last,
+ Post =>
+ Length (Container) + 1 = Length (Add'Result)
+ and Has_Key (Add'Result, New_Key)
+ and Get (Add'Result, New_Key) = New_Item
+ and Container <= Add'Result
+ and Keys_Included_Except (Add'Result, Container, New_Key);
+
+ function Set
+ (Container : Map;
+ Key : Key_Type;
+ New_Item : Element_Type) return Map
+ -- Returns Container, where the element associated to Key has been replaced
+ -- by New_Item.
+ with
Global => null,
- Pre => Mem (M, K),
+ Pre => Has_Key (Container, Key),
Post =>
- Length (M) = Length (Set'Result) and Is_Set (M, K, E, Set'Result);
+ Length (Container) = Length (Set'Result)
+ and Get (Set'Result, Key) = New_Item
+ and Same_Keys (Container, Set'Result)
+ and Elements_Equal_Except (Container, Set'Result, Key);
---------------------------
-- Iteration Primitives --
type Private_Key is private;
- function Iter_First (M : Map) return Private_Key with
+ function Iter_First (Container : Map) return Private_Key with
Global => null;
- function Iter_Has_Element (M : Map; K : Private_Key) return Boolean with
+ function Iter_Has_Element
+ (Container : Map;
+ Key : Private_Key) return Boolean
+ with
Global => null;
- function Iter_Next (M : Map; K : Private_Key) return Private_Key with
+ function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
+ with
Global => null,
- Pre => Iter_Has_Element (M, K);
+ Pre => Iter_Has_Element (Container, Key);
- function Iter_Element (M : Map; K : Private_Key) return Key_Type with
+ function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
+ with
Global => null,
- Pre => Iter_Has_Element (M, K);
- pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+ Pre => Iter_Has_Element (Container, Key);
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
private
type Private_Key is new Count_Type;
- function Iter_First (M : Map) return Private_Key is (1);
+ function Iter_First (Container : Map) return Private_Key is (1);
- function Iter_Has_Element (M : Map; K : Private_Key) return Boolean is
- (Count_Type (K) in 1 .. Key_Containers.Length (M.Keys));
+ function Iter_Has_Element
+ (Container : Map;
+ Key : Private_Key) return Boolean
+ is
+ (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
- function Iter_Next (M : Map; K : Private_Key) return Private_Key is
- (if K = Private_Key'Last then 0 else K + 1);
+ function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
+ is
+ (if Key = Private_Key'Last then 0 else Key + 1);
- function Iter_Element (M : Map; K : Private_Key) return Key_Type is
- (Key_Containers.Get (M.Keys, Count_Type (K)));
+ function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
+ is
+ (Key_Containers.Get (Container.Keys, Count_Type (Key)));
end Ada.Containers.Functional_Maps;
-- "=" --
---------
- function "=" (S1 : Set; S2 : Set) return Boolean is
- (S1.Content <= S2.Content and S2.Content <= S1.Content);
+ function "=" (Left : Set; Right : Set) return Boolean is
+ (Left.Content <= Right.Content and Right.Content <= Left.Content);
----------
-- "<=" --
----------
- function "<=" (S1 : Set; S2 : Set) return Boolean is
- (S1.Content <= S2.Content);
+ function "<=" (Left : Set; Right : Set) return Boolean is
+ (Left.Content <= Right.Content);
---------
-- Add --
---------
- function Add (S : Set; E : Element_Type) return Set is
- (Content => Add (S.Content, Length (S.Content) + 1, E));
+ function Add (Container : Set; Item : Element_Type) return Set is
+ (Content =>
+ Add (Container.Content, Length (Container.Content) + 1, Item));
- ------------------
- -- Intersection --
- ------------------
+ --------------
+ -- Contains --
+ --------------
- function Intersection (S1 : Set; S2 : Set) return Set is
- (Content => Intersection (S1.Content, S2.Content));
+ function Contains (Container : Set; Item : Element_Type) return Boolean is
+ (Find (Container.Content, Item) > 0);
- ------------
- -- Is_Add --
- ------------
+ ---------------------
+ -- Included_Except --
+ ---------------------
- function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
+ function Included_Except
+ (Left : Set;
+ Right : Set;
+ Item : Element_Type) return Boolean
is
- (Mem (Result, E)
- and (for all F of Result => Mem (S, F) or F = E)
- and (for all E of S => Mem (Result, E)));
+ (for all E of Left =>
+ Equivalent_Elements (E, Item) or Contains (Right, E));
- --------------
- -- Is_Empty --
- --------------
+ -----------------------
+ -- Included_In_Union --
+ -----------------------
- function Is_Empty (S : Set) return Boolean is (Length (S.Content) = 0);
+ function Included_In_Union
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
+ is
+ (for all Item of Container =>
+ Contains (Left, Item) or Contains (Right, Item));
- ---------------------
- -- Is_Intersection --
- ---------------------
+ ---------------------------
+ -- Includes_Intersection --
+ ---------------------------
- function Is_Intersection
- (S1 : Set;
- S2 : Set;
- Result : Set) return Boolean
+ function Includes_Intersection
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
is
- ((for all E of Result =>
- Mem (S1, E)
- and Mem (S2, E))
- and (for all E of S1 => (if Mem (S2, E) then Mem (Result, E))));
+ (for all Item of Left =>
+ (if Contains (Right, Item) then Contains (Container, Item)));
+
+ ------------------
+ -- Intersection --
+ ------------------
+
+ function Intersection (Left : Set; Right : Set) return Set is
+ (Content => Intersection (Left.Content, Right.Content));
--------------
- -- Is_Union --
+ -- Is_Empty --
--------------
- function Is_Union (S1 : Set; S2 : Set; Result : Set) return Boolean is
- ((for all E of Result => Mem (S1, E) or Mem (S2, E))
- and (for all E of S1 => Mem (Result, E))
- and (for all E of S2 => Mem (Result, E)));
+ function Is_Empty (Container : Set) return Boolean is
+ (Length (Container.Content) = 0);
------------
-- Length --
------------
- function Length (S : Set) return Count_Type is (Length (S.Content));
-
- ---------
- -- Mem --
- ---------
-
- function Mem (S : Set; E : Element_Type) return Boolean is
- (Find (S.Content, E) > 0);
+ function Length (Container : Set) return Count_Type is
+ (Length (Container.Content));
------------------
-- Num_Overlaps --
------------------
- function Num_Overlaps (S1 : Set; S2 : Set) return Count_Type is
- (Num_Overlaps (S1.Content, S2.Content));
+ function Num_Overlaps (Left : Set; Right : Set) return Count_Type is
+ (Num_Overlaps (Left.Content, Right.Content));
------------
-- Remove --
------------
- function Remove (S : Set; E : Element_Type) return Set is
- (Content => Remove (S.Content, Find (S.Content, E)));
+ function Remove (Container : Set; Item : Element_Type) return Set is
+ (Content => Remove (Container.Content, Find (Container.Content, Item)));
-----------
-- Union --
-----------
- function Union (S1 : Set; S2 : Set) return Set is
- (Content => Union (S1.Content, S2.Content));
+ function Union (Left : Set; Right : Set) return Set is
+ (Content => Union (Left.Content, Right.Content));
end Ada.Containers.Functional_Sets;
generic
type Element_Type (<>) is private;
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
-
+ with
+ function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
package Ada.Containers.Functional_Sets with SPARK_Mode is
- pragma Assertion_Policy (Post => Ignore);
-
type Set is private with
Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0,
Iterable => (First => Iter_First,
-- "For in" quantification over sets should not be used.
-- "For of" quantification over sets iterates over elements.
- -- Sets are axiomatized using Mem, which encodes whether an element is
+ -----------------------
+ -- Basic operations --
+ -----------------------
+
+ -- Sets are axiomatized using Contains, which encodes whether an element is
-- contained in a set. The length of a set is also added to protect Add
-- against overflows but it is not actually modeled.
- function Mem (S : Set; E : Element_Type) return Boolean with
+ function Contains (Container : Set; Item : Element_Type) return Boolean with
Global => null;
+ -- Return True if Item is contained in Container
- function Length (S : Set) return Count_Type with
+ function Length (Container : Set) return Count_Type with
Global => null;
+ -- Return the number of elements in Container
+
+ ------------------------
+ -- Property Functions --
+ ------------------------
- function "<=" (S1 : Set; S2 : Set) return Boolean with
+ function "<=" (Left : Set; Right : Set) return Boolean with
-- Set inclusion
Global => null,
- Post => "<="'Result = (for all E of S1 => Mem (S2, E));
+ Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
- function "=" (S1 : Set; S2 : Set) return Boolean with
+ function "=" (Left : Set; Right : Set) return Boolean with
-- Extensional equality over sets
Global => null,
Post =>
"="'Result =
- ((for all E of S1 => Mem (S2, E))
- and (for all E of S2 => Mem (S1, E)));
+ ((for all Item of Left => Contains (Right, Item))
+ and (for all Item of Right => Contains (Left, Item)));
- pragma Warnings (Off, "unused variable ""E""");
- function Is_Empty (S : Set) return Boolean with
+ pragma Warnings (Off, "unused variable ""Item""");
+ function Is_Empty (Container : Set) return Boolean with
-- A set is empty if it contains no element
Global => null,
- Post => Is_Empty'Result = (for all E of S => False);
- pragma Warnings (On, "unused variable ""E""");
+ Post => Is_Empty'Result = (for all Item of Container => False);
+ pragma Warnings (On, "unused variable ""Item""");
- function Is_Add (S : Set; E : Element_Type; Result : Set) return Boolean
- -- Returns True if Result is S augmented with E
+ function Included_Except
+ (Left : Set;
+ Right : Set;
+ Item : Element_Type) return Boolean
+ -- Return True if Left contains only elements of Right except possibly
+ -- Item.
with
Global => null,
Post =>
- Is_Add'Result =
- (Mem (Result, E)
- and not Mem (S, E)
- and (for all F of Result => Mem (S, F) or F = E)
- and (for all E of S => Mem (Result, E)));
-
- function Add (S : Set; E : Element_Type) return Set with
- -- Returns S augmented with E.
- -- Is_Add (S, E, Result) should be used instead of Result = Add (S, E)
- -- whenever possible both for execution and for proof.
+ Included_Except'Result =
+ (for all E of Left =>
+ Contains (Right, E) or Equivalent_Elements (E, Item));
+
+ function Includes_Intersection
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
+ with
+ -- Return True if every element of the intersection of Left and Right is
+ -- in Container.
Global => null,
- Pre => not Mem (S, E) and Length (S) < Count_Type'Last,
Post =>
- Length (Add'Result) = Length (S) + 1
- and Is_Add (S, E, Add'Result);
-
- function Remove (S : Set; E : Element_Type) return Set with
- -- Returns S without E.
- -- Is_Add (Result, E, S) should be used instead of Result = Remove (S, E)
- -- whenever possible both for execution and for proof.
+ Includes_Intersection'Result =
+ (for all Item of Left =>
+ (if Contains (Right, Item) then Contains (Container, Item)));
+
+ function Included_In_Union
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
+ with
+ -- Return True if every element of Container is the union of Left and Right
Global => null,
- Pre => Mem (S, E),
Post =>
- Length (Remove'Result) = Length (S) - 1
- and Is_Add (Remove'Result, E, S);
+ Included_In_Union'Result =
+ (for all Item of Container =>
+ Contains (Left, Item) or Contains (Right, Item));
- function Is_Intersection
- (S1 : Set;
- S2 : Set;
- Result : Set) return Boolean
- with
- -- Returns True if Result is the intersection of S1 and S2
+ function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
+ -- Number of elements that are both in Left and Right
Global => null,
Post =>
- Is_Intersection'Result =
- ((for all E of Result => Mem (S1, E) and Mem (S2, E))
- and (for all E of S1 => (if Mem (S2, E) then Mem (Result, E))));
+ Num_Overlaps'Result <= Length (Left)
+ and Num_Overlaps'Result <= Length (Right)
+ and (if Num_Overlaps'Result = 0 then
+ (for all Item of Left => not Contains (Right, Item)));
+
+ ----------------------------
+ -- Construction Functions --
+ ----------------------------
- function Num_Overlaps (S1 : Set; S2 : Set) return Count_Type with
- -- Number of elements that are both in S1 and S2
+ -- For better efficiency of both proofs and execution, avoid using
+ -- construction functions in annotations and rather use property functions.
+
+ function Add (Container : Set; Item : Element_Type) return Set with
+ -- Return a new set containing all the elements of Container plus E
Global => null,
+ Pre =>
+ not Contains (Container, Item)
+ and Length (Container) < Count_Type'Last,
Post =>
- Num_Overlaps'Result <= Length (S1)
- and Num_Overlaps'Result <= Length (S2)
- and (if Num_Overlaps'Result = 0 then
- (for all E of S1 => not Mem (S2, E)));
+ Length (Add'Result) = Length (Container) + 1
+ and Contains (Add'Result, Item)
+ and Container <= Add'Result
+ and Included_Except (Add'Result, Container, Item);
- function Intersection (S1 : Set; S2 : Set) return Set with
- -- Returns the intersection of S1 and S2.
- -- Intersection (S1, S2, Result) should be used instead of
- -- Result = Intersection (S1, S2) whenever possible both for execution and
- -- for proof.
+ function Remove (Container : Set; Item : Element_Type) return Set with
+ -- Return a new set containing all the elements of Container except E
Global => null,
+ Pre => Contains (Container, Item),
Post =>
- Length (Intersection'Result) = Num_Overlaps (S1, S2)
- and Is_Intersection (S1, S2, Intersection'Result);
+ Length (Remove'Result) = Length (Container) - 1
+ and not Contains (Remove'Result, Item)
+ and Remove'Result <= Container
+ and Included_Except (Container, Remove'Result, Item);
- function Is_Union (S1 : Set; S2 : Set; Result : Set) return Boolean with
- -- Returns True if Result is the union of S1 and S2
+ function Intersection (Left : Set; Right : Set) return Set with
+ -- Returns the intersection of Left and Right
Global => null,
Post =>
- Is_Union'Result =
- ((for all E of Result => Mem (S1, E) or Mem (S2, E))
- and (for all E of S1 => Mem (Result, E))
- and (for all E of S2 => Mem (Result, E)));
+ Length (Intersection'Result) = Num_Overlaps (Left, Right)
+ and Intersection'Result <= Left
+ and Intersection'Result <= Right
+ and Includes_Intersection (Intersection'Result, Left, Right);
- function Union (S1 : Set; S2 : Set) return Set with
- -- Returns the union of S1 and S2.
- -- Is_Union (S1, S2, Result) should be used instead of
- -- Result = Union (S1, S2) whenever possible both for execution and for
- -- proof.
+ function Union (Left : Set; Right : Set) return Set with
+ -- Returns the union of Left and Right
Global => null,
Pre =>
- Length (S1) - Num_Overlaps (S1, S2) <= Count_Type'Last - Length (S2),
+ Length (Left) - Num_Overlaps (Left, Right)
+ <= Count_Type'Last - Length (Right),
Post =>
Length (Union'Result) =
- Length (S1) - Num_Overlaps (S1, S2) + Length (S2)
- and Is_Union (S1, S2, Union'Result);
+ Length (Left) - Num_Overlaps (Left, Right) + Length (Right)
+ and Left <= Union'Result
+ and Right <= Union'Result
+ and Included_In_Union (Union'Result, Left, Right);
---------------------------
-- Iteration Primitives --
type Private_Key is private;
- function Iter_First (S : Set) return Private_Key with
+ function Iter_First (Container : Set) return Private_Key with
Global => null;
- function Iter_Has_Element (S : Set; K : Private_Key) return Boolean with
+ function Iter_Has_Element
+ (Container : Set;
+ Key : Private_Key) return Boolean
+ with
Global => null;
- function Iter_Next (S : Set; K : Private_Key) return Private_Key with
+ function Iter_Next (Container : Set; Key : Private_Key) return Private_Key
+ with
Global => null,
- Pre => Iter_Has_Element (S, K);
+ Pre => Iter_Has_Element (Container, Key);
- function Iter_Element (S : Set; K : Private_Key) return Element_Type with
+ function Iter_Element
+ (Container : Set;
+ Key : Private_Key) return Element_Type
+ with
Global => null,
- Pre => Iter_Has_Element (S, K);
- pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Mem);
+ Pre => Iter_Has_Element (Container, Key);
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains);
private
type Private_Key is new Count_Type;
- function Iter_First (S : Set) return Private_Key is (1);
+ function Iter_First (Container : Set) return Private_Key is (1);
- function Iter_Has_Element (S : Set; K : Private_Key) return Boolean is
- (Count_Type (K) in 1 .. Containers.Length (S.Content));
+ function Iter_Has_Element
+ (Container : Set;
+ Key : Private_Key) return Boolean
+ is
+ (Count_Type (Key) in 1 .. Containers.Length (Container.Content));
- function Iter_Next (S : Set; K : Private_Key) return Private_Key is
- (if K = Private_Key'Last then 0 else K + 1);
+ function Iter_Next (Container : Set; Key : Private_Key) return Private_Key
+ is
+ (if Key = Private_Key'Last then 0 else Key + 1);
- function Iter_Element (S : Set; K : Private_Key) return Element_Type is
- (Containers.Get (S.Content, Count_Type (K)));
+ function Iter_Element
+ (Container : Set;
+ Key : Private_Key) return Element_Type
+ is
+ (Containers.Get (Container.Content, Count_Type (Key)));
end Ada.Containers.Functional_Sets;
package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
use Containers;
- ---------
- -- "=" --
- ---------
-
- function "=" (S1 : Sequence; S2 : Sequence) return Boolean is
- (S1.Content = S2.Content);
-
---------
-- "<" --
---------
- function "<" (S1 : Sequence; S2 : Sequence) return Boolean is
- (Length (S1.Content) < Length (S2.Content)
- and then (for all I in Index_Type'First .. Last (S1) =>
- Get (S1.Content, I) = Get (S2.Content, I)));
+ function "<" (Left : Sequence; Right : Sequence) return Boolean is
+ (Length (Left.Content) < Length (Right.Content)
+ and then (for all I in Index_Type'First .. Last (Left) =>
+ Get (Left.Content, I) = Get (Right.Content, I)));
----------
-- "<=" --
----------
- function "<=" (S1 : Sequence; S2 : Sequence) return Boolean is
- (Length (S1.Content) <= Length (S2.Content)
- and then (for all I in Index_Type'First .. Last (S1) =>
- Get (S1.Content, I) = Get (S2.Content, I)));
+ function "<=" (Left : Sequence; Right : Sequence) return Boolean is
+ (Length (Left.Content) <= Length (Right.Content)
+ and then (for all I in Index_Type'First .. Last (Left) =>
+ Get (Left.Content, I) = Get (Right.Content, I)));
---------
- -- Add --
+ -- "=" --
---------
- function Add (S : Sequence; E : Element_Type) return Sequence is
- (Content => Add (S.Content,
- Index_Type'Val
- (Index_Type'Pos (Index_Type'First) +
- Length (S.Content)),
- E));
+ function "=" (Left : Sequence; Right : Sequence) return Boolean is
+ (Left.Content = Right.Content);
---------
- -- Get --
+ -- Add --
---------
- function Get (S : Sequence; N : Extended_Index) return Element_Type is
- (Get (S.Content, N));
-
- ------------
- -- Insert --
- ------------
-
- function Insert
- (S : Sequence;
- N : Index_Type;
- E : Element_Type) return Sequence
+ function Add (Container : Sequence; New_Item : Element_Type) return Sequence
is
- (Content => Add (S.Content, N, E));
-
- ------------
- -- Is_Add --
- ------------
+ (Content => Add (Container.Content,
+ Index_Type'Val
+ (Index_Type'Pos (Index_Type'First) +
+ Length (Container.Content)),
+ New_Item));
- function Is_Add
- (S : Sequence;
- E : Element_Type;
- Result : Sequence) return Boolean
+ function Add
+ (Container : Sequence;
+ Position : Index_Type;
+ New_Item : Element_Type) return Sequence
+ is
+ (Content => Add (Container.Content, Position, New_Item));
+
+ --------------------
+ -- Constant_Range --
+ --------------------
+
+ function Constant_Range
+ (Container : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Item : Element_Type) return Boolean is
+ begin
+ for I in Fst .. Lst loop
+ if Get (Container.Content, I) /= Item then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end Constant_Range;
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Item : Element_Type) return Boolean
is
- (Length (Result) = Length (S) + 1
- and then Get (Result, Index_Type'Val
- ((Index_Type'Pos (Index_Type'First) - 1) +
- Length (Result))) = E
- and then
- (for all M in Index_Type'First ..
- (Index_Type'Val
- ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) =>
- Get (Result, M) = Get (S, M)));
+ begin
+ for I in Fst .. Lst loop
+ if Get (Container.Content, I) = Item then
+ return True;
+ end if;
+ end loop;
+ return False;
+ end Contains;
+
+ ------------------
+ -- Range_Except --
+ ------------------
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ Position : Index_Type) return Boolean
+ is
+ begin
+ if Length (Left.Content) /= Length (Right.Content) then
+ return False;
+ end if;
+
+ for I in Index_Type'First .. Last (Left) loop
+ if I /= Position
+ and then Get (Left.Content, I) /= Get (Right.Content, I)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Equal_Except;
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ X, Y : Index_Type) return Boolean
+ is
+ begin
+ if Length (Left.Content) /= Length (Right.Content) then
+ return False;
+ end if;
+
+ for I in Index_Type'First .. Last (Left) loop
+ if I /= X and then I /= Y
+ and then Get (Left.Content, I) /= Get (Right.Content, I)
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Equal_Except;
- ------------
- -- Is_Set --
- ------------
+ ---------
+ -- Get --
+ ---------
- function Is_Set
- (S : Sequence;
- N : Index_Type;
- E : Element_Type;
- Result : Sequence) return Boolean
+ function Get (Container : Sequence;
+ Position : Extended_Index) return Element_Type
is
- (N in Index_Type'First ..
- (Index_Type'Val
- ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)))
- and then Length (Result) = Length (S)
- and then Get (Result, N) = E
- and then
- (for all M in Index_Type'First ..
- (Index_Type'Val
- ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))) =>
- (if M /= N then Get (Result, M) = Get (S, M))));
+ (Get (Container.Content, Position));
----------
-- Last --
----------
- function Last (S : Sequence) return Extended_Index is
- (Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S)));
+ function Last (Container : Sequence) return Extended_Index is
+ (Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1)
+ + Length (Container)));
------------
-- Length --
------------
- function Length (S : Sequence) return Count_Type is
- (Length (S.Content));
+ function Length (Container : Sequence) return Count_Type is
+ (Length (Container.Content));
+
+ -----------------
+ -- Range_Equal --
+ -----------------
+
+ function Range_Equal
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if Get (Left, I) /= Get (Right, I) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end Range_Equal;
+
+ -------------------
+ -- Range_Shifted --
+ -------------------
+
+ function Range_Shifted
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Offset : Count_Type'Base) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if Get (Left, I)
+ /= Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))
+ then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end Range_Shifted;
------------
-- Remove --
------------
- function Remove (S : Sequence; N : Index_Type) return Sequence is
- (Content => Remove (S.Content, N));
+ function Remove (Container : Sequence;
+ Position : Index_Type) return Sequence
+ is
+ (Content => Remove (Container.Content, Position));
---------
-- Set --
---------
function Set
- (S : Sequence;
- N : Index_Type;
- E : Element_Type) return Sequence
+ (Container : Sequence;
+ Position : Index_Type;
+ New_Item : Element_Type) return Sequence
is
- (Content => Set (S.Content, N, E));
+ (Content => Set (Container.Content, Position, New_Item));
end Ada.Containers.Functional_Vectors;
-- should have at least one more element at the low end than Index_Type.
type Element_Type (<>) is private;
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
-
package Ada.Containers.Functional_Vectors with SPARK_Mode is
- pragma Assertion_Policy (Post => Ignore);
-
subtype Extended_Index is Index_Type'Base range
Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
-- Index_Type with one more element at the low end of the range.
-- Quantification over sequences can be done using the regular
-- quantification over its range or directly on its elements with "for of".
+ -----------------------
+ -- Basic operations --
+ -----------------------
+
-- Sequences are axiomatized using Length and Get, providing respectively
-- the length of a sequence and an accessor to its Nth element:
- function Length (S : Sequence) return Count_Type with
+ function Length (Container : Sequence) return Count_Type with
+ -- Length of a sequence
+
Global => null,
Post =>
(Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
Index_Type'Pos (Index_Type'Last);
- function Last (S : Sequence) return Extended_Index with
+ function Get
+ (Container : Sequence;
+ Position : Extended_Index) return Element_Type
+ -- Access the Element at position Position in Container
+
+ with
Global => null,
- Post =>
+ Pre => Position in Index_Type'First .. Last (Container);
+
+ function Last (Container : Sequence) return Extended_Index with
+ -- Last index of a sequence
+
+ Global => null,
+ Post =>
Last'Result =
- Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + Length (S));
+ Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1)
+ + Length (Container));
+ pragma Annotate (GNATprove, Inline_For_Proof, Last);
function First return Extended_Index is (Index_Type'First);
+ -- First index of a sequence
- function Get (S : Sequence; N : Extended_Index) return Element_Type
- -- Get ranges over Extended_Index so that it can be used for iteration
+ ------------------------
+ -- Property Functions --
+ ------------------------
- with
- Global => null,
- Pre => N in Index_Type'First .. Last (S);
-
- function "=" (S1 : Sequence; S2 : Sequence) return Boolean with
+ function "=" (Left : Sequence; Right : Sequence) return Boolean with
-- Extensional equality over sequences
Global => null,
Post =>
"="'Result =
- (Length (S1) = Length (S2)
- and then (for all N in Index_Type'First .. Last (S1) =>
- Get (S1, N) = Get (S2, N)));
+ (Length (Left) = Length (Right)
+ and then (for all N in Index_Type'First .. Last (Left) =>
+ Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "=");
- function "<" (S1 : Sequence; S2 : Sequence) return Boolean with
- -- S1 is a strict subsequence of S2
+ function "<" (Left : Sequence; Right : Sequence) return Boolean with
+ -- Left is a strict subsequence of Right
Global => null,
Post =>
"<"'Result =
- (Length (S1) < Length (S2)
- and then (for all N in Index_Type'First .. Last (S1) =>
- Get (S1, N) = Get (S2, N)));
+ (Length (Left) < Length (Right)
+ and then (for all N in Index_Type'First .. Last (Left) =>
+ Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "<");
- function "<=" (S1 : Sequence; S2 : Sequence) return Boolean with
- -- S1 is a subsequence of S2
+ function "<=" (Left : Sequence; Right : Sequence) return Boolean with
+ -- Left is a subsequence of Right
Global => null,
Post =>
"<="'Result =
- (Length (S1) <= Length (S2)
- and then (for all N in Index_Type'First .. Last (S1) =>
- Get (S1, N) = Get (S2, N)));
-
- function Is_Set
- (S : Sequence;
- N : Index_Type;
- E : Element_Type;
- Result : Sequence) return Boolean
- -- Returns True if Result is S, where the Nth element has been replaced by
- -- E.
+ (Length (Left) <= Length (Right)
+ and then (for all N in Index_Type'First .. Last (Left) =>
+ Get (Left, N) = Get (Right, N)));
+ pragma Annotate (GNATprove, Inline_For_Proof, "<=");
+
+ function Contains
+ (Container : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Item : Element_Type)
+ return Boolean
+ -- Returns True if Item occurs in the range from Fst to Lst of Container
with
Global => null,
+ Pre => Lst <= Last (Container),
Post =>
- Is_Set'Result =
- (N in Index_Type'First .. Last (S)
- and then Length (Result) = Length (S)
- and then Get (Result, N) = E
- and then (for all M in Index_Type'First .. Last (S) =>
- (if M /= N then Get (Result, M) = Get (S, M))));
+ Contains'Result =
+ (for some I in Fst .. Lst => Get (Container, I) = Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, Contains);
+
+ function Constant_Range
+ (Container : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Item : Element_Type)
+ return Boolean
+ -- Returns True if every element of the range from Fst to Lst of Container
+ -- is equal to Item.
- function Set
- (S : Sequence;
- N : Index_Type;
- E : Element_Type) return Sequence
- -- Returns S, where the Nth element has been replaced by E.
- -- Is_Set (S, N, E, Result) should be used instead of
- -- Result = Set (S, N, E) whenever possible both for execution and for
- -- proof.
+ with
+ Global => null,
+ Pre => Lst <= Last (Container),
+ Post =>
+ Constant_Range'Result =
+ (for all I in Fst .. Lst => Get (Container, I) = Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ Position : Index_Type) return Boolean
+ -- Returns True is Left and Right are the same except at position Position
+
+ with
+ Global => null,
+ Pre => Position <= Last (Left),
+ Post =>
+ Equal_Except'Result =
+ (Length (Left) = Length (Right)
+ and then (for all I in Index_Type'First .. Last (Left) =>
+ (if I /= Position then Get (Left, I) = Get (Right, I))));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
+
+ function Equal_Except
+ (Left : Sequence;
+ Right : Sequence;
+ X, Y : Index_Type) return Boolean
+ -- Returns True is Left and Right are the same except at positions X and Y
with
Global => null,
- Pre => N in Index_Type'First .. Last (S),
- Post => Is_Set (S, N, E, Set'Result);
+ Pre => X <= Last (Left) and Y <= Last (Left),
+ Post =>
+ Equal_Except'Result =
+ (Length (Left) = Length (Right)
+ and then (for all I in Index_Type'First .. Last (Left) =>
+ (if I /= X and I /= Y then Get (Left, I) = Get (Right, I))));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
+
+ function Range_Equal
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index) return Boolean
+ -- Returns True if the ranges from Fst to Lst contain the same elements in
+ -- Left and Right.
- function Is_Add
- (S : Sequence;
- E : Element_Type;
- Result : Sequence) return Boolean
- -- Returns True if Result is S appended with E
+ with
+ Global => null,
+ Pre => Lst <= Last (Left) and Lst <= Last (Right),
+ Post =>
+ Range_Equal'Result =
+ (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I));
+ pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
+
+ function Range_Shifted
+ (Left : Sequence;
+ Right : Sequence;
+ Fst : Index_Type;
+ Lst : Extended_Index;
+ Offset : Count_Type'Base) return Boolean
+ -- Returns True if the range from Fst to Lst in Left contains the same
+ -- elements as the range from Fst + Offset to Lst + Offset in Right.
with
Global => null,
+ Pre => Lst <= Last (Left)
+ and Offset in
+ Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
+ (Index_Type'Pos (Index_Type'First) - 1)
+ + Length (Right) - Index_Type'Pos (Lst),
Post =>
- Is_Add'Result =
- (Length (Result) = Length (S) + 1
- and then Get (Result, Last (Result)) = E
- and then (for all M in Index_Type'First .. Last (S) =>
- Get (Result, M) = Get (S, M)));
+ Range_Shifted'Result =
+ ((for all I in Fst .. Lst =>
+ Get (Left, I)
+ = Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)))
+ and
+ (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) ..
+ Index_Type'Val (Index_Type'Pos (Lst) + Offset) =>
+ Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset))
+ = Get (Right, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
+
+ ----------------------------
+ -- Construction Functions --
+ ----------------------------
+
+ -- For better efficiency of both proofs and execution, avoid using
+ -- construction functions in annotations and rather use property functions.
- function Add (S : Sequence; E : Element_Type) return Sequence with
- -- Returns S appended with E.
- -- Is_Add (S, E, Result) should be used instead of Result = Add (S, E)
- -- whenever possible both for execution and for proof.
+ function Set
+ (Container : Sequence;
+ Position : Index_Type;
+ New_Item : Element_Type) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- except for the one at position Position which is replaced by New_Item.
+ with
Global => null,
- Pre => Length (S) < Count_Type'Last and Last (S) < Index_Type'Last,
- Post => Is_Add (S, E, Add'Result);
+ Pre => Position in Index_Type'First .. Last (Container),
+ Post => Get (Set'Result, Position) = New_Item
+ and then Equal_Except (Container, Set'Result, Position);
- function Insert
- (S : Sequence;
- N : Index_Type;
- E : Element_Type) return Sequence
+ function Add (Container : Sequence; New_Item : Element_Type) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- plus New_Item at the end.
+
+ with
+ Global => null,
+ Pre =>
+ Length (Container) < Count_Type'Last
+ and then Last (Container) < Index_Type'Last,
+ Post =>
+ Length (Add'Result) = Length (Container) + 1
+ and then Get (Add'Result, Last (Add'Result)) = New_Item
+ and then Container <= Add'Result;
+
+ function Add
+ (Container : Sequence;
+ Position : Index_Type;
+ New_Item : Element_Type) return Sequence
with
- -- Returns S with E inserted at index I
+ -- Returns a new sequence which contains the same elements as Container
+ -- except that New_Item has been inserted at position Position.
Global => null,
Pre =>
- Length (S) < Count_Type'Last
- and then Last (S) < Index_Type'Last
- and then N <= Extended_Index'Succ (Last (S)),
+ Length (Container) < Count_Type'Last
+ and then Last (Container) < Index_Type'Last
+ and then Position <= Extended_Index'Succ (Last (Container)),
Post =>
- Length (Insert'Result) = Length (S) + 1
- and then Get (Insert'Result, N) = E
+ Length (Add'Result) = Length (Container) + 1
+ and then Get (Add'Result, Position) = New_Item
and then
- (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
- Get (Insert'Result, M) = Get (S, M))
+ Range_Equal (Left => Container,
+ Right => Add'Result,
+ Fst => Index_Type'First,
+ Lst => Index_Type'Pred (Position))
and then
- (for all M in Extended_Index'Succ (N) .. Last (Insert'Result) =>
- Get (Insert'Result, M) = Get (S, Extended_Index'Pred (M)))
- and then
- (for all M in N .. Last (S) =>
- Get (Insert'Result, Extended_Index'Succ (M)) = Get (S, M));
-
- function Remove (S : Sequence; N : Index_Type) return Sequence with
- -- Returns S without the element at index N
+ Range_Shifted (Left => Container,
+ Right => Add'Result,
+ Fst => Position,
+ Lst => Last (Container),
+ Offset => 1);
+
+ function Remove
+ (Container : Sequence;
+ Position : Index_Type) return Sequence
+ -- Returns a new sequence which contains the same elements as Container
+ -- except that the element at position Position has been removed.
+ with
Global => null,
Pre =>
- Length (S) < Count_Type'Last
- and Last (S) < Index_Type'Last
- and N in Index_Type'First .. Last (S),
+ Length (Container) < Count_Type'Last
+ and Last (Container) < Index_Type'Last
+ and Position in Index_Type'First .. Last (Container),
Post =>
- Length (Remove'Result) = Length (S) - 1
- and then
- (for all M in Index_Type'First .. Extended_Index'Pred (N) =>
- Get (Remove'Result, M) = Get (S, M))
+ Length (Remove'Result) = Length (Container) - 1
and then
- (for all M in N .. Last (Remove'Result) =>
- Get (Remove'Result, M) = Get (S, Extended_Index'Succ (M)))
+ Range_Equal (Left => Container,
+ Right => Remove'Result,
+ Fst => Index_Type'First,
+ Lst => Index_Type'Pred (Position))
and then
- (for all M in Extended_Index'Succ (N) .. Last (S) =>
- Get (Remove'Result, Extended_Index'Pred (M)) = Get (S, M));
+ Range_Shifted (Left => Remove'Result,
+ Right => Container,
+ Fst => Position,
+ Lst => Last (Remove'Result),
+ Offset => 1);
---------------------------
-- Iteration Primitives --
---------------------------
- function Iter_First (S : Sequence) return Extended_Index with
+ function Iter_First (Container : Sequence) return Extended_Index with
Global => null;
- function Iter_Has_Element (S : Sequence; I : Extended_Index) return Boolean
+ function Iter_Has_Element
+ (Container : Sequence;
+ Position : Extended_Index) return Boolean
with
Global => null,
- Post => Iter_Has_Element'Result = (I in Index_Type'First .. Last (S));
+ Post => Iter_Has_Element'Result =
+ (Position in Index_Type'First .. Last (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
- function Iter_Next (S : Sequence; I : Extended_Index) return Extended_Index
+ function Iter_Next
+ (Container : Sequence;
+ Position : Extended_Index) return Extended_Index
with
Global => null,
- Pre => Iter_Has_Element (S, I);
+ Pre => Iter_Has_Element (Container, Position);
private
Content : Containers.Container;
end record;
- function Iter_First (S : Sequence) return Extended_Index is
+ function Iter_First (Container : Sequence) return Extended_Index is
(Index_Type'First);
-
function Iter_Next
- (S : Sequence;
- I : Extended_Index) return Extended_Index
+ (Container : Sequence;
+ Position : Extended_Index) return Extended_Index
is
- (if I = Extended_Index'Last then Extended_Index'First
- else Extended_Index'Succ (I));
+ (if Position = Extended_Index'Last then Extended_Index'First
+ else Extended_Index'Succ (Position));
function Iter_Has_Element
- (S : Sequence;
- I : Extended_Index) return Boolean
+ (Container : Sequence;
+ Position : Extended_Index) return Boolean
is
- (I in Index_Type'First ..
- (Index_Type'Val
- ((Index_Type'Pos (Index_Type'First) - 1) + Length (S))));
+ (Position in Index_Type'First ..
+ (Index_Type'Val
+ ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))));
end Ada.Containers.Functional_Vectors;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- A D A . E X C E P T I O N S --
--- --
--- B o d y --
--- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
--- --
--- GNAT is free software; you can redistribute it and/or modify it under --
--- terms of the GNU General Public License as published by the Free Soft- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. --
--- --
--- As a special exception under Section 7 of GPL version 3, you are granted --
--- additional permissions described in the GCC Runtime Library Exception, --
--- version 3.1, as published by the Free Software Foundation. --
--- --
--- You should have received a copy of the GNU General Public License and --
--- a copy of the GCC Runtime Library Exception along with this program; --
--- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
--- <http://www.gnu.org/licenses/>. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
-pragma Style_Checks (All_Checks);
--- No subprogram ordering check, due to logical grouping
-
-pragma Polling (Off);
--- We must turn polling off for this unit, because otherwise we get
--- elaboration circularities with System.Exception_Tables.
-
-with System; use System;
-with System.Exceptions; use System.Exceptions;
-with System.Exceptions_Debug; use System.Exceptions_Debug;
-with System.Standard_Library; use System.Standard_Library;
-with System.Soft_Links; use System.Soft_Links;
-with System.WCh_Con; use System.WCh_Con;
-with System.WCh_StW; use System.WCh_StW;
-
-pragma Warnings (Off);
--- Suppress complaints about Symbolic not being referenced, and about it not
--- having pragma Preelaborate.
-with System.Traceback.Symbolic;
--- Bring Symbolic into the closure. If it is the s-trasym-dwarf.adb version,
--- it will install symbolic tracebacks as the default decorator. Otherwise,
--- symbolic tracebacks are not supported, and we fall back to hexadecimal
--- addresses.
-pragma Warnings (On);
-
-package body Ada.Exceptions is
-
- pragma Suppress (All_Checks);
- -- We definitely do not want exceptions occurring within this unit, or
- -- we are in big trouble. If an exceptional situation does occur, better
- -- that it not be raised, since raising it can cause confusing chaos.
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- -- Note: the exported subprograms in this package body are called directly
- -- from C clients using the given external name, even though they are not
- -- technically visible in the Ada sense.
-
- function Code_Address_For_AAA return System.Address;
- function Code_Address_For_ZZZ return System.Address;
- -- Return start and end of procedures in this package
- --
- -- These procedures are used to provide exclusion bounds in
- -- calls to Call_Chain at exception raise points from this unit. The
- -- purpose is to arrange for the exception tracebacks not to include
- -- frames from subprograms involved in the raise process, as these are
- -- meaningless from the user's standpoint.
- --
- -- For these bounds to be meaningful, we need to ensure that the object
- -- code for the subprograms involved in processing a raise is located
- -- after the object code Code_Address_For_AAA and before the object
- -- code Code_Address_For_ZZZ. This will indeed be the case as long as
- -- the following rules are respected:
- --
- -- 1) The bodies of the subprograms involved in processing a raise
- -- are located after the body of Code_Address_For_AAA and before the
- -- body of Code_Address_For_ZZZ.
- --
- -- 2) No pragma Inline applies to any of these subprograms, as this
- -- could delay the corresponding assembly output until the end of
- -- the unit.
-
- procedure Call_Chain (Excep : EOA);
- -- Store up to Max_Tracebacks in Excep, corresponding to the current
- -- call chain.
-
- function Image (Index : Integer) return String;
- -- Return string image corresponding to Index
-
- procedure To_Stderr (S : String);
- pragma Export (Ada, To_Stderr, "__gnat_to_stderr");
- -- Little routine to output string to stderr that is also used
- -- in the tasking run time.
-
- procedure To_Stderr (C : Character);
- pragma Inline (To_Stderr);
- pragma Export (Ada, To_Stderr, "__gnat_to_stderr_char");
- -- Little routine to output a character to stderr, used by some of
- -- the separate units below.
-
- package Exception_Data is
-
- -----------------------------------
- -- Exception Message Subprograms --
- -----------------------------------
-
- procedure Set_Exception_C_Msg
- (Excep : EOA;
- Id : Exception_Id;
- Msg1 : System.Address;
- Line : Integer := 0;
- Column : Integer := 0;
- Msg2 : System.Address := System.Null_Address);
- -- This routine is called to setup the exception referenced by X
- -- to contain the indicated Id value and message. Msg1 is a null
- -- terminated string which is generated as the exception message. If
- -- line is non-zero, then a colon and the decimal representation of
- -- this integer is appended to the message. Ditto for Column. When Msg2
- -- is non-null, a space and this additional null terminated string is
- -- added to the message.
-
- procedure Set_Exception_Msg
- (Excep : EOA;
- Id : Exception_Id;
- Message : String);
- -- This routine is called to setup the exception referenced by X
- -- to contain the indicated Id value and message. Message is a string
- -- which is generated as the exception message.
-
- ---------------------------------------
- -- Exception Information Subprograms --
- ---------------------------------------
-
- function Untailored_Exception_Information
- (X : Exception_Occurrence) return String;
- -- This is used by Stream_Attributes.EO_To_String to convert an
- -- Exception_Occurrence to a String for the stream attributes.
- -- String_To_EO understands the format, as documented here.
- --
- -- The format of the string is as follows:
- --
- -- raised <exception name> : <message>
- -- (" : <message>" is present only if Exception_Message is not empty)
- -- PID=nnnn (only if nonzero)
- -- Call stack traceback locations: (only if at least one location)
- -- <0xyyyyyyyy 0xyyyyyyyy ...> (is recorded)
- --
- -- The lines are separated by a ASCII.LF character.
- -- The nnnn is the partition Id given as decimal digits.
- -- The 0x... line represents traceback program counter locations, in
- -- execution order with the first one being the exception location.
- --
- -- The Exception_Name and Message lines are omitted in the abort
- -- signal case, since this is not really an exception.
- --
- -- Note: If the format of the generated string is changed, please note
- -- that an equivalent modification to the routine String_To_EO must be
- -- made to preserve proper functioning of the stream attributes.
-
- function Exception_Information (X : Exception_Occurrence) return String;
- -- This is the implementation of Ada.Exceptions.Exception_Information,
- -- as defined in the Ada RM.
- --
- -- If no traceback decorator (see GNAT.Exception_Traces) is currently
- -- in place, this is the same as Untailored_Exception_Information.
- -- Otherwise, the decorator is used to produce a symbolic traceback
- -- instead of hexadecimal addresses.
- --
- -- Note that unlike Untailored_Exception_Information, there is no need
- -- to keep the output of Exception_Information stable for streaming
- -- purposes, and in fact the output differs across platforms.
-
- end Exception_Data;
-
- package Exception_Traces is
-
- -------------------------------------------------
- -- Run-Time Exception Notification Subprograms --
- -------------------------------------------------
-
- -- These subprograms provide a common run-time interface to trigger the
- -- actions required when an exception is about to be propagated (e.g.
- -- user specified actions or output of exception information). They are
- -- exported to be usable by the Ada exception handling personality
- -- routine when the GCC 3 mechanism is used.
-
- procedure Notify_Handled_Exception (Excep : EOA);
- pragma Export
- (C, Notify_Handled_Exception, "__gnat_notify_handled_exception");
- -- This routine is called for a handled occurrence is about to be
- -- propagated.
-
- procedure Notify_Unhandled_Exception (Excep : EOA);
- pragma Export
- (C, Notify_Unhandled_Exception, "__gnat_notify_unhandled_exception");
- -- This routine is called when an unhandled occurrence is about to be
- -- propagated.
-
- procedure Unhandled_Exception_Terminate (Excep : EOA);
- pragma No_Return (Unhandled_Exception_Terminate);
- -- This procedure is called to terminate execution following an
- -- unhandled exception. The exception information, including
- -- traceback if available is output, and execution is then
- -- terminated. Note that at the point where this routine is
- -- called, the stack has typically been destroyed.
-
- end Exception_Traces;
-
- package Exception_Propagation is
-
- ---------------------------------------
- -- Exception Propagation Subprograms --
- ---------------------------------------
-
- function Allocate_Occurrence return EOA;
- -- Allocate an exception occurrence (as well as the machine occurrence)
-
- procedure Propagate_Exception (Excep : EOA);
- pragma No_Return (Propagate_Exception);
- -- This procedure propagates the exception represented by Excep
-
- end Exception_Propagation;
-
- package Stream_Attributes is
-
- ----------------------------------
- -- Stream Attribute Subprograms --
- ----------------------------------
-
- function EId_To_String (X : Exception_Id) return String;
- function String_To_EId (S : String) return Exception_Id;
- -- Functions for implementing Exception_Id stream attributes
-
- function EO_To_String (X : Exception_Occurrence) return String;
- function String_To_EO (S : String) return Exception_Occurrence;
- -- Functions for implementing Exception_Occurrence stream
- -- attributes
-
- end Stream_Attributes;
-
- procedure Complete_Occurrence (X : EOA);
- -- Finish building the occurrence: save the call chain and notify the
- -- debugger.
-
- procedure Complete_And_Propagate_Occurrence (X : EOA);
- pragma No_Return (Complete_And_Propagate_Occurrence);
- -- This is a simple wrapper to Complete_Occurrence and
- -- Exception_Propagation.Propagate_Exception.
-
- function Create_Occurrence_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address) return EOA;
- -- Create and build an exception occurrence using exception id E and
- -- nul-terminated message M.
-
- function Create_Machine_Occurrence_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address) return System.Address;
- pragma Export (C, Create_Machine_Occurrence_From_Signal_Handler,
- "__gnat_create_machine_occurrence_from_signal_handler");
- -- Create and build an exception occurrence using exception id E and
- -- nul-terminated message M. Return the machine occurrence.
-
- procedure Raise_Exception_No_Defer
- (E : Exception_Id;
- Message : String := "");
- pragma Export
- (Ada, Raise_Exception_No_Defer,
- "ada__exceptions__raise_exception_no_defer");
- pragma No_Return (Raise_Exception_No_Defer);
- -- Similar to Raise_Exception, but with no abort deferral
-
- procedure Raise_With_Msg (E : Exception_Id);
- pragma No_Return (Raise_With_Msg);
- pragma Export (C, Raise_With_Msg, "__gnat_raise_with_msg");
- -- Raises an exception with given exception id value. A message
- -- is associated with the raise, and has already been stored in the
- -- exception occurrence referenced by the Current_Excep in the TSD.
- -- Abort is deferred before the raise call.
-
- procedure Raise_With_Location_And_Msg
- (E : Exception_Id;
- F : System.Address;
- L : Integer;
- C : Integer := 0;
- M : System.Address := System.Null_Address);
- pragma No_Return (Raise_With_Location_And_Msg);
- -- Raise an exception with given exception id value. A filename and line
- -- number is associated with the raise and is stored in the exception
- -- occurrence and in addition a column and a string message M may be
- -- appended to this (if not null/0).
-
- procedure Raise_Constraint_Error (File : System.Address; Line : Integer);
- pragma No_Return (Raise_Constraint_Error);
- pragma Export (C, Raise_Constraint_Error, "__gnat_raise_constraint_error");
- -- Raise constraint error with file:line information
-
- procedure Raise_Constraint_Error_Msg
- (File : System.Address;
- Line : Integer;
- Column : Integer;
- Msg : System.Address);
- pragma No_Return (Raise_Constraint_Error_Msg);
- pragma Export
- (C, Raise_Constraint_Error_Msg, "__gnat_raise_constraint_error_msg");
- -- Raise constraint error with file:line:col + msg information
-
- procedure Raise_Program_Error (File : System.Address; Line : Integer);
- pragma No_Return (Raise_Program_Error);
- pragma Export (C, Raise_Program_Error, "__gnat_raise_program_error");
- -- Raise program error with file:line information
-
- procedure Raise_Program_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address);
- pragma No_Return (Raise_Program_Error_Msg);
- pragma Export
- (C, Raise_Program_Error_Msg, "__gnat_raise_program_error_msg");
- -- Raise program error with file:line + msg information
-
- procedure Raise_Storage_Error (File : System.Address; Line : Integer);
- pragma No_Return (Raise_Storage_Error);
- pragma Export (C, Raise_Storage_Error, "__gnat_raise_storage_error");
- -- Raise storage error with file:line information
-
- procedure Raise_Storage_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address);
- pragma No_Return (Raise_Storage_Error_Msg);
- pragma Export
- (C, Raise_Storage_Error_Msg, "__gnat_raise_storage_error_msg");
- -- Raise storage error with file:line + reason msg information
-
- -- The exception raising process and the automatic tracing mechanism rely
- -- on some careful use of flags attached to the exception occurrence. The
- -- graph below illustrates the relations between the Raise_ subprograms
- -- and identifies the points where basic flags such as Exception_Raised
- -- are initialized.
-
- -- (i) signs indicate the flags initialization points. R stands for Raise,
- -- W for With, and E for Exception.
-
- -- R_No_Msg R_E R_Pe R_Ce R_Se
- -- | | | | |
- -- +--+ +--+ +---+ | +---+
- -- | | | | |
- -- R_E_No_Defer(i) R_W_Msg(i) R_W_Loc
- -- | | | |
- -- +------------+ | +-----------+ +--+
- -- | | | |
- -- | | | Set_E_C_Msg(i)
- -- | | |
- -- Complete_And_Propagate_Occurrence
-
- procedure Reraise;
- pragma No_Return (Reraise);
- pragma Export (C, Reraise, "__gnat_reraise");
- -- Reraises the exception referenced by the Current_Excep field
- -- of the TSD (all fields of this exception occurrence are set).
- -- Abort is deferred before the reraise operation. Called from
- -- System.Tasking.RendezVous.Exceptional_Complete_RendezVous
-
- procedure Transfer_Occurrence
- (Target : Exception_Occurrence_Access;
- Source : Exception_Occurrence);
- pragma Export (C, Transfer_Occurrence, "__gnat_transfer_occurrence");
- -- Called from s-tasren.adb:Local_Complete_RendezVous and
- -- s-tpobop.adb:Exceptional_Complete_Entry_Body to setup Target from
- -- Source as an exception to be propagated in the caller task. Target is
- -- expected to be a pointer to the fixed TSD occurrence for this task.
-
- --------------------------------
- -- Run-Time Check Subprograms --
- --------------------------------
-
- -- These subprograms raise a specific exception with a reason message
- -- attached. The parameters are the file name and line number in each
- -- case. The names are defined by Exp_Ch11.Get_RT_Exception_Name.
-
- procedure Rcheck_CE_Access_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Access_Parameter
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Discriminant_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Divide_By_Zero
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Explicit_Raise
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Index_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Invalid_Data
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Length_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Exception_Id
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Not_Allowed
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Overflow_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Partition_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Range_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Tag_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Access_Before_Elaboration
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Accessibility_Check
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Address_Of_Intrinsic
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Aliased_Parameters
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_All_Guards_Closed
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Bad_Predicated_Generic_Type
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Current_Task_In_Entry_Body
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Duplicated_Entry_Address
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Explicit_Raise
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Implicit_Return
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Misaligned_Address_Value
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Missing_Return
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Non_Transportable_Actual
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Overlaid_Controlled_Object
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Potentially_Blocking_Operation
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Stubbed_Subprogram_Called
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Unchecked_Union_Restriction
- (File : System.Address; Line : Integer);
- procedure Rcheck_SE_Empty_Storage_Pool
- (File : System.Address; Line : Integer);
- procedure Rcheck_SE_Explicit_Raise
- (File : System.Address; Line : Integer);
- procedure Rcheck_SE_Infinite_Recursion
- (File : System.Address; Line : Integer);
- procedure Rcheck_SE_Object_Too_Large
- (File : System.Address; Line : Integer);
- procedure Rcheck_PE_Stream_Operation_Not_Allowed
- (File : System.Address; Line : Integer);
- procedure Rcheck_CE_Access_Check_Ext
- (File : System.Address; Line, Column : Integer);
- procedure Rcheck_CE_Index_Check_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer);
- procedure Rcheck_CE_Invalid_Data_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer);
- procedure Rcheck_CE_Range_Check_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer);
-
- procedure Rcheck_PE_Finalize_Raised_Exception
- (File : System.Address; Line : Integer);
- -- This routine is separated out because it has quite different behavior
- -- from the others. This is the "finalize/adjust raised exception". This
- -- subprogram is always called with abort deferred, unlike all other
- -- Rcheck_* subprograms, it needs to call Raise_Exception_No_Defer.
-
- pragma Export (C, Rcheck_CE_Access_Check,
- "__gnat_rcheck_CE_Access_Check");
- pragma Export (C, Rcheck_CE_Null_Access_Parameter,
- "__gnat_rcheck_CE_Null_Access_Parameter");
- pragma Export (C, Rcheck_CE_Discriminant_Check,
- "__gnat_rcheck_CE_Discriminant_Check");
- pragma Export (C, Rcheck_CE_Divide_By_Zero,
- "__gnat_rcheck_CE_Divide_By_Zero");
- pragma Export (C, Rcheck_CE_Explicit_Raise,
- "__gnat_rcheck_CE_Explicit_Raise");
- pragma Export (C, Rcheck_CE_Index_Check,
- "__gnat_rcheck_CE_Index_Check");
- pragma Export (C, Rcheck_CE_Invalid_Data,
- "__gnat_rcheck_CE_Invalid_Data");
- pragma Export (C, Rcheck_CE_Length_Check,
- "__gnat_rcheck_CE_Length_Check");
- pragma Export (C, Rcheck_CE_Null_Exception_Id,
- "__gnat_rcheck_CE_Null_Exception_Id");
- pragma Export (C, Rcheck_CE_Null_Not_Allowed,
- "__gnat_rcheck_CE_Null_Not_Allowed");
- pragma Export (C, Rcheck_CE_Overflow_Check,
- "__gnat_rcheck_CE_Overflow_Check");
- pragma Export (C, Rcheck_CE_Partition_Check,
- "__gnat_rcheck_CE_Partition_Check");
- pragma Export (C, Rcheck_CE_Range_Check,
- "__gnat_rcheck_CE_Range_Check");
- pragma Export (C, Rcheck_CE_Tag_Check,
- "__gnat_rcheck_CE_Tag_Check");
- pragma Export (C, Rcheck_PE_Access_Before_Elaboration,
- "__gnat_rcheck_PE_Access_Before_Elaboration");
- pragma Export (C, Rcheck_PE_Accessibility_Check,
- "__gnat_rcheck_PE_Accessibility_Check");
- pragma Export (C, Rcheck_PE_Address_Of_Intrinsic,
- "__gnat_rcheck_PE_Address_Of_Intrinsic");
- pragma Export (C, Rcheck_PE_Aliased_Parameters,
- "__gnat_rcheck_PE_Aliased_Parameters");
- pragma Export (C, Rcheck_PE_All_Guards_Closed,
- "__gnat_rcheck_PE_All_Guards_Closed");
- pragma Export (C, Rcheck_PE_Bad_Predicated_Generic_Type,
- "__gnat_rcheck_PE_Bad_Predicated_Generic_Type");
- pragma Export (C, Rcheck_PE_Current_Task_In_Entry_Body,
- "__gnat_rcheck_PE_Current_Task_In_Entry_Body");
- pragma Export (C, Rcheck_PE_Duplicated_Entry_Address,
- "__gnat_rcheck_PE_Duplicated_Entry_Address");
- pragma Export (C, Rcheck_PE_Explicit_Raise,
- "__gnat_rcheck_PE_Explicit_Raise");
- pragma Export (C, Rcheck_PE_Finalize_Raised_Exception,
- "__gnat_rcheck_PE_Finalize_Raised_Exception");
- pragma Export (C, Rcheck_PE_Implicit_Return,
- "__gnat_rcheck_PE_Implicit_Return");
- pragma Export (C, Rcheck_PE_Misaligned_Address_Value,
- "__gnat_rcheck_PE_Misaligned_Address_Value");
- pragma Export (C, Rcheck_PE_Missing_Return,
- "__gnat_rcheck_PE_Missing_Return");
- pragma Export (C, Rcheck_PE_Non_Transportable_Actual,
- "__gnat_rcheck_PE_Non_Transportable_Actual");
- pragma Export (C, Rcheck_PE_Overlaid_Controlled_Object,
- "__gnat_rcheck_PE_Overlaid_Controlled_Object");
- pragma Export (C, Rcheck_PE_Potentially_Blocking_Operation,
- "__gnat_rcheck_PE_Potentially_Blocking_Operation");
- pragma Export (C, Rcheck_PE_Stream_Operation_Not_Allowed,
- "__gnat_rcheck_PE_Stream_Operation_Not_Allowed");
- pragma Export (C, Rcheck_PE_Stubbed_Subprogram_Called,
- "__gnat_rcheck_PE_Stubbed_Subprogram_Called");
- pragma Export (C, Rcheck_PE_Unchecked_Union_Restriction,
- "__gnat_rcheck_PE_Unchecked_Union_Restriction");
- pragma Export (C, Rcheck_SE_Empty_Storage_Pool,
- "__gnat_rcheck_SE_Empty_Storage_Pool");
- pragma Export (C, Rcheck_SE_Explicit_Raise,
- "__gnat_rcheck_SE_Explicit_Raise");
- pragma Export (C, Rcheck_SE_Infinite_Recursion,
- "__gnat_rcheck_SE_Infinite_Recursion");
- pragma Export (C, Rcheck_SE_Object_Too_Large,
- "__gnat_rcheck_SE_Object_Too_Large");
-
- pragma Export (C, Rcheck_CE_Access_Check_Ext,
- "__gnat_rcheck_CE_Access_Check_ext");
- pragma Export (C, Rcheck_CE_Index_Check_Ext,
- "__gnat_rcheck_CE_Index_Check_ext");
- pragma Export (C, Rcheck_CE_Invalid_Data_Ext,
- "__gnat_rcheck_CE_Invalid_Data_ext");
- pragma Export (C, Rcheck_CE_Range_Check_Ext,
- "__gnat_rcheck_CE_Range_Check_ext");
-
- -- None of these procedures ever returns (they raise an exception). By
- -- using pragma No_Return, we ensure that any junk code after the call,
- -- such as normal return epilogue stuff, can be eliminated).
-
- pragma No_Return (Rcheck_CE_Access_Check);
- pragma No_Return (Rcheck_CE_Null_Access_Parameter);
- pragma No_Return (Rcheck_CE_Discriminant_Check);
- pragma No_Return (Rcheck_CE_Divide_By_Zero);
- pragma No_Return (Rcheck_CE_Explicit_Raise);
- pragma No_Return (Rcheck_CE_Index_Check);
- pragma No_Return (Rcheck_CE_Invalid_Data);
- pragma No_Return (Rcheck_CE_Length_Check);
- pragma No_Return (Rcheck_CE_Null_Exception_Id);
- pragma No_Return (Rcheck_CE_Null_Not_Allowed);
- pragma No_Return (Rcheck_CE_Overflow_Check);
- pragma No_Return (Rcheck_CE_Partition_Check);
- pragma No_Return (Rcheck_CE_Range_Check);
- pragma No_Return (Rcheck_CE_Tag_Check);
- pragma No_Return (Rcheck_PE_Access_Before_Elaboration);
- pragma No_Return (Rcheck_PE_Accessibility_Check);
- pragma No_Return (Rcheck_PE_Address_Of_Intrinsic);
- pragma No_Return (Rcheck_PE_Aliased_Parameters);
- pragma No_Return (Rcheck_PE_All_Guards_Closed);
- pragma No_Return (Rcheck_PE_Bad_Predicated_Generic_Type);
- pragma No_Return (Rcheck_PE_Current_Task_In_Entry_Body);
- pragma No_Return (Rcheck_PE_Duplicated_Entry_Address);
- pragma No_Return (Rcheck_PE_Explicit_Raise);
- pragma No_Return (Rcheck_PE_Implicit_Return);
- pragma No_Return (Rcheck_PE_Misaligned_Address_Value);
- pragma No_Return (Rcheck_PE_Missing_Return);
- pragma No_Return (Rcheck_PE_Non_Transportable_Actual);
- pragma No_Return (Rcheck_PE_Overlaid_Controlled_Object);
- pragma No_Return (Rcheck_PE_Potentially_Blocking_Operation);
- pragma No_Return (Rcheck_PE_Stream_Operation_Not_Allowed);
- pragma No_Return (Rcheck_PE_Stubbed_Subprogram_Called);
- pragma No_Return (Rcheck_PE_Unchecked_Union_Restriction);
- pragma No_Return (Rcheck_PE_Finalize_Raised_Exception);
- pragma No_Return (Rcheck_SE_Empty_Storage_Pool);
- pragma No_Return (Rcheck_SE_Explicit_Raise);
- pragma No_Return (Rcheck_SE_Infinite_Recursion);
- pragma No_Return (Rcheck_SE_Object_Too_Large);
-
- pragma No_Return (Rcheck_CE_Access_Check_Ext);
- pragma No_Return (Rcheck_CE_Index_Check_Ext);
- pragma No_Return (Rcheck_CE_Invalid_Data_Ext);
- pragma No_Return (Rcheck_CE_Range_Check_Ext);
-
- ---------------------------------------------
- -- Reason Strings for Run-Time Check Calls --
- ---------------------------------------------
-
- -- These strings are null-terminated and are used by Rcheck_nn. The
- -- strings correspond to the definitions for Types.RT_Exception_Code.
-
- use ASCII;
-
- Rmsg_00 : constant String := "access check failed" & NUL;
- Rmsg_01 : constant String := "access parameter is null" & NUL;
- Rmsg_02 : constant String := "discriminant check failed" & NUL;
- Rmsg_03 : constant String := "divide by zero" & NUL;
- Rmsg_04 : constant String := "explicit raise" & NUL;
- Rmsg_05 : constant String := "index check failed" & NUL;
- Rmsg_06 : constant String := "invalid data" & NUL;
- Rmsg_07 : constant String := "length check failed" & NUL;
- Rmsg_08 : constant String := "null Exception_Id" & NUL;
- Rmsg_09 : constant String := "null-exclusion check failed" & NUL;
- Rmsg_10 : constant String := "overflow check failed" & NUL;
- Rmsg_11 : constant String := "partition check failed" & NUL;
- Rmsg_12 : constant String := "range check failed" & NUL;
- Rmsg_13 : constant String := "tag check failed" & NUL;
- Rmsg_14 : constant String := "access before elaboration" & NUL;
- Rmsg_15 : constant String := "accessibility check failed" & NUL;
- Rmsg_16 : constant String := "attempt to take address of" &
- " intrinsic subprogram" & NUL;
- Rmsg_17 : constant String := "aliased parameters" & NUL;
- Rmsg_18 : constant String := "all guards closed" & NUL;
- Rmsg_19 : constant String := "improper use of generic subtype" &
- " with predicate" & NUL;
- Rmsg_20 : constant String := "Current_Task referenced in entry" &
- " body" & NUL;
- Rmsg_21 : constant String := "duplicated entry address" & NUL;
- Rmsg_22 : constant String := "explicit raise" & NUL;
- Rmsg_23 : constant String := "finalize/adjust raised exception" & NUL;
- Rmsg_24 : constant String := "implicit return with No_Return" & NUL;
- Rmsg_25 : constant String := "misaligned address value" & NUL;
- Rmsg_26 : constant String := "missing return" & NUL;
- Rmsg_27 : constant String := "overlaid controlled object" & NUL;
- Rmsg_28 : constant String := "potentially blocking operation" & NUL;
- Rmsg_29 : constant String := "stubbed subprogram called" & NUL;
- Rmsg_30 : constant String := "unchecked union restriction" & NUL;
- Rmsg_31 : constant String := "actual/returned class-wide" &
- " value not transportable" & NUL;
- Rmsg_32 : constant String := "empty storage pool" & NUL;
- Rmsg_33 : constant String := "explicit raise" & NUL;
- Rmsg_34 : constant String := "infinite recursion" & NUL;
- Rmsg_35 : constant String := "object too large" & NUL;
- Rmsg_36 : constant String := "stream operation not allowed" & NUL;
-
- -----------------------
- -- Polling Interface --
- -----------------------
-
- type Unsigned is mod 2 ** 32;
-
- Counter : Unsigned := 0;
- pragma Warnings (Off, Counter);
- -- This counter is provided for convenience. It can be used in Poll to
- -- perform periodic but not systematic operations.
-
- procedure Poll is separate;
- -- The actual polling routine is separate, so that it can easily be
- -- replaced with a target dependent version.
-
- --------------------------
- -- Code_Address_For_AAA --
- --------------------------
-
- -- This function gives us the start of the PC range for addresses within
- -- the exception unit itself. We hope that gigi/gcc keep all the procedures
- -- in their original order.
-
- function Code_Address_For_AAA return System.Address is
- begin
- -- We are using a label instead of Code_Address_For_AAA'Address because
- -- on some platforms the latter does not yield the address we want, but
- -- the address of a stub or of a descriptor instead. This is the case at
- -- least on PA-HPUX.
-
- <<Start_Of_AAA>>
- return Start_Of_AAA'Address;
- end Code_Address_For_AAA;
-
- ----------------
- -- Call_Chain --
- ----------------
-
- procedure Call_Chain (Excep : EOA) is separate;
- -- The actual Call_Chain routine is separate, so that it can easily
- -- be dummied out when no exception traceback information is needed.
-
- -------------------
- -- EId_To_String --
- -------------------
-
- function EId_To_String (X : Exception_Id) return String
- renames Stream_Attributes.EId_To_String;
-
- ------------------
- -- EO_To_String --
- ------------------
-
- -- We use the null string to represent the null occurrence, otherwise we
- -- output the Untailored_Exception_Information string for the occurrence.
-
- function EO_To_String (X : Exception_Occurrence) return String
- renames Stream_Attributes.EO_To_String;
-
- ------------------------
- -- Exception_Identity --
- ------------------------
-
- function Exception_Identity
- (X : Exception_Occurrence) return Exception_Id
- is
- begin
- -- Note that the following test used to be here for the original
- -- Ada 95 semantics, but these were modified by AI-241 to require
- -- returning Null_Id instead of raising Constraint_Error.
-
- -- if X.Id = Null_Id then
- -- raise Constraint_Error;
- -- end if;
-
- return X.Id;
- end Exception_Identity;
-
- ---------------------------
- -- Exception_Information --
- ---------------------------
-
- function Exception_Information (X : Exception_Occurrence) return String is
- begin
- if X.Id = Null_Id then
- raise Constraint_Error;
- else
- return Exception_Data.Exception_Information (X);
- end if;
- end Exception_Information;
-
- -----------------------
- -- Exception_Message --
- -----------------------
-
- function Exception_Message (X : Exception_Occurrence) return String is
- begin
- if X.Id = Null_Id then
- raise Constraint_Error;
- else
- return X.Msg (1 .. X.Msg_Length);
- end if;
- end Exception_Message;
-
- --------------------
- -- Exception_Name --
- --------------------
-
- function Exception_Name (Id : Exception_Id) return String is
- begin
- if Id = null then
- raise Constraint_Error;
- else
- return To_Ptr (Id.Full_Name) (1 .. Id.Name_Length - 1);
- end if;
- end Exception_Name;
-
- function Exception_Name (X : Exception_Occurrence) return String is
- begin
- return Exception_Name (X.Id);
- end Exception_Name;
-
- ---------------------------
- -- Exception_Name_Simple --
- ---------------------------
-
- function Exception_Name_Simple (X : Exception_Occurrence) return String is
- Name : constant String := Exception_Name (X);
- P : Natural;
-
- begin
- P := Name'Length;
- while P > 1 loop
- exit when Name (P - 1) = '.';
- P := P - 1;
- end loop;
-
- -- Return result making sure lower bound is 1
-
- declare
- subtype Rname is String (1 .. Name'Length - P + 1);
- begin
- return Rname (Name (P .. Name'Length));
- end;
- end Exception_Name_Simple;
-
- --------------------
- -- Exception_Data --
- --------------------
-
- package body Exception_Data is separate;
- -- This package can be easily dummied out if we do not want the basic
- -- support for exception messages (such as in Ada 83).
-
- ---------------------------
- -- Exception_Propagation --
- ---------------------------
-
- package body Exception_Propagation is separate;
- -- Depending on the actual exception mechanism used (front-end or
- -- back-end based), the implementation will differ, which is why this
- -- package is separated.
-
- ----------------------
- -- Exception_Traces --
- ----------------------
-
- package body Exception_Traces is separate;
- -- Depending on the underlying support for IO the implementation will
- -- differ. Moreover we would like to dummy out this package in case we
- -- do not want any exception tracing support. This is why this package
- -- is separated.
-
- --------------------------------------
- -- Get_Exception_Machine_Occurrence --
- --------------------------------------
-
- function Get_Exception_Machine_Occurrence
- (X : Exception_Occurrence) return System.Address
- is
- begin
- return X.Machine_Occurrence;
- end Get_Exception_Machine_Occurrence;
-
- -----------
- -- Image --
- -----------
-
- function Image (Index : Integer) return String is
- Result : constant String := Integer'Image (Index);
- begin
- if Result (1) = ' ' then
- return Result (2 .. Result'Last);
- else
- return Result;
- end if;
- end Image;
-
- -----------------------
- -- Stream Attributes --
- -----------------------
-
- package body Stream_Attributes is separate;
- -- This package can be easily dummied out if we do not want the
- -- support for streaming Exception_Ids and Exception_Occurrences.
-
- ----------------------------
- -- Raise_Constraint_Error --
- ----------------------------
-
- procedure Raise_Constraint_Error (File : System.Address; Line : Integer) is
- begin
- Raise_With_Location_And_Msg (Constraint_Error_Def'Access, File, Line);
- end Raise_Constraint_Error;
-
- --------------------------------
- -- Raise_Constraint_Error_Msg --
- --------------------------------
-
- procedure Raise_Constraint_Error_Msg
- (File : System.Address;
- Line : Integer;
- Column : Integer;
- Msg : System.Address)
- is
- begin
- Raise_With_Location_And_Msg
- (Constraint_Error_Def'Access, File, Line, Column, Msg);
- end Raise_Constraint_Error_Msg;
-
- -------------------------
- -- Complete_Occurrence --
- -------------------------
-
- procedure Complete_Occurrence (X : EOA) is
- begin
- -- Compute the backtrace for this occurrence if the corresponding
- -- binder option has been set. Call_Chain takes care of the reraise
- -- case.
-
- -- ??? Using Call_Chain here means we are going to walk up the stack
- -- once only for backtracing purposes before doing it again for the
- -- propagation per se.
-
- -- The first inspection is much lighter, though, as it only requires
- -- partial unwinding of each frame. Additionally, although we could use
- -- the personality routine to record the addresses while propagating,
- -- this method has two drawbacks:
-
- -- 1) the trace is incomplete if the exception is handled since we
- -- don't walk past the frame with the handler,
-
- -- and
-
- -- 2) we would miss the frames for which our personality routine is not
- -- called, e.g. if C or C++ calls are on the way.
-
- Call_Chain (X);
-
- -- Notify the debugger
- Debug_Raise_Exception
- (E => SSL.Exception_Data_Ptr (X.Id),
- Message => X.Msg (1 .. X.Msg_Length));
- end Complete_Occurrence;
-
- ---------------------------------------
- -- Complete_And_Propagate_Occurrence --
- ---------------------------------------
-
- procedure Complete_And_Propagate_Occurrence (X : EOA) is
- begin
- Complete_Occurrence (X);
- Exception_Propagation.Propagate_Exception (X);
- end Complete_And_Propagate_Occurrence;
-
- ---------------------
- -- Raise_Exception --
- ---------------------
-
- procedure Raise_Exception
- (E : Exception_Id;
- Message : String := "")
- is
- EF : Exception_Id := E;
- begin
- -- Raise CE if E = Null_ID (AI-446)
-
- if E = null then
- EF := Constraint_Error'Identity;
- end if;
-
- -- Go ahead and raise appropriate exception
-
- Raise_Exception_Always (EF, Message);
- end Raise_Exception;
-
- ----------------------------
- -- Raise_Exception_Always --
- ----------------------------
-
- procedure Raise_Exception_Always
- (E : Exception_Id;
- Message : String := "")
- is
- X : constant EOA := Exception_Propagation.Allocate_Occurrence;
-
- begin
- Exception_Data.Set_Exception_Msg (X, E, Message);
-
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Complete_And_Propagate_Occurrence (X);
- end Raise_Exception_Always;
-
- ------------------------------
- -- Raise_Exception_No_Defer --
- ------------------------------
-
- procedure Raise_Exception_No_Defer
- (E : Exception_Id;
- Message : String := "")
- is
- X : constant EOA := Exception_Propagation.Allocate_Occurrence;
-
- begin
- Exception_Data.Set_Exception_Msg (X, E, Message);
-
- -- Do not call Abort_Defer.all, as specified by the spec
-
- Complete_And_Propagate_Occurrence (X);
- end Raise_Exception_No_Defer;
-
- -------------------------------------
- -- Raise_From_Controlled_Operation --
- -------------------------------------
-
- procedure Raise_From_Controlled_Operation
- (X : Ada.Exceptions.Exception_Occurrence)
- is
- Prefix : constant String := "adjust/finalize raised ";
- Orig_Msg : constant String := Exception_Message (X);
- Orig_Prefix_Length : constant Natural :=
- Integer'Min (Prefix'Length, Orig_Msg'Length);
-
- Orig_Prefix : String renames
- Orig_Msg (Orig_Msg'First .. Orig_Msg'First + Orig_Prefix_Length - 1);
-
- begin
- -- Message already has the proper prefix, just re-raise
-
- if Orig_Prefix = Prefix then
- Raise_Exception_No_Defer
- (E => Program_Error'Identity,
- Message => Orig_Msg);
-
- else
- declare
- New_Msg : constant String := Prefix & Exception_Name (X);
-
- begin
- -- No message present, just provide our own
-
- if Orig_Msg = "" then
- Raise_Exception_No_Defer
- (E => Program_Error'Identity,
- Message => New_Msg);
-
- -- Message present, add informational prefix
-
- else
- Raise_Exception_No_Defer
- (E => Program_Error'Identity,
- Message => New_Msg & ": " & Orig_Msg);
- end if;
- end;
- end if;
- end Raise_From_Controlled_Operation;
-
- -------------------------------------------
- -- Create_Occurrence_From_Signal_Handler --
- -------------------------------------------
-
- function Create_Occurrence_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address) return EOA
- is
- X : constant EOA := Exception_Propagation.Allocate_Occurrence;
-
- begin
- Exception_Data.Set_Exception_C_Msg (X, E, M);
-
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Complete_Occurrence (X);
- return X;
- end Create_Occurrence_From_Signal_Handler;
-
- ---------------------------------------------------
- -- Create_Machine_Occurrence_From_Signal_Handler --
- ---------------------------------------------------
-
- function Create_Machine_Occurrence_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address) return System.Address
- is
- begin
- return Create_Occurrence_From_Signal_Handler (E, M).Machine_Occurrence;
- end Create_Machine_Occurrence_From_Signal_Handler;
-
- -------------------------------
- -- Raise_From_Signal_Handler --
- -------------------------------
-
- procedure Raise_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address)
- is
- begin
- Exception_Propagation.Propagate_Exception
- (Create_Occurrence_From_Signal_Handler (E, M));
- end Raise_From_Signal_Handler;
-
- -------------------------
- -- Raise_Program_Error --
- -------------------------
-
- procedure Raise_Program_Error
- (File : System.Address;
- Line : Integer)
- is
- begin
- Raise_With_Location_And_Msg (Program_Error_Def'Access, File, Line);
- end Raise_Program_Error;
-
- -----------------------------
- -- Raise_Program_Error_Msg --
- -----------------------------
-
- procedure Raise_Program_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address)
- is
- begin
- Raise_With_Location_And_Msg
- (Program_Error_Def'Access, File, Line, M => Msg);
- end Raise_Program_Error_Msg;
-
- -------------------------
- -- Raise_Storage_Error --
- -------------------------
-
- procedure Raise_Storage_Error
- (File : System.Address;
- Line : Integer)
- is
- begin
- Raise_With_Location_And_Msg (Storage_Error_Def'Access, File, Line);
- end Raise_Storage_Error;
-
- -----------------------------
- -- Raise_Storage_Error_Msg --
- -----------------------------
-
- procedure Raise_Storage_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address)
- is
- begin
- Raise_With_Location_And_Msg
- (Storage_Error_Def'Access, File, Line, M => Msg);
- end Raise_Storage_Error_Msg;
-
- ---------------------------------
- -- Raise_With_Location_And_Msg --
- ---------------------------------
-
- procedure Raise_With_Location_And_Msg
- (E : Exception_Id;
- F : System.Address;
- L : Integer;
- C : Integer := 0;
- M : System.Address := System.Null_Address)
- is
- X : constant EOA := Exception_Propagation.Allocate_Occurrence;
- begin
- Exception_Data.Set_Exception_C_Msg (X, E, F, L, C, M);
-
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Complete_And_Propagate_Occurrence (X);
- end Raise_With_Location_And_Msg;
-
- --------------------
- -- Raise_With_Msg --
- --------------------
-
- procedure Raise_With_Msg (E : Exception_Id) is
- Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
- Ex : constant Exception_Occurrence_Access := Get_Current_Excep.all;
- begin
- Excep.Exception_Raised := False;
- Excep.Id := E;
- Excep.Num_Tracebacks := 0;
- Excep.Pid := Local_Partition_ID;
-
- -- Copy the message from the current exception
- -- Change the interface to be called with an occurrence ???
-
- Excep.Msg_Length := Ex.Msg_Length;
- Excep.Msg (1 .. Excep.Msg_Length) := Ex.Msg (1 .. Ex.Msg_Length);
-
- -- The following is a common pattern, should be abstracted
- -- into a procedure call ???
-
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Complete_And_Propagate_Occurrence (Excep);
- end Raise_With_Msg;
-
- -----------------------------------------
- -- Calls to Run-Time Check Subprograms --
- -----------------------------------------
-
- procedure Rcheck_CE_Access_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_00'Address);
- end Rcheck_CE_Access_Check;
-
- procedure Rcheck_CE_Null_Access_Parameter
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_01'Address);
- end Rcheck_CE_Null_Access_Parameter;
-
- procedure Rcheck_CE_Discriminant_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_02'Address);
- end Rcheck_CE_Discriminant_Check;
-
- procedure Rcheck_CE_Divide_By_Zero
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_03'Address);
- end Rcheck_CE_Divide_By_Zero;
-
- procedure Rcheck_CE_Explicit_Raise
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_04'Address);
- end Rcheck_CE_Explicit_Raise;
-
- procedure Rcheck_CE_Index_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_05'Address);
- end Rcheck_CE_Index_Check;
-
- procedure Rcheck_CE_Invalid_Data
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_06'Address);
- end Rcheck_CE_Invalid_Data;
-
- procedure Rcheck_CE_Length_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_07'Address);
- end Rcheck_CE_Length_Check;
-
- procedure Rcheck_CE_Null_Exception_Id
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_08'Address);
- end Rcheck_CE_Null_Exception_Id;
-
- procedure Rcheck_CE_Null_Not_Allowed
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_09'Address);
- end Rcheck_CE_Null_Not_Allowed;
-
- procedure Rcheck_CE_Overflow_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_10'Address);
- end Rcheck_CE_Overflow_Check;
-
- procedure Rcheck_CE_Partition_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_11'Address);
- end Rcheck_CE_Partition_Check;
-
- procedure Rcheck_CE_Range_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_12'Address);
- end Rcheck_CE_Range_Check;
-
- procedure Rcheck_CE_Tag_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_13'Address);
- end Rcheck_CE_Tag_Check;
-
- procedure Rcheck_PE_Access_Before_Elaboration
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_14'Address);
- end Rcheck_PE_Access_Before_Elaboration;
-
- procedure Rcheck_PE_Accessibility_Check
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_15'Address);
- end Rcheck_PE_Accessibility_Check;
-
- procedure Rcheck_PE_Address_Of_Intrinsic
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_16'Address);
- end Rcheck_PE_Address_Of_Intrinsic;
-
- procedure Rcheck_PE_Aliased_Parameters
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_17'Address);
- end Rcheck_PE_Aliased_Parameters;
-
- procedure Rcheck_PE_All_Guards_Closed
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_18'Address);
- end Rcheck_PE_All_Guards_Closed;
-
- procedure Rcheck_PE_Bad_Predicated_Generic_Type
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_19'Address);
- end Rcheck_PE_Bad_Predicated_Generic_Type;
-
- procedure Rcheck_PE_Current_Task_In_Entry_Body
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_20'Address);
- end Rcheck_PE_Current_Task_In_Entry_Body;
-
- procedure Rcheck_PE_Duplicated_Entry_Address
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_21'Address);
- end Rcheck_PE_Duplicated_Entry_Address;
-
- procedure Rcheck_PE_Explicit_Raise
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_22'Address);
- end Rcheck_PE_Explicit_Raise;
-
- procedure Rcheck_PE_Implicit_Return
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_24'Address);
- end Rcheck_PE_Implicit_Return;
-
- procedure Rcheck_PE_Misaligned_Address_Value
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_25'Address);
- end Rcheck_PE_Misaligned_Address_Value;
-
- procedure Rcheck_PE_Missing_Return
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_26'Address);
- end Rcheck_PE_Missing_Return;
-
- procedure Rcheck_PE_Non_Transportable_Actual
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_31'Address);
- end Rcheck_PE_Non_Transportable_Actual;
-
- procedure Rcheck_PE_Overlaid_Controlled_Object
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_27'Address);
- end Rcheck_PE_Overlaid_Controlled_Object;
-
- procedure Rcheck_PE_Potentially_Blocking_Operation
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_28'Address);
- end Rcheck_PE_Potentially_Blocking_Operation;
-
- procedure Rcheck_PE_Stream_Operation_Not_Allowed
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_36'Address);
- end Rcheck_PE_Stream_Operation_Not_Allowed;
-
- procedure Rcheck_PE_Stubbed_Subprogram_Called
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_29'Address);
- end Rcheck_PE_Stubbed_Subprogram_Called;
-
- procedure Rcheck_PE_Unchecked_Union_Restriction
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_30'Address);
- end Rcheck_PE_Unchecked_Union_Restriction;
-
- procedure Rcheck_SE_Empty_Storage_Pool
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Storage_Error_Msg (File, Line, Rmsg_32'Address);
- end Rcheck_SE_Empty_Storage_Pool;
-
- procedure Rcheck_SE_Explicit_Raise
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Storage_Error_Msg (File, Line, Rmsg_33'Address);
- end Rcheck_SE_Explicit_Raise;
-
- procedure Rcheck_SE_Infinite_Recursion
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Storage_Error_Msg (File, Line, Rmsg_34'Address);
- end Rcheck_SE_Infinite_Recursion;
-
- procedure Rcheck_SE_Object_Too_Large
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Storage_Error_Msg (File, Line, Rmsg_35'Address);
- end Rcheck_SE_Object_Too_Large;
-
- procedure Rcheck_CE_Access_Check_Ext
- (File : System.Address; Line, Column : Integer)
- is
- begin
- Raise_Constraint_Error_Msg (File, Line, Column, Rmsg_00'Address);
- end Rcheck_CE_Access_Check_Ext;
-
- procedure Rcheck_CE_Index_Check_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer)
- is
- Msg : constant String :=
- Rmsg_05 (Rmsg_05'First .. Rmsg_05'Last - 1) & ASCII.LF
- & "index " & Image (Index) & " not in " & Image (First)
- & ".." & Image (Last) & ASCII.NUL;
- begin
- Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
- end Rcheck_CE_Index_Check_Ext;
-
- procedure Rcheck_CE_Invalid_Data_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer)
- is
- Msg : constant String :=
- Rmsg_06 (Rmsg_06'First .. Rmsg_06'Last - 1) & ASCII.LF
- & "value " & Image (Index) & " not in " & Image (First)
- & ".." & Image (Last) & ASCII.NUL;
- begin
- Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
- end Rcheck_CE_Invalid_Data_Ext;
-
- procedure Rcheck_CE_Range_Check_Ext
- (File : System.Address; Line, Column, Index, First, Last : Integer)
- is
- Msg : constant String :=
- Rmsg_12 (Rmsg_12'First .. Rmsg_12'Last - 1) & ASCII.LF
- & "value " & Image (Index) & " not in " & Image (First)
- & ".." & Image (Last) & ASCII.NUL;
- begin
- Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
- end Rcheck_CE_Range_Check_Ext;
-
- procedure Rcheck_PE_Finalize_Raised_Exception
- (File : System.Address; Line : Integer)
- is
- X : constant EOA := Exception_Propagation.Allocate_Occurrence;
-
- begin
- -- This is "finalize/adjust raised exception". This subprogram is always
- -- called with abort deferred, unlike all other Rcheck_* subprograms, it
- -- needs to call Raise_Exception_No_Defer.
-
- -- This is consistent with Raise_From_Controlled_Operation
-
- Exception_Data.Set_Exception_C_Msg
- (X, Program_Error_Def'Access, File, Line, 0, Rmsg_23'Address);
- Complete_And_Propagate_Occurrence (X);
- end Rcheck_PE_Finalize_Raised_Exception;
-
- -------------
- -- Reraise --
- -------------
-
- procedure Reraise is
- Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
- Saved_MO : constant System.Address := Excep.Machine_Occurrence;
-
- begin
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Save_Occurrence (Excep.all, Get_Current_Excep.all.all);
- Excep.Machine_Occurrence := Saved_MO;
- Complete_And_Propagate_Occurrence (Excep);
- end Reraise;
-
- --------------------------------------
- -- Reraise_Library_Exception_If_Any --
- --------------------------------------
-
- procedure Reraise_Library_Exception_If_Any is
- LE : Exception_Occurrence;
-
- begin
- if Library_Exception_Set then
- LE := Library_Exception;
-
- if LE.Id = Null_Id then
- Raise_Exception_No_Defer
- (E => Program_Error'Identity,
- Message => "finalize/adjust raised exception");
- else
- Raise_From_Controlled_Operation (LE);
- end if;
- end if;
- end Reraise_Library_Exception_If_Any;
-
- ------------------------
- -- Reraise_Occurrence --
- ------------------------
-
- procedure Reraise_Occurrence (X : Exception_Occurrence) is
- begin
- if X.Id = null then
- return;
- else
- Reraise_Occurrence_Always (X);
- end if;
- end Reraise_Occurrence;
-
- -------------------------------
- -- Reraise_Occurrence_Always --
- -------------------------------
-
- procedure Reraise_Occurrence_Always (X : Exception_Occurrence) is
- begin
- if not ZCX_By_Default then
- Abort_Defer.all;
- end if;
-
- Reraise_Occurrence_No_Defer (X);
- end Reraise_Occurrence_Always;
-
- ---------------------------------
- -- Reraise_Occurrence_No_Defer --
- ---------------------------------
-
- procedure Reraise_Occurrence_No_Defer (X : Exception_Occurrence) is
- Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
- Saved_MO : constant System.Address := Excep.Machine_Occurrence;
- begin
- Save_Occurrence (Excep.all, X);
- Excep.Machine_Occurrence := Saved_MO;
- Complete_And_Propagate_Occurrence (Excep);
- end Reraise_Occurrence_No_Defer;
-
- ---------------------
- -- Save_Occurrence --
- ---------------------
-
- procedure Save_Occurrence
- (Target : out Exception_Occurrence;
- Source : Exception_Occurrence)
- is
- begin
- -- As the machine occurrence might be a data that must be finalized
- -- (outside any Ada mechanism), do not copy it
-
- Target.Id := Source.Id;
- Target.Machine_Occurrence := System.Null_Address;
- Target.Msg_Length := Source.Msg_Length;
- Target.Num_Tracebacks := Source.Num_Tracebacks;
- Target.Pid := Source.Pid;
-
- Target.Msg (1 .. Target.Msg_Length) :=
- Source.Msg (1 .. Target.Msg_Length);
-
- Target.Tracebacks (1 .. Target.Num_Tracebacks) :=
- Source.Tracebacks (1 .. Target.Num_Tracebacks);
- end Save_Occurrence;
-
- function Save_Occurrence (Source : Exception_Occurrence) return EOA is
- Target : constant EOA := new Exception_Occurrence;
- begin
- Save_Occurrence (Target.all, Source);
- return Target;
- end Save_Occurrence;
-
- -------------------
- -- String_To_EId --
- -------------------
-
- function String_To_EId (S : String) return Exception_Id
- renames Stream_Attributes.String_To_EId;
-
- ------------------
- -- String_To_EO --
- ------------------
-
- function String_To_EO (S : String) return Exception_Occurrence
- renames Stream_Attributes.String_To_EO;
-
- ---------------
- -- To_Stderr --
- ---------------
-
- procedure To_Stderr (C : Character) is
- procedure Put_Char_Stderr (C : Character);
- pragma Import (C, Put_Char_Stderr, "put_char_stderr");
- begin
- Put_Char_Stderr (C);
- end To_Stderr;
-
- procedure To_Stderr (S : String) is
- begin
- for J in S'Range loop
- if S (J) /= ASCII.CR then
- To_Stderr (S (J));
- end if;
- end loop;
- end To_Stderr;
-
- -------------------------
- -- Transfer_Occurrence --
- -------------------------
-
- procedure Transfer_Occurrence
- (Target : Exception_Occurrence_Access;
- Source : Exception_Occurrence)
- is
- begin
- Save_Occurrence (Target.all, Source);
- end Transfer_Occurrence;
-
- ------------------------
- -- Triggered_By_Abort --
- ------------------------
-
- function Triggered_By_Abort return Boolean is
- Ex : constant Exception_Occurrence_Access := Get_Current_Excep.all;
- begin
- return Ex /= null
- and then Exception_Identity (Ex.all) = Standard'Abort_Signal'Identity;
- end Triggered_By_Abort;
-
- -------------------------
- -- Wide_Exception_Name --
- -------------------------
-
- WC_Encoding : Character;
- pragma Import (C, WC_Encoding, "__gl_wc_encoding");
- -- Encoding method for source, as exported by binder
-
- function Wide_Exception_Name
- (Id : Exception_Id) return Wide_String
- is
- S : constant String := Exception_Name (Id);
- W : Wide_String (1 .. S'Length);
- L : Natural;
- begin
- String_To_Wide_String
- (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
- return W (1 .. L);
- end Wide_Exception_Name;
-
- function Wide_Exception_Name
- (X : Exception_Occurrence) return Wide_String
- is
- S : constant String := Exception_Name (X);
- W : Wide_String (1 .. S'Length);
- L : Natural;
- begin
- String_To_Wide_String
- (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
- return W (1 .. L);
- end Wide_Exception_Name;
-
- ----------------------------
- -- Wide_Wide_Exception_Name --
- -----------------------------
-
- function Wide_Wide_Exception_Name
- (Id : Exception_Id) return Wide_Wide_String
- is
- S : constant String := Exception_Name (Id);
- W : Wide_Wide_String (1 .. S'Length);
- L : Natural;
- begin
- String_To_Wide_Wide_String
- (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
- return W (1 .. L);
- end Wide_Wide_Exception_Name;
-
- function Wide_Wide_Exception_Name
- (X : Exception_Occurrence) return Wide_Wide_String
- is
- S : constant String := Exception_Name (X);
- W : Wide_Wide_String (1 .. S'Length);
- L : Natural;
- begin
- String_To_Wide_Wide_String
- (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
- return W (1 .. L);
- end Wide_Wide_Exception_Name;
-
- --------------------------
- -- Code_Address_For_ZZZ --
- --------------------------
-
- -- This function gives us the end of the PC range for addresses
- -- within the exception unit itself. We hope that gigi/gcc keeps all the
- -- procedures in their original order.
-
- function Code_Address_For_ZZZ return System.Address is
- begin
- <<Start_Of_ZZZ>>
- return Start_Of_ZZZ'Address;
- end Code_Address_For_ZZZ;
-
-end Ada.Exceptions;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT RUN-TIME COMPONENTS --
--- --
--- A D A . E X C E P T I O N S --
--- --
--- S p e c --
--- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
--- --
--- This specification is derived from the Ada Reference Manual for use with --
--- GNAT. The copyright notice above, and the license provisions that follow --
--- apply solely to the contents of the part following the private keyword. --
--- --
--- 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. --
--- --
--- As a special exception under Section 7 of GPL version 3, you are granted --
--- additional permissions described in the GCC Runtime Library Exception, --
--- version 3.1, as published by the Free Software Foundation. --
--- --
--- You should have received a copy of the GNU General Public License and --
--- a copy of the GCC Runtime Library Exception along with this program; --
--- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
--- <http://www.gnu.org/licenses/>. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This version of Ada.Exceptions fully supports Ada 95 and later language
--- versions. It is used in all situations except for the build of the
--- compiler and other basic tools. For these latter builds, we use an
--- Ada 95-only version.
-
--- The reason for this splitting off of a separate version is to support
--- older bootstrap compilers that do not support Ada 2005 features, and
--- Ada.Exceptions is part of the compiler sources.
-
-pragma Polling (Off);
--- We must turn polling off for this unit, because otherwise we get
--- elaboration circularities with ourself.
-
-with System;
-with System.Parameters;
-with System.Standard_Library;
-with System.Traceback_Entries;
-
-package Ada.Exceptions is
- pragma Preelaborate;
- -- In accordance with Ada 2005 AI-362.
-
- type Exception_Id is private;
- pragma Preelaborable_Initialization (Exception_Id);
-
- Null_Id : constant Exception_Id;
-
- type Exception_Occurrence is limited private;
- pragma Preelaborable_Initialization (Exception_Occurrence);
-
- type Exception_Occurrence_Access is access all Exception_Occurrence;
-
- Null_Occurrence : constant Exception_Occurrence;
-
- function Exception_Name (Id : Exception_Id) return String;
-
- function Exception_Name (X : Exception_Occurrence) return String;
-
- function Wide_Exception_Name
- (Id : Exception_Id) return Wide_String;
- pragma Ada_05 (Wide_Exception_Name);
-
- function Wide_Exception_Name
- (X : Exception_Occurrence) return Wide_String;
- pragma Ada_05 (Wide_Exception_Name);
-
- function Wide_Wide_Exception_Name
- (Id : Exception_Id) return Wide_Wide_String;
- pragma Ada_05 (Wide_Wide_Exception_Name);
-
- function Wide_Wide_Exception_Name
- (X : Exception_Occurrence) return Wide_Wide_String;
- pragma Ada_05 (Wide_Wide_Exception_Name);
-
- procedure Raise_Exception (E : Exception_Id; Message : String := "");
- pragma No_Return (Raise_Exception);
- -- Note: In accordance with AI-466, CE is raised if E = Null_Id
-
- function Exception_Message (X : Exception_Occurrence) return String;
-
- procedure Reraise_Occurrence (X : Exception_Occurrence);
- -- Note: it would be really nice to give a pragma No_Return for this
- -- procedure, but it would be wrong, since Reraise_Occurrence does return
- -- if the argument is the null exception occurrence. See also procedure
- -- Reraise_Occurrence_Always in the private part of this package.
-
- function Exception_Identity (X : Exception_Occurrence) return Exception_Id;
-
- function Exception_Information (X : Exception_Occurrence) return String;
- -- The format of the exception information is as follows:
- --
- -- exception name (as in Exception_Name)
- -- message (or a null line if no message)
- -- PID=nnnn
- -- 0xyyyyyyyy 0xyyyyyyyy ...
- --
- -- The lines are separated by a ASCII.LF character
- --
- -- The nnnn is the partition Id given as decimal digits
- --
- -- The 0x... line represents traceback program counter locations,
- -- in order with the first one being the exception location.
-
- -- Note on ordering: the compiler uses the Save_Occurrence procedure, but
- -- not the function from Rtsfind, so it is important that the procedure
- -- come first, since Rtsfind finds the first matching entity.
-
- procedure Save_Occurrence
- (Target : out Exception_Occurrence;
- Source : Exception_Occurrence);
-
- function Save_Occurrence
- (Source : Exception_Occurrence)
- return Exception_Occurrence_Access;
-
- -- Ada 2005 (AI-438): The language revision introduces the following
- -- subprograms and attribute definitions. We do not provide them
- -- explicitly. instead, the corresponding stream attributes are made
- -- available through a pragma Stream_Convert in the private part.
-
- -- procedure Read_Exception_Occurrence
- -- (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
- -- Item : out Exception_Occurrence);
-
- -- procedure Write_Exception_Occurrence
- -- (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
- -- Item : Exception_Occurrence);
-
- -- for Exception_Occurrence'Read use Read_Exception_Occurrence;
- -- for Exception_Occurrence'Write use Write_Exception_Occurrence;
-
-private
- package SSL renames System.Standard_Library;
- package SP renames System.Parameters;
-
- subtype EOA is Exception_Occurrence_Access;
-
- Exception_Msg_Max_Length : constant := SP.Default_Exception_Msg_Max_Length;
-
- ------------------
- -- Exception_Id --
- ------------------
-
- subtype Code_Loc is System.Address;
- -- Code location used in building exception tables and for call addresses
- -- when propagating an exception. Values of this type are created by using
- -- Label'Address or extracted from machine states using Get_Code_Loc.
-
- Null_Loc : constant Code_Loc := System.Null_Address;
- -- Null code location, used to flag outer level frame
-
- type Exception_Id is new SSL.Exception_Data_Ptr;
-
- function EId_To_String (X : Exception_Id) return String;
- function String_To_EId (S : String) return Exception_Id;
- pragma Stream_Convert (Exception_Id, String_To_EId, EId_To_String);
- -- Functions for implementing Exception_Id stream attributes
-
- Null_Id : constant Exception_Id := null;
-
- -------------------------
- -- Private Subprograms --
- -------------------------
-
- function Exception_Name_Simple (X : Exception_Occurrence) return String;
- -- Like Exception_Name, but returns the simple non-qualified name of the
- -- exception. This is used to implement the Exception_Name function in
- -- Current_Exceptions (the DEC compatible unit). It is called from the
- -- compiler generated code (using Rtsfind, which does not respect the
- -- private barrier, so we can place this function in the private part
- -- where the compiler can find it, but the spec is unchanged.)
-
- procedure Raise_Exception_Always (E : Exception_Id; Message : String := "");
- pragma No_Return (Raise_Exception_Always);
- pragma Export (Ada, Raise_Exception_Always, "__gnat_raise_exception");
- -- This differs from Raise_Exception only in that the caller has determined
- -- that for sure the parameter E is not null, and that therefore no check
- -- for Null_Id is required. The expander converts Raise_Exception calls to
- -- Raise_Exception_Always if it can determine this is the case. The Export
- -- allows this routine to be accessed from Pure units.
-
- procedure Raise_From_Signal_Handler
- (E : Exception_Id;
- M : System.Address);
- pragma Export
- (Ada, Raise_From_Signal_Handler,
- "ada__exceptions__raise_from_signal_handler");
- pragma No_Return (Raise_From_Signal_Handler);
- -- This routine is used to raise an exception from a signal handler. The
- -- signal handler has already stored the machine state (i.e. the state that
- -- corresponds to the location at which the signal was raised). E is the
- -- Exception_Id specifying what exception is being raised, and M is a
- -- pointer to a null-terminated string which is the message to be raised.
- -- Note that this routine never returns, so it is permissible to simply
- -- jump to this routine, rather than call it. This may be appropriate for
- -- systems where the right way to get out of signal handler is to alter the
- -- PC value in the machine state or in some other way ask the operating
- -- system to return here rather than to the original location.
-
- procedure Raise_From_Controlled_Operation
- (X : Ada.Exceptions.Exception_Occurrence);
- pragma No_Return (Raise_From_Controlled_Operation);
- pragma Export
- (Ada, Raise_From_Controlled_Operation,
- "__gnat_raise_from_controlled_operation");
- -- Raise Program_Error, providing information about X (an exception raised
- -- during a controlled operation) in the exception message.
-
- procedure Reraise_Library_Exception_If_Any;
- pragma Export
- (Ada, Reraise_Library_Exception_If_Any,
- "__gnat_reraise_library_exception_if_any");
- -- If there was an exception raised during library-level finalization,
- -- reraise the exception.
-
- procedure Reraise_Occurrence_Always (X : Exception_Occurrence);
- pragma No_Return (Reraise_Occurrence_Always);
- -- This differs from Raise_Occurrence only in that the caller guarantees
- -- that for sure the parameter X is not the null occurrence, and that
- -- therefore this procedure cannot return. The expander uses this routine
- -- in the translation of a raise statement with no parameter (reraise).
-
- procedure Reraise_Occurrence_No_Defer (X : Exception_Occurrence);
- pragma No_Return (Reraise_Occurrence_No_Defer);
- -- Exactly like Reraise_Occurrence, except that abort is not deferred
- -- before the call and the parameter X is known not to be the null
- -- occurrence. This is used in generated code when it is known that abort
- -- is already deferred.
-
- function Triggered_By_Abort return Boolean;
- -- Determine whether the current exception (if it exists) is an instance of
- -- Standard'Abort_Signal.
-
- -----------------------
- -- Polling Interface --
- -----------------------
-
- -- The GNAT compiler has an option to generate polling calls to the Poll
- -- routine in this package. Specifying the -gnatP option for a compilation
- -- causes a call to Ada.Exceptions.Poll to be generated on every subprogram
- -- entry and on every iteration of a loop, thus avoiding the possibility of
- -- a case of unbounded time between calls.
-
- -- This polling interface may be used for instrumentation or debugging
- -- purposes (e.g. implementing watchpoints in software or in the debugger).
-
- -- In the GNAT technology itself, this interface is used to implement
- -- immediate asynchronous transfer of control and immediate abort on
- -- targets which do not provide for one thread interrupting another.
-
- -- Note: this used to be in a separate unit called System.Poll, but that
- -- caused horrible circular elaboration problems between System.Poll and
- -- Ada.Exceptions.
-
- procedure Poll;
- -- Check for asynchronous abort. Note that we do not inline the body.
- -- This makes the interface more useful for debugging purposes.
-
- --------------------------
- -- Exception_Occurrence --
- --------------------------
-
- package TBE renames System.Traceback_Entries;
-
- Max_Tracebacks : constant := 50;
- -- Maximum number of trace backs stored in exception occurrence
-
- subtype Tracebacks_Array is TBE.Tracebacks_Array (1 .. Max_Tracebacks);
- -- Traceback array stored in exception occurrence
-
- type Exception_Occurrence is record
- Id : Exception_Id;
- -- Exception_Identity for this exception occurrence
-
- Machine_Occurrence : System.Address;
- -- The underlying machine occurrence. For GCC, this corresponds to the
- -- _Unwind_Exception structure address.
-
- Msg_Length : Natural := 0;
- -- Length of message (zero = no message)
-
- Msg : String (1 .. Exception_Msg_Max_Length);
- -- Characters of message
-
- Exception_Raised : Boolean := False;
- -- Set to true to indicate that this exception occurrence has actually
- -- been raised. When an exception occurrence is first created, this is
- -- set to False, then when it is processed by Raise_Current_Exception,
- -- it is set to True. If Raise_Current_Exception is used to raise an
- -- exception for which this flag is already True, then it knows that
- -- it is dealing with the reraise case (which is useful to distinguish
- -- for exception tracing purposes).
-
- Pid : Natural := 0;
- -- Partition_Id for partition raising exception
-
- Num_Tracebacks : Natural range 0 .. Max_Tracebacks := 0;
- -- Number of traceback entries stored
-
- Tracebacks : Tracebacks_Array;
- -- Stored tracebacks (in Tracebacks (1 .. Num_Tracebacks))
- end record;
-
- function "=" (Left, Right : Exception_Occurrence) return Boolean
- is abstract;
- -- Don't allow comparison on exception occurrences, we should not need
- -- this, and it would not work right, because of the Msg and Tracebacks
- -- fields which have unused entries not copied by Save_Occurrence.
-
- function Get_Exception_Machine_Occurrence
- (X : Exception_Occurrence) return System.Address;
- pragma Export (Ada, Get_Exception_Machine_Occurrence,
- "__gnat_get_exception_machine_occurrence");
- -- Get the machine occurrence corresponding to an exception occurrence.
- -- It is Null_Address if there is no machine occurrence (in runtimes that
- -- doesn't use GCC mechanism) or if it has been lost (Save_Occurrence
- -- doesn't save the machine occurrence).
-
- function EO_To_String (X : Exception_Occurrence) return String;
- function String_To_EO (S : String) return Exception_Occurrence;
- pragma Stream_Convert (Exception_Occurrence, String_To_EO, EO_To_String);
- -- Functions for implementing Exception_Occurrence stream attributes
-
- Null_Occurrence : constant Exception_Occurrence := (
- Id => null,
- Machine_Occurrence => System.Null_Address,
- Msg_Length => 0,
- Msg => (others => ' '),
- Exception_Raised => False,
- Pid => 0,
- Num_Tracebacks => 0,
- Tracebacks => (others => TBE.Null_TB_Entry));
-
-end Ada.Exceptions;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, 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- --
-- --
------------------------------------------------------------------------------
-pragma Compiler_Unit_Warning;
-
pragma Style_Checks (All_Checks);
-- No subprogram ordering check, due to logical grouping
-- elaboration circularities with System.Exception_Tables.
with System; use System;
+with System.Exceptions; use System.Exceptions;
with System.Exceptions_Debug; use System.Exceptions_Debug;
with System.Standard_Library; use System.Standard_Library;
with System.Soft_Links; use System.Soft_Links;
+with System.WCh_Con; use System.WCh_Con;
+with System.WCh_StW; use System.WCh_StW;
+
+pragma Warnings (Off);
+-- Suppress complaints about Symbolic not being referenced, and about it not
+-- having pragma Preelaborate.
+with System.Traceback.Symbolic;
+-- Bring Symbolic into the closure. If it is the s-trasym-dwarf.adb version,
+-- it will install symbolic tracebacks as the default decorator. Otherwise,
+-- symbolic tracebacks are not supported, and we fall back to hexadecimal
+-- addresses.
+pragma Warnings (On);
package body Ada.Exceptions is
pragma Suppress (All_Checks);
- -- We definitely do not want exceptions occurring within this unit, or we
- -- are in big trouble. If an exceptional situation does occur, better that
- -- it not be raised, since raising it can cause confusing chaos.
+ -- We definitely do not want exceptions occurring within this unit, or
+ -- we are in big trouble. If an exceptional situation does occur, better
+ -- that it not be raised, since raising it can cause confusing chaos.
-----------------------
-- Local Subprograms --
-- from C clients using the given external name, even though they are not
-- technically visible in the Ada sense.
- procedure Process_Raise_Exception (E : Exception_Id);
- pragma No_Return (Process_Raise_Exception);
- -- This is the lowest level raise routine. It raises the exception
- -- referenced by Current_Excep.all in the TSD, without deferring abort
- -- (the caller must ensure that abort is deferred on entry).
+ function Code_Address_For_AAA return System.Address;
+ function Code_Address_For_ZZZ return System.Address;
+ -- Return start and end of procedures in this package
+ --
+ -- These procedures are used to provide exclusion bounds in
+ -- calls to Call_Chain at exception raise points from this unit. The
+ -- purpose is to arrange for the exception tracebacks not to include
+ -- frames from subprograms involved in the raise process, as these are
+ -- meaningless from the user's standpoint.
+ --
+ -- For these bounds to be meaningful, we need to ensure that the object
+ -- code for the subprograms involved in processing a raise is located
+ -- after the object code Code_Address_For_AAA and before the object
+ -- code Code_Address_For_ZZZ. This will indeed be the case as long as
+ -- the following rules are respected:
+ --
+ -- 1) The bodies of the subprograms involved in processing a raise
+ -- are located after the body of Code_Address_For_AAA and before the
+ -- body of Code_Address_For_ZZZ.
+ --
+ -- 2) No pragma Inline applies to any of these subprograms, as this
+ -- could delay the corresponding assembly output until the end of
+ -- the unit.
+
+ procedure Call_Chain (Excep : EOA);
+ -- Store up to Max_Tracebacks in Excep, corresponding to the current
+ -- call chain.
+
+ function Image (Index : Integer) return String;
+ -- Return string image corresponding to Index
procedure To_Stderr (S : String);
pragma Export (Ada, To_Stderr, "__gnat_to_stderr");
- -- Little routine to output string to stderr that is also used in the
- -- tasking run time.
+ -- Little routine to output string to stderr that is also used
+ -- in the tasking run time.
procedure To_Stderr (C : Character);
pragma Inline (To_Stderr);
pragma Export (Ada, To_Stderr, "__gnat_to_stderr_char");
- -- Little routine to output a character to stderr, used by some of the
- -- separate units below.
+ -- Little routine to output a character to stderr, used by some of
+ -- the separate units below.
package Exception_Data is
Line : Integer := 0;
Column : Integer := 0;
Msg2 : System.Address := System.Null_Address);
- -- This routine is called to setup the exception referenced by the
- -- Current_Excep field in the TSD to contain the indicated Id value
- -- and message. Msg1 is a null terminated string which is generated
- -- as the exception message. If line is non-zero, then a colon and
- -- the decimal representation of this integer is appended to the
- -- message. Ditto for Column. When Msg2 is non-null, a space and this
- -- additional null terminated string is added to the message.
+ -- This routine is called to setup the exception referenced by X
+ -- to contain the indicated Id value and message. Msg1 is a null
+ -- terminated string which is generated as the exception message. If
+ -- line is non-zero, then a colon and the decimal representation of
+ -- this integer is appended to the message. Ditto for Column. When Msg2
+ -- is non-null, a space and this additional null terminated string is
+ -- added to the message.
procedure Set_Exception_Msg
(Excep : EOA;
Id : Exception_Id;
Message : String);
- -- This routine is called to setup the exception referenced by the
- -- Current_Excep field in the TSD to contain the indicated Id value and
- -- message. Message is a string which is generated as the exception
- -- message.
+ -- This routine is called to setup the exception referenced by X
+ -- to contain the indicated Id value and message. Message is a string
+ -- which is generated as the exception message.
---------------------------------------
-- Exception Information Subprograms --
procedure Unhandled_Exception_Terminate (Excep : EOA);
pragma No_Return (Unhandled_Exception_Terminate);
- -- This procedure is called to terminate program execution following an
- -- unhandled exception. The exception information, including traceback
- -- if available is output, and execution is then terminated. Note that
- -- at the point where this routine is called, the stack has typically
- -- been destroyed.
+ -- This procedure is called to terminate execution following an
+ -- unhandled exception. The exception information, including
+ -- traceback if available is output, and execution is then
+ -- terminated. Note that at the point where this routine is
+ -- called, the stack has typically been destroyed.
end Exception_Traces;
+ package Exception_Propagation is
+
+ ---------------------------------------
+ -- Exception Propagation Subprograms --
+ ---------------------------------------
+
+ function Allocate_Occurrence return EOA;
+ -- Allocate an exception occurrence (as well as the machine occurrence)
+
+ procedure Propagate_Exception (Excep : EOA);
+ pragma No_Return (Propagate_Exception);
+ -- This procedure propagates the exception represented by Excep
+
+ end Exception_Propagation;
+
package Stream_Attributes is
----------------------------------
end Stream_Attributes;
- procedure Raise_Current_Excep (E : Exception_Id);
- pragma No_Return (Raise_Current_Excep);
- pragma Export (C, Raise_Current_Excep, "__gnat_raise_nodefer_with_msg");
- -- This is a simple wrapper to Process_Raise_Exception.
- --
- -- This external name for Raise_Current_Excep is historical, and probably
- -- should be changed but for now we keep it, because gdb and gigi know
- -- about it.
+ procedure Complete_Occurrence (X : EOA);
+ -- Finish building the occurrence: save the call chain and notify the
+ -- debugger.
+
+ procedure Complete_And_Propagate_Occurrence (X : EOA);
+ pragma No_Return (Complete_And_Propagate_Occurrence);
+ -- This is a simple wrapper to Complete_Occurrence and
+ -- Exception_Propagation.Propagate_Exception.
+
+ function Create_Occurrence_From_Signal_Handler
+ (E : Exception_Id;
+ M : System.Address) return EOA;
+ -- Create and build an exception occurrence using exception id E and
+ -- nul-terminated message M.
+
+ function Create_Machine_Occurrence_From_Signal_Handler
+ (E : Exception_Id;
+ M : System.Address) return System.Address;
+ pragma Export (C, Create_Machine_Occurrence_From_Signal_Handler,
+ "__gnat_create_machine_occurrence_from_signal_handler");
+ -- Create and build an exception occurrence using exception id E and
+ -- nul-terminated message M. Return the machine occurrence.
procedure Raise_Exception_No_Defer
- (E : Exception_Id;
- Message : String := "");
+ (E : Exception_Id;
+ Message : String := "");
pragma Export
(Ada, Raise_Exception_No_Defer,
"ada__exceptions__raise_exception_no_defer");
procedure Raise_With_Msg (E : Exception_Id);
pragma No_Return (Raise_With_Msg);
pragma Export (C, Raise_With_Msg, "__gnat_raise_with_msg");
- -- Raises an exception with given exception id value. A message is
- -- associated with the raise, and has already been stored in the exception
- -- occurrence referenced by the Current_Excep in the TSD. Abort is deferred
- -- before the raise call.
+ -- Raises an exception with given exception id value. A message
+ -- is associated with the raise, and has already been stored in the
+ -- exception occurrence referenced by the Current_Excep in the TSD.
+ -- Abort is deferred before the raise call.
procedure Raise_With_Location_And_Msg
(E : Exception_Id;
F : System.Address;
L : Integer;
+ C : Integer := 0;
M : System.Address := System.Null_Address);
pragma No_Return (Raise_With_Location_And_Msg);
-- Raise an exception with given exception id value. A filename and line
-- number is associated with the raise and is stored in the exception
- -- occurrence and in addition a string message M is appended to this
- -- if M is not null.
+ -- occurrence and in addition a column and a string message M may be
+ -- appended to this (if not null/0).
- procedure Raise_Constraint_Error
- (File : System.Address;
- Line : Integer);
+ procedure Raise_Constraint_Error (File : System.Address; Line : Integer);
pragma No_Return (Raise_Constraint_Error);
- pragma Export
- (C, Raise_Constraint_Error, "__gnat_raise_constraint_error");
+ pragma Export (C, Raise_Constraint_Error, "__gnat_raise_constraint_error");
-- Raise constraint error with file:line information
procedure Raise_Constraint_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address);
+ (File : System.Address;
+ Line : Integer;
+ Column : Integer;
+ Msg : System.Address);
pragma No_Return (Raise_Constraint_Error_Msg);
pragma Export
(C, Raise_Constraint_Error_Msg, "__gnat_raise_constraint_error_msg");
- -- Raise constraint error with file:line + msg information
+ -- Raise constraint error with file:line:col + msg information
- procedure Raise_Program_Error
- (File : System.Address;
- Line : Integer);
+ procedure Raise_Program_Error (File : System.Address; Line : Integer);
pragma No_Return (Raise_Program_Error);
- pragma Export
- (C, Raise_Program_Error, "__gnat_raise_program_error");
+ pragma Export (C, Raise_Program_Error, "__gnat_raise_program_error");
-- Raise program error with file:line information
procedure Raise_Program_Error_Msg
(C, Raise_Program_Error_Msg, "__gnat_raise_program_error_msg");
-- Raise program error with file:line + msg information
- procedure Raise_Storage_Error
- (File : System.Address;
- Line : Integer);
+ procedure Raise_Storage_Error (File : System.Address; Line : Integer);
pragma No_Return (Raise_Storage_Error);
- pragma Export
- (C, Raise_Storage_Error, "__gnat_raise_storage_error");
+ pragma Export (C, Raise_Storage_Error, "__gnat_raise_storage_error");
-- Raise storage error with file:line information
procedure Raise_Storage_Error_Msg
-- graph below illustrates the relations between the Raise_ subprograms
-- and identifies the points where basic flags such as Exception_Raised
-- are initialized.
- --
+
-- (i) signs indicate the flags initialization points. R stands for Raise,
-- W for With, and E for Exception.
- --
+
-- R_No_Msg R_E R_Pe R_Ce R_Se
-- | | | | |
-- +--+ +--+ +---+ | +---+
-- | | | |
-- | | | Set_E_C_Msg(i)
-- | | |
- -- Raise_Current_Excep
+ -- Complete_And_Propagate_Occurrence
procedure Reraise;
pragma No_Return (Reraise);
pragma Export (C, Reraise, "__gnat_reraise");
- -- Reraises the exception referenced by the Current_Excep field of the TSD
- -- (all fields of this exception occurrence are set). Abort is deferred
- -- before the reraise operation.
+ -- Reraises the exception referenced by the Current_Excep field
+ -- of the TSD (all fields of this exception occurrence are set).
+ -- Abort is deferred before the reraise operation. Called from
+ -- System.Tasking.RendezVous.Exceptional_Complete_RendezVous
procedure Transfer_Occurrence
(Target : Exception_Occurrence_Access;
Source : Exception_Occurrence);
pragma Export (C, Transfer_Occurrence, "__gnat_transfer_occurrence");
- -- Called from System.Tasking.RendezVous.Exceptional_Complete_RendezVous
- -- to setup Target from Source as an exception to be propagated in the
- -- caller task. Target is expected to be a pointer to the fixed TSD
- -- occurrence for this task.
+ -- Called from s-tasren.adb:Local_Complete_RendezVous and
+ -- s-tpobop.adb:Exceptional_Complete_Entry_Body to setup Target from
+ -- Source as an exception to be propagated in the caller task. Target is
+ -- expected to be a pointer to the fixed TSD occurrence for this task.
--------------------------------
-- Run-Time Check Subprograms --
-- attached. The parameters are the file name and line number in each
-- case. The names are defined by Exp_Ch11.Get_RT_Exception_Name.
- -- Note on ordering of these subprograms. Normally in the Ada.Exceptions
- -- units we do not care about the ordering of entries for Rcheck
- -- subprograms, and the normal approach is to keep them in the same
- -- order as declarations in Types.
-
- -- This section is an IMPORTANT EXCEPTION. It is required by the .Net
- -- runtime that the routine Rcheck_PE_Finalize_Raise_Exception is at the
- -- end of the list (for reasons that are documented in the exceptmsg.awk
- -- script which takes care of generating the required exception data).
-
- procedure Rcheck_CE_Access_Check -- 00
+ procedure Rcheck_CE_Access_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Access_Parameter -- 01
+ procedure Rcheck_CE_Null_Access_Parameter
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Discriminant_Check -- 02
+ procedure Rcheck_CE_Discriminant_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Divide_By_Zero -- 03
+ procedure Rcheck_CE_Divide_By_Zero
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Explicit_Raise -- 04
+ procedure Rcheck_CE_Explicit_Raise
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Index_Check -- 05
+ procedure Rcheck_CE_Index_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Invalid_Data -- 06
+ procedure Rcheck_CE_Invalid_Data
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Length_Check -- 07
+ procedure Rcheck_CE_Length_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Exception_Id -- 08
+ procedure Rcheck_CE_Null_Exception_Id
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Null_Not_Allowed -- 09
+ procedure Rcheck_CE_Null_Not_Allowed
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Overflow_Check -- 10
+ procedure Rcheck_CE_Overflow_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Partition_Check -- 11
+ procedure Rcheck_CE_Partition_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Range_Check -- 12
+ procedure Rcheck_CE_Range_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_CE_Tag_Check -- 13
+ procedure Rcheck_CE_Tag_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Access_Before_Elaboration -- 14
+ procedure Rcheck_PE_Access_Before_Elaboration
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Accessibility_Check -- 15
+ procedure Rcheck_PE_Accessibility_Check
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Address_Of_Intrinsic -- 16
+ procedure Rcheck_PE_Address_Of_Intrinsic
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Aliased_Parameters -- 17
+ procedure Rcheck_PE_Aliased_Parameters
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_All_Guards_Closed -- 18
+ procedure Rcheck_PE_All_Guards_Closed
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Bad_Predicated_Generic_Type -- 19
+ procedure Rcheck_PE_Bad_Predicated_Generic_Type
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Current_Task_In_Entry_Body -- 20
+ procedure Rcheck_PE_Current_Task_In_Entry_Body
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Duplicated_Entry_Address -- 21
+ procedure Rcheck_PE_Duplicated_Entry_Address
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Explicit_Raise -- 22
+ procedure Rcheck_PE_Explicit_Raise
(File : System.Address; Line : Integer);
-
- procedure Rcheck_PE_Implicit_Return -- 24
+ procedure Rcheck_PE_Implicit_Return
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Misaligned_Address_Value -- 25
+ procedure Rcheck_PE_Misaligned_Address_Value
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Missing_Return -- 26
+ procedure Rcheck_PE_Missing_Return
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Overlaid_Controlled_Object -- 27
+ procedure Rcheck_PE_Non_Transportable_Actual
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Potentially_Blocking_Operation -- 28
+ procedure Rcheck_PE_Overlaid_Controlled_Object
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Stubbed_Subprogram_Called -- 29
+ procedure Rcheck_PE_Potentially_Blocking_Operation
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Unchecked_Union_Restriction -- 30
+ procedure Rcheck_PE_Stubbed_Subprogram_Called
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Non_Transportable_Actual -- 31
+ procedure Rcheck_PE_Unchecked_Union_Restriction
(File : System.Address; Line : Integer);
- procedure Rcheck_SE_Empty_Storage_Pool -- 32
+ procedure Rcheck_SE_Empty_Storage_Pool
(File : System.Address; Line : Integer);
- procedure Rcheck_SE_Explicit_Raise -- 33
+ procedure Rcheck_SE_Explicit_Raise
(File : System.Address; Line : Integer);
- procedure Rcheck_SE_Infinite_Recursion -- 34
+ procedure Rcheck_SE_Infinite_Recursion
(File : System.Address; Line : Integer);
- procedure Rcheck_SE_Object_Too_Large -- 35
+ procedure Rcheck_SE_Object_Too_Large
(File : System.Address; Line : Integer);
- procedure Rcheck_PE_Stream_Operation_Not_Allowed -- 36
+ procedure Rcheck_PE_Stream_Operation_Not_Allowed
(File : System.Address; Line : Integer);
+ procedure Rcheck_CE_Access_Check_Ext
+ (File : System.Address; Line, Column : Integer);
+ procedure Rcheck_CE_Index_Check_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer);
+ procedure Rcheck_CE_Invalid_Data_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer);
+ procedure Rcheck_CE_Range_Check_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer);
- procedure Rcheck_PE_Finalize_Raised_Exception -- 23
+ procedure Rcheck_PE_Finalize_Raised_Exception
(File : System.Address; Line : Integer);
-- This routine is separated out because it has quite different behavior
-- from the others. This is the "finalize/adjust raised exception". This
pragma Export (C, Rcheck_SE_Object_Too_Large,
"__gnat_rcheck_SE_Object_Too_Large");
+ pragma Export (C, Rcheck_CE_Access_Check_Ext,
+ "__gnat_rcheck_CE_Access_Check_ext");
+ pragma Export (C, Rcheck_CE_Index_Check_Ext,
+ "__gnat_rcheck_CE_Index_Check_ext");
+ pragma Export (C, Rcheck_CE_Invalid_Data_Ext,
+ "__gnat_rcheck_CE_Invalid_Data_ext");
+ pragma Export (C, Rcheck_CE_Range_Check_Ext,
+ "__gnat_rcheck_CE_Range_Check_ext");
+
-- None of these procedures ever returns (they raise an exception). By
-- using pragma No_Return, we ensure that any junk code after the call,
-- such as normal return epilogue stuff, can be eliminated).
pragma No_Return (Rcheck_PE_Implicit_Return);
pragma No_Return (Rcheck_PE_Misaligned_Address_Value);
pragma No_Return (Rcheck_PE_Missing_Return);
- pragma No_Return (Rcheck_PE_Overlaid_Controlled_Object);
pragma No_Return (Rcheck_PE_Non_Transportable_Actual);
+ pragma No_Return (Rcheck_PE_Overlaid_Controlled_Object);
pragma No_Return (Rcheck_PE_Potentially_Blocking_Operation);
pragma No_Return (Rcheck_PE_Stream_Operation_Not_Allowed);
pragma No_Return (Rcheck_PE_Stubbed_Subprogram_Called);
pragma No_Return (Rcheck_SE_Infinite_Recursion);
pragma No_Return (Rcheck_SE_Object_Too_Large);
- -- For compatibility with previous version of GNAT, to preserve bootstrap
-
- procedure Rcheck_00 (File : System.Address; Line : Integer);
- procedure Rcheck_01 (File : System.Address; Line : Integer);
- procedure Rcheck_02 (File : System.Address; Line : Integer);
- procedure Rcheck_03 (File : System.Address; Line : Integer);
- procedure Rcheck_04 (File : System.Address; Line : Integer);
- procedure Rcheck_05 (File : System.Address; Line : Integer);
- procedure Rcheck_06 (File : System.Address; Line : Integer);
- procedure Rcheck_07 (File : System.Address; Line : Integer);
- procedure Rcheck_08 (File : System.Address; Line : Integer);
- procedure Rcheck_09 (File : System.Address; Line : Integer);
- procedure Rcheck_10 (File : System.Address; Line : Integer);
- procedure Rcheck_11 (File : System.Address; Line : Integer);
- procedure Rcheck_12 (File : System.Address; Line : Integer);
- procedure Rcheck_13 (File : System.Address; Line : Integer);
- procedure Rcheck_14 (File : System.Address; Line : Integer);
- procedure Rcheck_15 (File : System.Address; Line : Integer);
- procedure Rcheck_16 (File : System.Address; Line : Integer);
- procedure Rcheck_17 (File : System.Address; Line : Integer);
- procedure Rcheck_18 (File : System.Address; Line : Integer);
- procedure Rcheck_19 (File : System.Address; Line : Integer);
- procedure Rcheck_20 (File : System.Address; Line : Integer);
- procedure Rcheck_21 (File : System.Address; Line : Integer);
- procedure Rcheck_22 (File : System.Address; Line : Integer);
- procedure Rcheck_23 (File : System.Address; Line : Integer);
- procedure Rcheck_24 (File : System.Address; Line : Integer);
- procedure Rcheck_25 (File : System.Address; Line : Integer);
- procedure Rcheck_26 (File : System.Address; Line : Integer);
- procedure Rcheck_27 (File : System.Address; Line : Integer);
- procedure Rcheck_28 (File : System.Address; Line : Integer);
- procedure Rcheck_29 (File : System.Address; Line : Integer);
- procedure Rcheck_30 (File : System.Address; Line : Integer);
- procedure Rcheck_31 (File : System.Address; Line : Integer);
- procedure Rcheck_32 (File : System.Address; Line : Integer);
- procedure Rcheck_33 (File : System.Address; Line : Integer);
- procedure Rcheck_34 (File : System.Address; Line : Integer);
- procedure Rcheck_35 (File : System.Address; Line : Integer);
- procedure Rcheck_36 (File : System.Address; Line : Integer);
-
- pragma Export (C, Rcheck_00, "__gnat_rcheck_00");
- pragma Export (C, Rcheck_01, "__gnat_rcheck_01");
- pragma Export (C, Rcheck_02, "__gnat_rcheck_02");
- pragma Export (C, Rcheck_03, "__gnat_rcheck_03");
- pragma Export (C, Rcheck_04, "__gnat_rcheck_04");
- pragma Export (C, Rcheck_05, "__gnat_rcheck_05");
- pragma Export (C, Rcheck_06, "__gnat_rcheck_06");
- pragma Export (C, Rcheck_07, "__gnat_rcheck_07");
- pragma Export (C, Rcheck_08, "__gnat_rcheck_08");
- pragma Export (C, Rcheck_09, "__gnat_rcheck_09");
- pragma Export (C, Rcheck_10, "__gnat_rcheck_10");
- pragma Export (C, Rcheck_11, "__gnat_rcheck_11");
- pragma Export (C, Rcheck_12, "__gnat_rcheck_12");
- pragma Export (C, Rcheck_13, "__gnat_rcheck_13");
- pragma Export (C, Rcheck_14, "__gnat_rcheck_14");
- pragma Export (C, Rcheck_15, "__gnat_rcheck_15");
- pragma Export (C, Rcheck_16, "__gnat_rcheck_16");
- pragma Export (C, Rcheck_17, "__gnat_rcheck_17");
- pragma Export (C, Rcheck_18, "__gnat_rcheck_18");
- pragma Export (C, Rcheck_19, "__gnat_rcheck_19");
- pragma Export (C, Rcheck_20, "__gnat_rcheck_20");
- pragma Export (C, Rcheck_21, "__gnat_rcheck_21");
- pragma Export (C, Rcheck_22, "__gnat_rcheck_22");
- pragma Export (C, Rcheck_23, "__gnat_rcheck_23");
- pragma Export (C, Rcheck_24, "__gnat_rcheck_24");
- pragma Export (C, Rcheck_25, "__gnat_rcheck_25");
- pragma Export (C, Rcheck_26, "__gnat_rcheck_26");
- pragma Export (C, Rcheck_27, "__gnat_rcheck_27");
- pragma Export (C, Rcheck_28, "__gnat_rcheck_28");
- pragma Export (C, Rcheck_29, "__gnat_rcheck_29");
- pragma Export (C, Rcheck_30, "__gnat_rcheck_30");
- pragma Export (C, Rcheck_31, "__gnat_rcheck_31");
- pragma Export (C, Rcheck_32, "__gnat_rcheck_32");
- pragma Export (C, Rcheck_33, "__gnat_rcheck_33");
- pragma Export (C, Rcheck_34, "__gnat_rcheck_34");
- pragma Export (C, Rcheck_35, "__gnat_rcheck_35");
- pragma Export (C, Rcheck_36, "__gnat_rcheck_36");
-
- -- None of these procedures ever returns (they raise an exception). By
- -- using pragma No_Return, we ensure that any junk code after the call,
- -- such as normal return epilogue stuff, can be eliminated).
-
- pragma No_Return (Rcheck_00);
- pragma No_Return (Rcheck_01);
- pragma No_Return (Rcheck_02);
- pragma No_Return (Rcheck_03);
- pragma No_Return (Rcheck_04);
- pragma No_Return (Rcheck_05);
- pragma No_Return (Rcheck_06);
- pragma No_Return (Rcheck_07);
- pragma No_Return (Rcheck_08);
- pragma No_Return (Rcheck_09);
- pragma No_Return (Rcheck_10);
- pragma No_Return (Rcheck_11);
- pragma No_Return (Rcheck_12);
- pragma No_Return (Rcheck_13);
- pragma No_Return (Rcheck_14);
- pragma No_Return (Rcheck_15);
- pragma No_Return (Rcheck_16);
- pragma No_Return (Rcheck_17);
- pragma No_Return (Rcheck_18);
- pragma No_Return (Rcheck_19);
- pragma No_Return (Rcheck_20);
- pragma No_Return (Rcheck_21);
- pragma No_Return (Rcheck_22);
- pragma No_Return (Rcheck_23);
- pragma No_Return (Rcheck_24);
- pragma No_Return (Rcheck_25);
- pragma No_Return (Rcheck_26);
- pragma No_Return (Rcheck_27);
- pragma No_Return (Rcheck_28);
- pragma No_Return (Rcheck_29);
- pragma No_Return (Rcheck_30);
- pragma No_Return (Rcheck_32);
- pragma No_Return (Rcheck_33);
- pragma No_Return (Rcheck_34);
- pragma No_Return (Rcheck_35);
- pragma No_Return (Rcheck_36);
+ pragma No_Return (Rcheck_CE_Access_Check_Ext);
+ pragma No_Return (Rcheck_CE_Index_Check_Ext);
+ pragma No_Return (Rcheck_CE_Invalid_Data_Ext);
+ pragma No_Return (Rcheck_CE_Range_Check_Ext);
---------------------------------------------
-- Reason Strings for Run-Time Check Calls --
-- The actual polling routine is separate, so that it can easily be
-- replaced with a target dependent version.
+ --------------------------
+ -- Code_Address_For_AAA --
+ --------------------------
+
+ -- This function gives us the start of the PC range for addresses within
+ -- the exception unit itself. We hope that gigi/gcc keep all the procedures
+ -- in their original order.
+
+ function Code_Address_For_AAA return System.Address is
+ begin
+ -- We are using a label instead of Code_Address_For_AAA'Address because
+ -- on some platforms the latter does not yield the address we want, but
+ -- the address of a stub or of a descriptor instead. This is the case at
+ -- least on PA-HPUX.
+
+ <<Start_Of_AAA>>
+ return Start_Of_AAA'Address;
+ end Code_Address_For_AAA;
+
+ ----------------
+ -- Call_Chain --
+ ----------------
+
+ procedure Call_Chain (Excep : EOA) is separate;
+ -- The actual Call_Chain routine is separate, so that it can easily
+ -- be dummied out when no exception traceback information is needed.
+
-------------------
-- EId_To_String --
-------------------
(X : Exception_Occurrence) return Exception_Id
is
begin
- -- Note that the following test used to be here for the original Ada 95
- -- semantics, but these were modified by AI-241 to require returning
- -- Null_Id instead of raising Constraint_Error.
+ -- Note that the following test used to be here for the original
+ -- Ada 95 semantics, but these were modified by AI-241 to require
+ -- returning Null_Id instead of raising Constraint_Error.
-- if X.Id = Null_Id then
-- raise Constraint_Error;
begin
if X.Id = Null_Id then
raise Constraint_Error;
+ else
+ return X.Msg (1 .. X.Msg_Length);
end if;
-
- return X.Msg (1 .. X.Msg_Length);
end Exception_Message;
--------------------
begin
if Id = null then
raise Constraint_Error;
+ else
+ return To_Ptr (Id.Full_Name) (1 .. Id.Name_Length - 1);
end if;
-
- return To_Ptr (Id.Full_Name) (1 .. Id.Name_Length - 1);
end Exception_Name;
function Exception_Name (X : Exception_Occurrence) return String is
-- This package can be easily dummied out if we do not want the basic
-- support for exception messages (such as in Ada 83).
+ ---------------------------
+ -- Exception_Propagation --
+ ---------------------------
+
+ package body Exception_Propagation is separate;
+ -- Depending on the actual exception mechanism used (front-end or
+ -- back-end based), the implementation will differ, which is why this
+ -- package is separated.
+
----------------------
-- Exception_Traces --
----------------------
package body Exception_Traces is separate;
-- Depending on the underlying support for IO the implementation will
- -- differ. Moreover we would like to dummy out this package in case we do
- -- not want any exception tracing support. This is why this package is
- -- separated.
+ -- differ. Moreover we would like to dummy out this package in case we
+ -- do not want any exception tracing support. This is why this package
+ -- is separated.
+
+ --------------------------------------
+ -- Get_Exception_Machine_Occurrence --
+ --------------------------------------
+
+ function Get_Exception_Machine_Occurrence
+ (X : Exception_Occurrence) return System.Address
+ is
+ begin
+ return X.Machine_Occurrence;
+ end Get_Exception_Machine_Occurrence;
+
+ -----------
+ -- Image --
+ -----------
+
+ function Image (Index : Integer) return String is
+ Result : constant String := Integer'Image (Index);
+ begin
+ if Result (1) = ' ' then
+ return Result (2 .. Result'Last);
+ else
+ return Result;
+ end if;
+ end Image;
-----------------------
-- Stream Attributes --
-- This package can be easily dummied out if we do not want the
-- support for streaming Exception_Ids and Exception_Occurrences.
- -----------------------------
- -- Process_Raise_Exception --
- -----------------------------
-
- procedure Process_Raise_Exception (E : Exception_Id) is
- pragma Inspection_Point (E);
- -- This is so the debugger can reliably inspect the parameter
-
- Jumpbuf_Ptr : constant Address := Get_Jmpbuf_Address.all;
- Excep : constant EOA := Get_Current_Excep.all;
-
- procedure builtin_longjmp (buffer : Address; Flag : Integer);
- pragma No_Return (builtin_longjmp);
- pragma Import (C, builtin_longjmp, "_gnat_builtin_longjmp");
-
- begin
- -- WARNING: There should be no exception handler for this body because
- -- this would cause gigi to prepend a setup for a new jmpbuf to the
- -- sequence of statements in case of built-in sjljl. We would then
- -- always get this new buf in Jumpbuf_Ptr instead of the one for the
- -- exception we are handling, which would completely break the whole
- -- design of this procedure.
-
- -- If the jump buffer pointer is non-null, transfer control using it.
- -- Otherwise announce an unhandled exception (note that this means that
- -- we have no finalizations to do other than at the outer level).
- -- Perform the necessary notification tasks in both cases.
-
- if Jumpbuf_Ptr /= Null_Address then
- if not Excep.Exception_Raised then
- Excep.Exception_Raised := True;
- Exception_Traces.Notify_Handled_Exception (Excep);
- end if;
-
- builtin_longjmp (Jumpbuf_Ptr, 1);
-
- else
- Exception_Traces.Notify_Unhandled_Exception (Excep);
- Exception_Traces.Unhandled_Exception_Terminate (Excep);
- end if;
- end Process_Raise_Exception;
-
----------------------------
-- Raise_Constraint_Error --
----------------------------
- procedure Raise_Constraint_Error
- (File : System.Address;
- Line : Integer)
- is
+ procedure Raise_Constraint_Error (File : System.Address; Line : Integer) is
begin
- Raise_With_Location_And_Msg
- (Constraint_Error_Def'Access, File, Line);
+ Raise_With_Location_And_Msg (Constraint_Error_Def'Access, File, Line);
end Raise_Constraint_Error;
--------------------------------
--------------------------------
procedure Raise_Constraint_Error_Msg
- (File : System.Address;
- Line : Integer;
- Msg : System.Address)
+ (File : System.Address;
+ Line : Integer;
+ Column : Integer;
+ Msg : System.Address)
is
begin
Raise_With_Location_And_Msg
- (Constraint_Error_Def'Access, File, Line, Msg);
+ (Constraint_Error_Def'Access, File, Line, Column, Msg);
end Raise_Constraint_Error_Msg;
-------------------------
- -- Raise_Current_Excep --
+ -- Complete_Occurrence --
-------------------------
- procedure Raise_Current_Excep (E : Exception_Id) is
+ procedure Complete_Occurrence (X : EOA) is
+ begin
+ -- Compute the backtrace for this occurrence if the corresponding
+ -- binder option has been set. Call_Chain takes care of the reraise
+ -- case.
+
+ -- ??? Using Call_Chain here means we are going to walk up the stack
+ -- once only for backtracing purposes before doing it again for the
+ -- propagation per se.
+
+ -- The first inspection is much lighter, though, as it only requires
+ -- partial unwinding of each frame. Additionally, although we could use
+ -- the personality routine to record the addresses while propagating,
+ -- this method has two drawbacks:
+
+ -- 1) the trace is incomplete if the exception is handled since we
+ -- don't walk past the frame with the handler,
- pragma Inspection_Point (E);
- -- This is so the debugger can reliably inspect the parameter when
- -- inserting a breakpoint at the start of this procedure.
+ -- and
- Id : Exception_Id := E;
- pragma Volatile (Id);
- pragma Warnings (Off, Id);
- -- In order to provide support for breakpoints on unhandled exceptions,
- -- the debugger will also need to be able to inspect the value of E from
- -- another (inner) frame. So we need to make sure that if E is passed in
- -- a register, its value is also spilled on stack. For this, we store
- -- the parameter value in a local variable, and add a pragma Volatile to
- -- make sure it is spilled. The pragma Warnings (Off) is needed because
- -- the compiler knows that Id is not referenced and that this use of
- -- pragma Volatile is peculiar.
+ -- 2) we would miss the frames for which our personality routine is not
+ -- called, e.g. if C or C++ calls are on the way.
+ Call_Chain (X);
+
+ -- Notify the debugger
+ Debug_Raise_Exception
+ (E => SSL.Exception_Data_Ptr (X.Id),
+ Message => X.Msg (1 .. X.Msg_Length));
+ end Complete_Occurrence;
+
+ ---------------------------------------
+ -- Complete_And_Propagate_Occurrence --
+ ---------------------------------------
+
+ procedure Complete_And_Propagate_Occurrence (X : EOA) is
begin
- Debug_Raise_Exception (E => SSL.Exception_Data_Ptr (E), Message => "");
- Process_Raise_Exception (E);
- end Raise_Current_Excep;
+ Complete_Occurrence (X);
+ Exception_Propagation.Propagate_Exception (X);
+ end Complete_And_Propagate_Occurrence;
---------------------
-- Raise_Exception --
(E : Exception_Id;
Message : String := "")
is
- EF : Exception_Id := E;
- Excep : constant EOA := Get_Current_Excep.all;
+ EF : Exception_Id := E;
begin
-- Raise CE if E = Null_ID (AI-446)
-- Go ahead and raise appropriate exception
- Exception_Data.Set_Exception_Msg (Excep, EF, Message);
- Abort_Defer.all;
- Raise_Current_Excep (EF);
+ Raise_Exception_Always (EF, Message);
end Raise_Exception;
----------------------------
(E : Exception_Id;
Message : String := "")
is
- Excep : constant EOA := Get_Current_Excep.all;
+ X : constant EOA := Exception_Propagation.Allocate_Occurrence;
+
begin
- Exception_Data.Set_Exception_Msg (Excep, E, Message);
- Abort_Defer.all;
- Raise_Current_Excep (E);
+ Exception_Data.Set_Exception_Msg (X, E, Message);
+
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Complete_And_Propagate_Occurrence (X);
end Raise_Exception_Always;
------------------------------
(E : Exception_Id;
Message : String := "")
is
- Excep : constant EOA := Get_Current_Excep.all;
+ X : constant EOA := Exception_Propagation.Allocate_Occurrence;
+
begin
- Exception_Data.Set_Exception_Msg (Excep, E, Message);
+ Exception_Data.Set_Exception_Msg (X, E, Message);
-- Do not call Abort_Defer.all, as specified by the spec
- Raise_Current_Excep (E);
+ Complete_And_Propagate_Occurrence (X);
end Raise_Exception_No_Defer;
-------------------------------------
Prefix : constant String := "adjust/finalize raised ";
Orig_Msg : constant String := Exception_Message (X);
Orig_Prefix_Length : constant Natural :=
- Integer'Min (Prefix'Length, Orig_Msg'Length);
- Orig_Prefix : String renames Orig_Msg
- (Orig_Msg'First .. Orig_Msg'First + Orig_Prefix_Length - 1);
+ Integer'Min (Prefix'Length, Orig_Msg'Length);
+
+ Orig_Prefix : String renames
+ Orig_Msg (Orig_Msg'First .. Orig_Msg'First + Orig_Prefix_Length - 1);
+
begin
- -- Message already has proper prefix, just re-reraise
+ -- Message already has the proper prefix, just re-raise
if Orig_Prefix = Prefix then
Raise_Exception_No_Defer
end if;
end Raise_From_Controlled_Operation;
+ -------------------------------------------
+ -- Create_Occurrence_From_Signal_Handler --
+ -------------------------------------------
+
+ function Create_Occurrence_From_Signal_Handler
+ (E : Exception_Id;
+ M : System.Address) return EOA
+ is
+ X : constant EOA := Exception_Propagation.Allocate_Occurrence;
+
+ begin
+ Exception_Data.Set_Exception_C_Msg (X, E, M);
+
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Complete_Occurrence (X);
+ return X;
+ end Create_Occurrence_From_Signal_Handler;
+
+ ---------------------------------------------------
+ -- Create_Machine_Occurrence_From_Signal_Handler --
+ ---------------------------------------------------
+
+ function Create_Machine_Occurrence_From_Signal_Handler
+ (E : Exception_Id;
+ M : System.Address) return System.Address
+ is
+ begin
+ return Create_Occurrence_From_Signal_Handler (E, M).Machine_Occurrence;
+ end Create_Machine_Occurrence_From_Signal_Handler;
+
-------------------------------
-- Raise_From_Signal_Handler --
-------------------------------
(E : Exception_Id;
M : System.Address)
is
- Excep : constant EOA := Get_Current_Excep.all;
begin
- Exception_Data.Set_Exception_C_Msg (Excep, E, M);
- Abort_Defer.all;
- Process_Raise_Exception (E);
+ Exception_Propagation.Propagate_Exception
+ (Create_Occurrence_From_Signal_Handler (E, M));
end Raise_From_Signal_Handler;
-------------------------
Line : Integer)
is
begin
- Raise_With_Location_And_Msg
- (Program_Error_Def'Access, File, Line);
+ Raise_With_Location_And_Msg (Program_Error_Def'Access, File, Line);
end Raise_Program_Error;
-----------------------------
is
begin
Raise_With_Location_And_Msg
- (Program_Error_Def'Access, File, Line, Msg);
+ (Program_Error_Def'Access, File, Line, M => Msg);
end Raise_Program_Error_Msg;
-------------------------
Line : Integer)
is
begin
- Raise_With_Location_And_Msg
- (Storage_Error_Def'Access, File, Line);
+ Raise_With_Location_And_Msg (Storage_Error_Def'Access, File, Line);
end Raise_Storage_Error;
-----------------------------
is
begin
Raise_With_Location_And_Msg
- (Storage_Error_Def'Access, File, Line, Msg);
+ (Storage_Error_Def'Access, File, Line, M => Msg);
end Raise_Storage_Error_Msg;
---------------------------------
(E : Exception_Id;
F : System.Address;
L : Integer;
+ C : Integer := 0;
M : System.Address := System.Null_Address)
is
- Excep : constant EOA := Get_Current_Excep.all;
+ X : constant EOA := Exception_Propagation.Allocate_Occurrence;
begin
- Exception_Data.Set_Exception_C_Msg (Excep, E, F, L, Msg2 => M);
- Abort_Defer.all;
- Raise_Current_Excep (E);
+ Exception_Data.Set_Exception_C_Msg (X, E, F, L, C, M);
+
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Complete_And_Propagate_Occurrence (X);
end Raise_With_Location_And_Msg;
--------------------
--------------------
procedure Raise_With_Msg (E : Exception_Id) is
- Excep : constant EOA := Get_Current_Excep.all;
-
+ Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
+ Ex : constant Exception_Occurrence_Access := Get_Current_Excep.all;
begin
Excep.Exception_Raised := False;
Excep.Id := E;
Excep.Num_Tracebacks := 0;
Excep.Pid := Local_Partition_ID;
- Abort_Defer.all;
- Raise_Current_Excep (E);
+
+ -- Copy the message from the current exception
+ -- Change the interface to be called with an occurrence ???
+
+ Excep.Msg_Length := Ex.Msg_Length;
+ Excep.Msg (1 .. Excep.Msg_Length) := Ex.Msg (1 .. Ex.Msg_Length);
+
+ -- The following is a common pattern, should be abstracted
+ -- into a procedure call ???
+
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Complete_And_Propagate_Occurrence (Excep);
end Raise_With_Msg;
-----------------------------------------
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_00'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_00'Address);
end Rcheck_CE_Access_Check;
procedure Rcheck_CE_Null_Access_Parameter
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_01'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_01'Address);
end Rcheck_CE_Null_Access_Parameter;
procedure Rcheck_CE_Discriminant_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_02'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_02'Address);
end Rcheck_CE_Discriminant_Check;
procedure Rcheck_CE_Divide_By_Zero
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_03'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_03'Address);
end Rcheck_CE_Divide_By_Zero;
procedure Rcheck_CE_Explicit_Raise
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_04'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_04'Address);
end Rcheck_CE_Explicit_Raise;
procedure Rcheck_CE_Index_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_05'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_05'Address);
end Rcheck_CE_Index_Check;
procedure Rcheck_CE_Invalid_Data
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_06'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_06'Address);
end Rcheck_CE_Invalid_Data;
procedure Rcheck_CE_Length_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_07'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_07'Address);
end Rcheck_CE_Length_Check;
procedure Rcheck_CE_Null_Exception_Id
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_08'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_08'Address);
end Rcheck_CE_Null_Exception_Id;
procedure Rcheck_CE_Null_Not_Allowed
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_09'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_09'Address);
end Rcheck_CE_Null_Not_Allowed;
procedure Rcheck_CE_Overflow_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_10'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_10'Address);
end Rcheck_CE_Overflow_Check;
procedure Rcheck_CE_Partition_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_11'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_11'Address);
end Rcheck_CE_Partition_Check;
procedure Rcheck_CE_Range_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_12'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_12'Address);
end Rcheck_CE_Range_Check;
procedure Rcheck_CE_Tag_Check
(File : System.Address; Line : Integer)
is
begin
- Raise_Constraint_Error_Msg (File, Line, Rmsg_13'Address);
+ Raise_Constraint_Error_Msg (File, Line, 0, Rmsg_13'Address);
end Rcheck_CE_Tag_Check;
procedure Rcheck_PE_Access_Before_Elaboration
Raise_Program_Error_Msg (File, Line, Rmsg_26'Address);
end Rcheck_PE_Missing_Return;
+ procedure Rcheck_PE_Non_Transportable_Actual
+ (File : System.Address; Line : Integer)
+ is
+ begin
+ Raise_Program_Error_Msg (File, Line, Rmsg_31'Address);
+ end Rcheck_PE_Non_Transportable_Actual;
+
procedure Rcheck_PE_Overlaid_Controlled_Object
(File : System.Address; Line : Integer)
is
Raise_Program_Error_Msg (File, Line, Rmsg_28'Address);
end Rcheck_PE_Potentially_Blocking_Operation;
+ procedure Rcheck_PE_Stream_Operation_Not_Allowed
+ (File : System.Address; Line : Integer)
+ is
+ begin
+ Raise_Program_Error_Msg (File, Line, Rmsg_36'Address);
+ end Rcheck_PE_Stream_Operation_Not_Allowed;
+
procedure Rcheck_PE_Stubbed_Subprogram_Called
(File : System.Address; Line : Integer)
is
Raise_Program_Error_Msg (File, Line, Rmsg_30'Address);
end Rcheck_PE_Unchecked_Union_Restriction;
- procedure Rcheck_PE_Non_Transportable_Actual
- (File : System.Address; Line : Integer)
- is
- begin
- Raise_Program_Error_Msg (File, Line, Rmsg_31'Address);
- end Rcheck_PE_Non_Transportable_Actual;
-
procedure Rcheck_SE_Empty_Storage_Pool
(File : System.Address; Line : Integer)
is
Raise_Storage_Error_Msg (File, Line, Rmsg_35'Address);
end Rcheck_SE_Object_Too_Large;
- procedure Rcheck_PE_Stream_Operation_Not_Allowed
- (File : System.Address; Line : Integer)
+ procedure Rcheck_CE_Access_Check_Ext
+ (File : System.Address; Line, Column : Integer)
is
begin
- Raise_Program_Error_Msg (File, Line, Rmsg_36'Address);
- end Rcheck_PE_Stream_Operation_Not_Allowed;
+ Raise_Constraint_Error_Msg (File, Line, Column, Rmsg_00'Address);
+ end Rcheck_CE_Access_Check_Ext;
+
+ procedure Rcheck_CE_Index_Check_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer)
+ is
+ Msg : constant String :=
+ Rmsg_05 (Rmsg_05'First .. Rmsg_05'Last - 1) & ASCII.LF
+ & "index " & Image (Index) & " not in " & Image (First)
+ & ".." & Image (Last) & ASCII.NUL;
+ begin
+ Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
+ end Rcheck_CE_Index_Check_Ext;
+
+ procedure Rcheck_CE_Invalid_Data_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer)
+ is
+ Msg : constant String :=
+ Rmsg_06 (Rmsg_06'First .. Rmsg_06'Last - 1) & ASCII.LF
+ & "value " & Image (Index) & " not in " & Image (First)
+ & ".." & Image (Last) & ASCII.NUL;
+ begin
+ Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
+ end Rcheck_CE_Invalid_Data_Ext;
+
+ procedure Rcheck_CE_Range_Check_Ext
+ (File : System.Address; Line, Column, Index, First, Last : Integer)
+ is
+ Msg : constant String :=
+ Rmsg_12 (Rmsg_12'First .. Rmsg_12'Last - 1) & ASCII.LF
+ & "value " & Image (Index) & " not in " & Image (First)
+ & ".." & Image (Last) & ASCII.NUL;
+ begin
+ Raise_Constraint_Error_Msg (File, Line, Column, Msg'Address);
+ end Rcheck_CE_Range_Check_Ext;
procedure Rcheck_PE_Finalize_Raised_Exception
(File : System.Address; Line : Integer)
is
- E : constant Exception_Id := Program_Error_Def'Access;
- Excep : constant EOA := Get_Current_Excep.all;
+ X : constant EOA := Exception_Propagation.Allocate_Occurrence;
begin
-- This is "finalize/adjust raised exception". This subprogram is always
- -- called with abort deferred, unlike all other Rcheck_* subprograms,
- -- itneeds to call Raise_Exception_No_Defer.
+ -- called with abort deferred, unlike all other Rcheck_* subprograms, it
+ -- needs to call Raise_Exception_No_Defer.
-- This is consistent with Raise_From_Controlled_Operation
- Exception_Data.Set_Exception_C_Msg (Excep, E, File, Line, 0,
- Rmsg_23'Address);
- Raise_Current_Excep (E);
+ Exception_Data.Set_Exception_C_Msg
+ (X, Program_Error_Def'Access, File, Line, 0, Rmsg_23'Address);
+ Complete_And_Propagate_Occurrence (X);
end Rcheck_PE_Finalize_Raised_Exception;
- procedure Rcheck_00 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Access_Check;
- procedure Rcheck_01 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Null_Access_Parameter;
- procedure Rcheck_02 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Discriminant_Check;
- procedure Rcheck_03 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Divide_By_Zero;
- procedure Rcheck_04 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Explicit_Raise;
- procedure Rcheck_05 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Index_Check;
- procedure Rcheck_06 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Invalid_Data;
- procedure Rcheck_07 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Length_Check;
- procedure Rcheck_08 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Null_Exception_Id;
- procedure Rcheck_09 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Null_Not_Allowed;
- procedure Rcheck_10 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Overflow_Check;
- procedure Rcheck_11 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Partition_Check;
- procedure Rcheck_12 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Range_Check;
- procedure Rcheck_13 (File : System.Address; Line : Integer)
- renames Rcheck_CE_Tag_Check;
- procedure Rcheck_14 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Access_Before_Elaboration;
- procedure Rcheck_15 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Accessibility_Check;
- procedure Rcheck_16 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Address_Of_Intrinsic;
- procedure Rcheck_17 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Aliased_Parameters;
- procedure Rcheck_18 (File : System.Address; Line : Integer)
- renames Rcheck_PE_All_Guards_Closed;
- procedure Rcheck_19 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Bad_Predicated_Generic_Type;
- procedure Rcheck_20 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Current_Task_In_Entry_Body;
- procedure Rcheck_21 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Duplicated_Entry_Address;
- procedure Rcheck_22 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Explicit_Raise;
- procedure Rcheck_23 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Finalize_Raised_Exception;
- procedure Rcheck_24 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Implicit_Return;
- procedure Rcheck_25 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Misaligned_Address_Value;
- procedure Rcheck_26 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Missing_Return;
- procedure Rcheck_27 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Overlaid_Controlled_Object;
- procedure Rcheck_28 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Potentially_Blocking_Operation;
- procedure Rcheck_29 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Stubbed_Subprogram_Called;
- procedure Rcheck_30 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Unchecked_Union_Restriction;
- procedure Rcheck_31 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Non_Transportable_Actual;
- procedure Rcheck_32 (File : System.Address; Line : Integer)
- renames Rcheck_SE_Empty_Storage_Pool;
- procedure Rcheck_33 (File : System.Address; Line : Integer)
- renames Rcheck_SE_Explicit_Raise;
- procedure Rcheck_34 (File : System.Address; Line : Integer)
- renames Rcheck_SE_Infinite_Recursion;
- procedure Rcheck_35 (File : System.Address; Line : Integer)
- renames Rcheck_SE_Object_Too_Large;
- procedure Rcheck_36 (File : System.Address; Line : Integer)
- renames Rcheck_PE_Stream_Operation_Not_Allowed;
-
-------------
-- Reraise --
-------------
procedure Reraise is
- Excep : constant EOA := Get_Current_Excep.all;
+ Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
+ Saved_MO : constant System.Address := Excep.Machine_Occurrence;
begin
- Abort_Defer.all;
- Raise_Current_Excep (Excep.Id);
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Save_Occurrence (Excep.all, Get_Current_Excep.all.all);
+ Excep.Machine_Occurrence := Saved_MO;
+ Complete_And_Propagate_Occurrence (Excep);
end Reraise;
--------------------------------------
procedure Reraise_Library_Exception_If_Any is
LE : Exception_Occurrence;
+
begin
if Library_Exception_Set then
LE := Library_Exception;
- Raise_From_Controlled_Operation (LE);
+
+ if LE.Id = Null_Id then
+ Raise_Exception_No_Defer
+ (E => Program_Error'Identity,
+ Message => "finalize/adjust raised exception");
+ else
+ Raise_From_Controlled_Operation (LE);
+ end if;
end if;
end Reraise_Library_Exception_If_Any;
procedure Reraise_Occurrence (X : Exception_Occurrence) is
begin
- if X.Id /= null then
- Abort_Defer.all;
- Save_Occurrence (Get_Current_Excep.all.all, X);
- Raise_Current_Excep (X.Id);
+ if X.Id = null then
+ return;
+ else
+ Reraise_Occurrence_Always (X);
end if;
end Reraise_Occurrence;
procedure Reraise_Occurrence_Always (X : Exception_Occurrence) is
begin
- Abort_Defer.all;
- Save_Occurrence (Get_Current_Excep.all.all, X);
- Raise_Current_Excep (X.Id);
+ if not ZCX_By_Default then
+ Abort_Defer.all;
+ end if;
+
+ Reraise_Occurrence_No_Defer (X);
end Reraise_Occurrence_Always;
---------------------------------
---------------------------------
procedure Reraise_Occurrence_No_Defer (X : Exception_Occurrence) is
+ Excep : constant EOA := Exception_Propagation.Allocate_Occurrence;
+ Saved_MO : constant System.Address := Excep.Machine_Occurrence;
begin
- Save_Occurrence (Get_Current_Excep.all.all, X);
- Raise_Current_Excep (X.Id);
+ Save_Occurrence (Excep.all, X);
+ Excep.Machine_Occurrence := Saved_MO;
+ Complete_And_Propagate_Occurrence (Excep);
end Reraise_Occurrence_No_Defer;
---------------------
Source : Exception_Occurrence)
is
begin
- Target.Id := Source.Id;
- Target.Msg_Length := Source.Msg_Length;
- Target.Num_Tracebacks := Source.Num_Tracebacks;
- Target.Pid := Source.Pid;
+ -- As the machine occurrence might be a data that must be finalized
+ -- (outside any Ada mechanism), do not copy it
+
+ Target.Id := Source.Id;
+ Target.Machine_Occurrence := System.Null_Address;
+ Target.Msg_Length := Source.Msg_Length;
+ Target.Num_Tracebacks := Source.Num_Tracebacks;
+ Target.Pid := Source.Pid;
Target.Msg (1 .. Target.Msg_Length) :=
Source.Msg (1 .. Target.Msg_Length);
---------------
procedure To_Stderr (C : Character) is
- type int is new Integer;
-
- procedure put_char_stderr (C : int);
- pragma Import (C, put_char_stderr, "put_char_stderr");
-
+ procedure Put_Char_Stderr (C : Character);
+ pragma Import (C, Put_Char_Stderr, "put_char_stderr");
begin
- put_char_stderr (Character'Pos (C));
+ Put_Char_Stderr (C);
end To_Stderr;
procedure To_Stderr (S : String) is
and then Exception_Identity (Ex.all) = Standard'Abort_Signal'Identity;
end Triggered_By_Abort;
+ -------------------------
+ -- Wide_Exception_Name --
+ -------------------------
+
+ WC_Encoding : Character;
+ pragma Import (C, WC_Encoding, "__gl_wc_encoding");
+ -- Encoding method for source, as exported by binder
+
+ function Wide_Exception_Name
+ (Id : Exception_Id) return Wide_String
+ is
+ S : constant String := Exception_Name (Id);
+ W : Wide_String (1 .. S'Length);
+ L : Natural;
+ begin
+ String_To_Wide_String
+ (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
+ return W (1 .. L);
+ end Wide_Exception_Name;
+
+ function Wide_Exception_Name
+ (X : Exception_Occurrence) return Wide_String
+ is
+ S : constant String := Exception_Name (X);
+ W : Wide_String (1 .. S'Length);
+ L : Natural;
+ begin
+ String_To_Wide_String
+ (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
+ return W (1 .. L);
+ end Wide_Exception_Name;
+
+ ----------------------------
+ -- Wide_Wide_Exception_Name --
+ -----------------------------
+
+ function Wide_Wide_Exception_Name
+ (Id : Exception_Id) return Wide_Wide_String
+ is
+ S : constant String := Exception_Name (Id);
+ W : Wide_Wide_String (1 .. S'Length);
+ L : Natural;
+ begin
+ String_To_Wide_Wide_String
+ (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
+ return W (1 .. L);
+ end Wide_Wide_Exception_Name;
+
+ function Wide_Wide_Exception_Name
+ (X : Exception_Occurrence) return Wide_Wide_String
+ is
+ S : constant String := Exception_Name (X);
+ W : Wide_Wide_String (1 .. S'Length);
+ L : Natural;
+ begin
+ String_To_Wide_Wide_String
+ (S, W, L, Get_WC_Encoding_Method (WC_Encoding));
+ return W (1 .. L);
+ end Wide_Wide_Exception_Name;
+
+ --------------------------
+ -- Code_Address_For_ZZZ --
+ --------------------------
+
+ -- This function gives us the end of the PC range for addresses
+ -- within the exception unit itself. We hope that gigi/gcc keeps all the
+ -- procedures in their original order.
+
+ function Code_Address_For_ZZZ return System.Address is
+ begin
+ <<Start_Of_ZZZ>>
+ return Start_Of_ZZZ'Address;
+ end Code_Address_For_ZZZ;
+
end Ada.Exceptions;
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- --
------------------------------------------------------------------------------
--- This version of Ada.Exceptions is used only for building the compiler
--- and certain basic tools. The "real" version of Ada.Exceptions is in
--- a-except-2005.ads/adb, and is used for all other builds where full Ada
--- functionality is required. In particular, it is used for building run
--- times on all targets.
-
--- This version is limited to Ada 95 features. It omits Ada 2005 features
--- such as the additional definitions of Exception_Name returning
--- Wide_[Wide_]String. It differs from the version specified in the Ada 95 RM
--- only in that it is declared Preelaborate (see declaration below for why
--- this is done).
+-- This version of Ada.Exceptions fully supports Ada 95 and later language
+-- versions. It is used in all situations except for the build of the
+-- compiler and other basic tools. For these latter builds, we use an
+-- Ada 95-only version.
-- The reason for this splitting off of a separate version is to support
-- older bootstrap compilers that do not support Ada 2005 features, and
-- Ada.Exceptions is part of the compiler sources.
-pragma Compiler_Unit_Warning;
-
pragma Polling (Off);
-- We must turn polling off for this unit, because otherwise we get
-- elaboration circularities with ourself.
package Ada.Exceptions is
pragma Preelaborate;
- -- We make this preelaborable. If we did not do this, then run time units
- -- used by the compiler (e.g. s-soflin.ads) would run into trouble.
- -- Conformance with Ada 95 is not an issue, since this version is used
- -- only by the compiler.
+ -- In accordance with Ada 2005 AI-362.
type Exception_Id is private;
+ pragma Preelaborable_Initialization (Exception_Id);
Null_Id : constant Exception_Id;
type Exception_Occurrence is limited private;
+ pragma Preelaborable_Initialization (Exception_Occurrence);
type Exception_Occurrence_Access is access all Exception_Occurrence;
Null_Occurrence : constant Exception_Occurrence;
+ function Exception_Name (Id : Exception_Id) return String;
+
function Exception_Name (X : Exception_Occurrence) return String;
- -- Same as Exception_Name (Exception_Identity (X))
- function Exception_Name (Id : Exception_Id) return String;
+ function Wide_Exception_Name
+ (Id : Exception_Id) return Wide_String;
+ pragma Ada_05 (Wide_Exception_Name);
+
+ function Wide_Exception_Name
+ (X : Exception_Occurrence) return Wide_String;
+ pragma Ada_05 (Wide_Exception_Name);
+
+ function Wide_Wide_Exception_Name
+ (Id : Exception_Id) return Wide_Wide_String;
+ pragma Ada_05 (Wide_Wide_Exception_Name);
+
+ function Wide_Wide_Exception_Name
+ (X : Exception_Occurrence) return Wide_Wide_String;
+ pragma Ada_05 (Wide_Wide_Exception_Name);
procedure Raise_Exception (E : Exception_Id; Message : String := "");
pragma No_Return (Raise_Exception);
-- 0xyyyyyyyy 0xyyyyyyyy ...
--
-- The lines are separated by a ASCII.LF character
- -- The nnnn is the partition Id given as decimal digits.
+ --
+ -- The nnnn is the partition Id given as decimal digits
+ --
-- The 0x... line represents traceback program counter locations,
-- in order with the first one being the exception location.
(Source : Exception_Occurrence)
return Exception_Occurrence_Access;
+ -- Ada 2005 (AI-438): The language revision introduces the following
+ -- subprograms and attribute definitions. We do not provide them
+ -- explicitly. instead, the corresponding stream attributes are made
+ -- available through a pragma Stream_Convert in the private part.
+
+ -- procedure Read_Exception_Occurrence
+ -- (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
+ -- Item : out Exception_Occurrence);
+
+ -- procedure Write_Exception_Occurrence
+ -- (Stream : not null access Ada.Streams.Root_Stream_Type'Class;
+ -- Item : Exception_Occurrence);
+
+ -- for Exception_Occurrence'Read use Read_Exception_Occurrence;
+ -- for Exception_Occurrence'Write use Write_Exception_Occurrence;
+
private
package SSL renames System.Standard_Library;
package SP renames System.Parameters;
pragma No_Return (Reraise_Occurrence_No_Defer);
-- Exactly like Reraise_Occurrence, except that abort is not deferred
-- before the call and the parameter X is known not to be the null
- -- occurrence. This is used in generated code when it is known that
- -- abort is already deferred.
+ -- occurrence. This is used in generated code when it is known that abort
+ -- is already deferred.
function Triggered_By_Abort return Boolean;
-- Determine whether the current exception (if it exists) is an instance of
Id : Exception_Id;
-- Exception_Identity for this exception occurrence
+ Machine_Occurrence : System.Address;
+ -- The underlying machine occurrence. For GCC, this corresponds to the
+ -- _Unwind_Exception structure address.
+
Msg_Length : Natural := 0;
-- Length of message (zero = no message)
-- this, and it would not work right, because of the Msg and Tracebacks
-- fields which have unused entries not copied by Save_Occurrence.
+ function Get_Exception_Machine_Occurrence
+ (X : Exception_Occurrence) return System.Address;
+ pragma Export (Ada, Get_Exception_Machine_Occurrence,
+ "__gnat_get_exception_machine_occurrence");
+ -- Get the machine occurrence corresponding to an exception occurrence.
+ -- It is Null_Address if there is no machine occurrence (in runtimes that
+ -- doesn't use GCC mechanism) or if it has been lost (Save_Occurrence
+ -- doesn't save the machine occurrence).
+
function EO_To_String (X : Exception_Occurrence) return String;
function String_To_EO (S : String) return Exception_Occurrence;
pragma Stream_Convert (Exception_Occurrence, String_To_EO, EO_To_String);
-- Functions for implementing Exception_Occurrence stream attributes
Null_Occurrence : constant Exception_Occurrence := (
- Id => null,
- Msg_Length => 0,
- Msg => (others => ' '),
- Exception_Raised => False,
- Pid => 0,
- Num_Tracebacks => 0,
- Tracebacks => (others => TBE.Null_TB_Entry));
+ Id => null,
+ Machine_Occurrence => System.Null_Address,
+ Msg_Length => 0,
+ Msg => (others => ' '),
+ Exception_Raised => False,
+ Pid => 0,
+ Num_Tracebacks => 0,
+ Tracebacks => (others => TBE.Null_TB_Entry));
end Ada.Exceptions;
+++ /dev/null
-------------------------------------------------------------------------------
--- --
--- GNAT COMPILER COMPONENTS --
--- --
--- A D A . E X C E P T I O N S . E X C E P T I O N _ P R O P A G A T I O N --
--- --
--- B o d y --
--- --
--- Copyright (C) 1992-2016, 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- --
--- ware Foundation; either version 3, or (at your option) any later ver- --
--- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
--- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
--- or FITNESS FOR A PARTICULAR PURPOSE. --
--- --
--- As a special exception under Section 7 of GPL version 3, you are granted --
--- additional permissions described in the GCC Runtime Library Exception, --
--- version 3.1, as published by the Free Software Foundation. --
--- --
--- You should have received a copy of the GNU General Public License and --
--- a copy of the GCC Runtime Library Exception along with this program; --
--- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
--- <http://www.gnu.org/licenses/>. --
--- --
--- GNAT was originally developed by the GNAT team at New York University. --
--- Extensive contributions were provided by Ada Core Technologies Inc. --
--- --
-------------------------------------------------------------------------------
-
--- This is the version using the GCC EH mechanism
-
-with Ada.Unchecked_Conversion;
-with Ada.Unchecked_Deallocation;
-
-with System.Storage_Elements; use System.Storage_Elements;
-with System.Exceptions.Machine; use System.Exceptions.Machine;
-
-separate (Ada.Exceptions)
-package body Exception_Propagation is
-
- use Exception_Traces;
-
- Foreign_Exception : aliased System.Standard_Library.Exception_Data;
- pragma Import (Ada, Foreign_Exception,
- "system__exceptions__foreign_exception");
- -- Id for foreign exceptions
-
- --------------------------------------------------------------
- -- GNAT Specific Entities To Deal With The GCC EH Circuitry --
- --------------------------------------------------------------
-
- procedure GNAT_GCC_Exception_Cleanup
- (Reason : Unwind_Reason_Code;
- Excep : not null GNAT_GCC_Exception_Access);
- pragma Convention (C, GNAT_GCC_Exception_Cleanup);
- -- Procedure called when a GNAT GCC exception is free.
-
- procedure Propagate_GCC_Exception
- (GCC_Exception : not null GCC_Exception_Access);
- pragma No_Return (Propagate_GCC_Exception);
- -- Propagate a GCC exception
-
- procedure Reraise_GCC_Exception
- (GCC_Exception : not null GCC_Exception_Access);
- pragma No_Return (Reraise_GCC_Exception);
- pragma Export (C, Reraise_GCC_Exception, "__gnat_reraise_zcx");
- -- Called to implement raise without exception, ie reraise. Called
- -- directly from gigi.
-
- function Setup_Current_Excep
- (GCC_Exception : not null GCC_Exception_Access) return EOA;
- pragma Export (C, Setup_Current_Excep, "__gnat_setup_current_excep");
- -- Write Get_Current_Excep.all from GCC_Exception. Called by the
- -- personality routine.
-
- procedure Unhandled_Except_Handler
- (GCC_Exception : not null GCC_Exception_Access);
- pragma No_Return (Unhandled_Except_Handler);
- pragma Export (C, Unhandled_Except_Handler,
- "__gnat_unhandled_except_handler");
- -- Called for handle unhandled exceptions, ie the last chance handler
- -- on platforms (such as SEH) that never returns after throwing an
- -- exception. Called directly by gigi.
-
- function CleanupUnwind_Handler
- (UW_Version : Integer;
- UW_Phases : Unwind_Action;
- UW_Eclass : Exception_Class;
- UW_Exception : not null GCC_Exception_Access;
- UW_Context : System.Address;
- UW_Argument : System.Address) return Unwind_Reason_Code;
- pragma Import (C, CleanupUnwind_Handler,
- "__gnat_cleanupunwind_handler");
- -- Hook called at each step of the forced unwinding we perform to trigger
- -- cleanups found during the propagation of an unhandled exception.
-
- -- GCC runtime functions used. These are C non-void functions, actually,
- -- but we ignore the return values. See raise.c as to why we are using
- -- __gnat stubs for these.
-
- procedure Unwind_RaiseException
- (UW_Exception : not null GCC_Exception_Access);
- pragma Import (C, Unwind_RaiseException, "__gnat_Unwind_RaiseException");
-
- procedure Unwind_ForcedUnwind
- (UW_Exception : not null GCC_Exception_Access;
- UW_Handler : System.Address;
- UW_Argument : System.Address);
- pragma Import (C, Unwind_ForcedUnwind, "__gnat_Unwind_ForcedUnwind");
-
- procedure Set_Exception_Parameter
- (Excep : EOA;
- GCC_Exception : not null GCC_Exception_Access);
- pragma Export
- (C, Set_Exception_Parameter, "__gnat_set_exception_parameter");
- -- Called inserted by gigi to set the exception choice parameter from the
- -- gcc occurrence.
-
- procedure Set_Foreign_Occurrence (Excep : EOA; Mo : System.Address);
- -- Utility routine to initialize occurrence Excep from a foreign exception
- -- whose machine occurrence is Mo. The message is empty, the backtrace
- -- is empty too and the exception identity is Foreign_Exception.
-
- -- Hooks called when entering/leaving an exception handler for a given
- -- occurrence, aimed at handling the stack of active occurrences. The
- -- calls are generated by gigi in tree_transform/N_Exception_Handler.
-
- procedure Begin_Handler (GCC_Exception : not null GCC_Exception_Access);
- pragma Export (C, Begin_Handler, "__gnat_begin_handler");
-
- procedure End_Handler (GCC_Exception : GCC_Exception_Access);
- pragma Export (C, End_Handler, "__gnat_end_handler");
-
- --------------------------------------------------------------------
- -- Accessors to Basic Components of a GNAT Exception Data Pointer --
- --------------------------------------------------------------------
-
- -- As of today, these are only used by the C implementation of the GCC
- -- propagation personality routine to avoid having to rely on a C
- -- counterpart of the whole exception_data structure, which is both
- -- painful and error prone. These subprograms could be moved to a more
- -- widely visible location if need be.
-
- function Is_Handled_By_Others (E : Exception_Data_Ptr) return Boolean;
- pragma Export (C, Is_Handled_By_Others, "__gnat_is_handled_by_others");
- pragma Warnings (Off, Is_Handled_By_Others);
-
- function Language_For (E : Exception_Data_Ptr) return Character;
- pragma Export (C, Language_For, "__gnat_language_for");
-
- function Foreign_Data_For (E : Exception_Data_Ptr) return Address;
- pragma Export (C, Foreign_Data_For, "__gnat_foreign_data_for");
-
- function EID_For (GNAT_Exception : not null GNAT_GCC_Exception_Access)
- return Exception_Id;
- pragma Export (C, EID_For, "__gnat_eid_for");
-
- ---------------------------------------------------------------------------
- -- Objects to materialize "others" and "all others" in the GCC EH tables --
- ---------------------------------------------------------------------------
-
- -- Currently, these only have their address taken and compared so there is
- -- no real point having whole exception data blocks allocated. Note that
- -- there are corresponding declarations in gigi (trans.c) which must be
- -- kept properly synchronized.
-
- Others_Value : constant Character := 'O';
- pragma Export (C, Others_Value, "__gnat_others_value");
-
- All_Others_Value : constant Character := 'A';
- pragma Export (C, All_Others_Value, "__gnat_all_others_value");
-
- Unhandled_Others_Value : constant Character := 'U';
- pragma Export (C, Unhandled_Others_Value, "__gnat_unhandled_others_value");
- -- Special choice (emitted by gigi) to catch and notify unhandled
- -- exceptions on targets which always handle exceptions (such as SEH).
- -- The handler will simply call Unhandled_Except_Handler.
-
- -------------------------
- -- Allocate_Occurrence --
- -------------------------
-
- function Allocate_Occurrence return EOA is
- Res : GNAT_GCC_Exception_Access;
-
- begin
- Res := New_Occurrence;
- Res.Header.Cleanup := GNAT_GCC_Exception_Cleanup'Address;
- Res.Occurrence.Machine_Occurrence := Res.all'Address;
-
- return Res.Occurrence'Access;
- end Allocate_Occurrence;
-
- --------------------------------
- -- GNAT_GCC_Exception_Cleanup --
- --------------------------------
-
- procedure GNAT_GCC_Exception_Cleanup
- (Reason : Unwind_Reason_Code;
- Excep : not null GNAT_GCC_Exception_Access)
- is
- pragma Unreferenced (Reason);
-
- procedure Free is new Unchecked_Deallocation
- (GNAT_GCC_Exception, GNAT_GCC_Exception_Access);
-
- Copy : GNAT_GCC_Exception_Access := Excep;
-
- begin
- -- Simply free the memory
-
- Free (Copy);
- end GNAT_GCC_Exception_Cleanup;
-
- ----------------------------
- -- Set_Foreign_Occurrence --
- ----------------------------
-
- procedure Set_Foreign_Occurrence (Excep : EOA; Mo : System.Address) is
- begin
- Excep.all := (
- Id => Foreign_Exception'Access,
- Machine_Occurrence => Mo,
- Msg => <>,
- Msg_Length => 0,
- Exception_Raised => True,
- Pid => Local_Partition_ID,
- Num_Tracebacks => 0,
- Tracebacks => <>);
- end Set_Foreign_Occurrence;
-
- -------------------------
- -- Setup_Current_Excep --
- -------------------------
-
- function Setup_Current_Excep
- (GCC_Exception : not null GCC_Exception_Access) return EOA
- is
- Excep : constant EOA := Get_Current_Excep.all;
-
- begin
- -- Setup the exception occurrence
-
- if GCC_Exception.Class = GNAT_Exception_Class then
-
- -- From the GCC exception
-
- declare
- GNAT_Occurrence : constant GNAT_GCC_Exception_Access :=
- To_GNAT_GCC_Exception (GCC_Exception);
- begin
- Excep.all := GNAT_Occurrence.Occurrence;
- return GNAT_Occurrence.Occurrence'Access;
- end;
-
- else
- -- A default one
-
- Set_Foreign_Occurrence (Excep, GCC_Exception.all'Address);
-
- return Excep;
- end if;
- end Setup_Current_Excep;
-
- -------------------
- -- Begin_Handler --
- -------------------
-
- procedure Begin_Handler (GCC_Exception : not null GCC_Exception_Access) is
- pragma Unreferenced (GCC_Exception);
- begin
- null;
- end Begin_Handler;
-
- -----------------
- -- End_Handler --
- -----------------
-
- procedure End_Handler (GCC_Exception : GCC_Exception_Access) is
- begin
- if GCC_Exception /= null then
-
- -- The exception might have been reraised, in this case the cleanup
- -- mustn't be called.
-
- Unwind_DeleteException (GCC_Exception);
- end if;
- end End_Handler;
-
- -----------------------------
- -- Reraise_GCC_Exception --
- -----------------------------
-
- procedure Reraise_GCC_Exception
- (GCC_Exception : not null GCC_Exception_Access)
- is
- begin
- -- Simply propagate it
-
- Propagate_GCC_Exception (GCC_Exception);
- end Reraise_GCC_Exception;
-
- -----------------------------
- -- Propagate_GCC_Exception --
- -----------------------------
-
- -- Call Unwind_RaiseException to actually throw, taking care of handling
- -- the two phase scheme it implements.
-
- procedure Propagate_GCC_Exception
- (GCC_Exception : not null GCC_Exception_Access)
- is
- Excep : EOA;
-
- begin
- -- Perform a standard raise first. If a regular handler is found, it
- -- will be entered after all the intermediate cleanups have run. If
- -- there is no regular handler, it will return.
-
- Unwind_RaiseException (GCC_Exception);
-
- -- If we get here we know the exception is not handled, as otherwise
- -- Unwind_RaiseException arranges for the handler to be entered. Take
- -- the necessary steps to enable the debugger to gain control while the
- -- stack is still intact.
-
- Excep := Setup_Current_Excep (GCC_Exception);
- Notify_Unhandled_Exception (Excep);
-
- -- Now, un a forced unwind to trigger cleanups. Control should not
- -- resume there, if there are cleanups and in any cases as the
- -- unwinding hook calls Unhandled_Exception_Terminate when end of
- -- stack is reached.
-
- Unwind_ForcedUnwind
- (GCC_Exception,
- CleanupUnwind_Handler'Address,
- System.Null_Address);
-
- -- We get here in case of error. The debugger has been notified before
- -- the second step above.
-
- Unhandled_Except_Handler (GCC_Exception);
- end Propagate_GCC_Exception;
-
- -------------------------
- -- Propagate_Exception --
- -------------------------
-
- procedure Propagate_Exception (Excep : EOA) is
- begin
- Propagate_GCC_Exception (To_GCC_Exception (Excep.Machine_Occurrence));
- end Propagate_Exception;
-
- -----------------------------
- -- Set_Exception_Parameter --
- -----------------------------
-
- procedure Set_Exception_Parameter
- (Excep : EOA;
- GCC_Exception : not null GCC_Exception_Access)
- is
- begin
- -- Setup the exception occurrence
-
- if GCC_Exception.Class = GNAT_Exception_Class then
-
- -- From the GCC exception
-
- declare
- GNAT_Occurrence : constant GNAT_GCC_Exception_Access :=
- To_GNAT_GCC_Exception (GCC_Exception);
- begin
- Save_Occurrence (Excep.all, GNAT_Occurrence.Occurrence);
- end;
-
- else
- -- A default one
-
- Set_Foreign_Occurrence (Excep, GCC_Exception.all'Address);
- end if;
- end Set_Exception_Parameter;
-
- ------------------------------
- -- Unhandled_Except_Handler --
- ------------------------------
-
- procedure Unhandled_Except_Handler
- (GCC_Exception : not null GCC_Exception_Access)
- is
- Excep : EOA;
- begin
- Excep := Setup_Current_Excep (GCC_Exception);
- Unhandled_Exception_Terminate (Excep);
- end Unhandled_Except_Handler;
-
- -------------
- -- EID_For --
- -------------
-
- function EID_For
- (GNAT_Exception : not null GNAT_GCC_Exception_Access) return Exception_Id
- is
- begin
- return GNAT_Exception.Occurrence.Id;
- end EID_For;
-
- ----------------------
- -- Foreign_Data_For --
- ----------------------
-
- function Foreign_Data_For
- (E : SSL.Exception_Data_Ptr) return Address
- is
- begin
- return E.Foreign_Data;
- end Foreign_Data_For;
-
- --------------------------
- -- Is_Handled_By_Others --
- --------------------------
-
- function Is_Handled_By_Others (E : SSL.Exception_Data_Ptr) return Boolean is
- begin
- return not E.all.Not_Handled_By_Others;
- end Is_Handled_By_Others;
-
- ------------------
- -- Language_For --
- ------------------
-
- function Language_For (E : SSL.Exception_Data_Ptr) return Character is
- begin
- return E.all.Lang;
- end Language_For;
-
-end Exception_Propagation;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, 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- --
-- --
------------------------------------------------------------------------------
--- This is the default version, using the __builtin_setjmp/longjmp EH
--- mechanism.
+-- This is the version using the GCC EH mechanism
with Ada.Unchecked_Conversion;
+with Ada.Unchecked_Deallocation;
+
+with System.Storage_Elements; use System.Storage_Elements;
+with System.Exceptions.Machine; use System.Exceptions.Machine;
separate (Ada.Exceptions)
package body Exception_Propagation is
- -- Common binding to __builtin_longjmp for sjlj variants.
+ use Exception_Traces;
+
+ Foreign_Exception : aliased System.Standard_Library.Exception_Data;
+ pragma Import (Ada, Foreign_Exception,
+ "system__exceptions__foreign_exception");
+ -- Id for foreign exceptions
+
+ --------------------------------------------------------------
+ -- GNAT Specific Entities To Deal With The GCC EH Circuitry --
+ --------------------------------------------------------------
+
+ procedure GNAT_GCC_Exception_Cleanup
+ (Reason : Unwind_Reason_Code;
+ Excep : not null GNAT_GCC_Exception_Access);
+ pragma Convention (C, GNAT_GCC_Exception_Cleanup);
+ -- Procedure called when a GNAT GCC exception is free.
+
+ procedure Propagate_GCC_Exception
+ (GCC_Exception : not null GCC_Exception_Access);
+ pragma No_Return (Propagate_GCC_Exception);
+ -- Propagate a GCC exception
+
+ procedure Reraise_GCC_Exception
+ (GCC_Exception : not null GCC_Exception_Access);
+ pragma No_Return (Reraise_GCC_Exception);
+ pragma Export (C, Reraise_GCC_Exception, "__gnat_reraise_zcx");
+ -- Called to implement raise without exception, ie reraise. Called
+ -- directly from gigi.
+
+ function Setup_Current_Excep
+ (GCC_Exception : not null GCC_Exception_Access) return EOA;
+ pragma Export (C, Setup_Current_Excep, "__gnat_setup_current_excep");
+ -- Write Get_Current_Excep.all from GCC_Exception. Called by the
+ -- personality routine.
+
+ procedure Unhandled_Except_Handler
+ (GCC_Exception : not null GCC_Exception_Access);
+ pragma No_Return (Unhandled_Except_Handler);
+ pragma Export (C, Unhandled_Except_Handler,
+ "__gnat_unhandled_except_handler");
+ -- Called for handle unhandled exceptions, ie the last chance handler
+ -- on platforms (such as SEH) that never returns after throwing an
+ -- exception. Called directly by gigi.
+
+ function CleanupUnwind_Handler
+ (UW_Version : Integer;
+ UW_Phases : Unwind_Action;
+ UW_Eclass : Exception_Class;
+ UW_Exception : not null GCC_Exception_Access;
+ UW_Context : System.Address;
+ UW_Argument : System.Address) return Unwind_Reason_Code;
+ pragma Import (C, CleanupUnwind_Handler,
+ "__gnat_cleanupunwind_handler");
+ -- Hook called at each step of the forced unwinding we perform to trigger
+ -- cleanups found during the propagation of an unhandled exception.
+
+ -- GCC runtime functions used. These are C non-void functions, actually,
+ -- but we ignore the return values. See raise.c as to why we are using
+ -- __gnat stubs for these.
+
+ procedure Unwind_RaiseException
+ (UW_Exception : not null GCC_Exception_Access);
+ pragma Import (C, Unwind_RaiseException, "__gnat_Unwind_RaiseException");
+
+ procedure Unwind_ForcedUnwind
+ (UW_Exception : not null GCC_Exception_Access;
+ UW_Handler : System.Address;
+ UW_Argument : System.Address);
+ pragma Import (C, Unwind_ForcedUnwind, "__gnat_Unwind_ForcedUnwind");
+
+ procedure Set_Exception_Parameter
+ (Excep : EOA;
+ GCC_Exception : not null GCC_Exception_Access);
+ pragma Export
+ (C, Set_Exception_Parameter, "__gnat_set_exception_parameter");
+ -- Called inserted by gigi to set the exception choice parameter from the
+ -- gcc occurrence.
+
+ procedure Set_Foreign_Occurrence (Excep : EOA; Mo : System.Address);
+ -- Utility routine to initialize occurrence Excep from a foreign exception
+ -- whose machine occurrence is Mo. The message is empty, the backtrace
+ -- is empty too and the exception identity is Foreign_Exception.
+
+ -- Hooks called when entering/leaving an exception handler for a given
+ -- occurrence, aimed at handling the stack of active occurrences. The
+ -- calls are generated by gigi in tree_transform/N_Exception_Handler.
+
+ procedure Begin_Handler (GCC_Exception : not null GCC_Exception_Access);
+ pragma Export (C, Begin_Handler, "__gnat_begin_handler");
+
+ procedure End_Handler (GCC_Exception : GCC_Exception_Access);
+ pragma Export (C, End_Handler, "__gnat_end_handler");
+
+ --------------------------------------------------------------------
+ -- Accessors to Basic Components of a GNAT Exception Data Pointer --
+ --------------------------------------------------------------------
+
+ -- As of today, these are only used by the C implementation of the GCC
+ -- propagation personality routine to avoid having to rely on a C
+ -- counterpart of the whole exception_data structure, which is both
+ -- painful and error prone. These subprograms could be moved to a more
+ -- widely visible location if need be.
+
+ function Is_Handled_By_Others (E : Exception_Data_Ptr) return Boolean;
+ pragma Export (C, Is_Handled_By_Others, "__gnat_is_handled_by_others");
+ pragma Warnings (Off, Is_Handled_By_Others);
+
+ function Language_For (E : Exception_Data_Ptr) return Character;
+ pragma Export (C, Language_For, "__gnat_language_for");
+
+ function Foreign_Data_For (E : Exception_Data_Ptr) return Address;
+ pragma Export (C, Foreign_Data_For, "__gnat_foreign_data_for");
+
+ function EID_For (GNAT_Exception : not null GNAT_GCC_Exception_Access)
+ return Exception_Id;
+ pragma Export (C, EID_For, "__gnat_eid_for");
+
+ ---------------------------------------------------------------------------
+ -- Objects to materialize "others" and "all others" in the GCC EH tables --
+ ---------------------------------------------------------------------------
- procedure builtin_longjmp (buffer : System.Address; Flag : Integer);
- pragma No_Return (builtin_longjmp);
- pragma Import (Intrinsic, builtin_longjmp, "__builtin_longjmp");
+ -- Currently, these only have their address taken and compared so there is
+ -- no real point having whole exception data blocks allocated. Note that
+ -- there are corresponding declarations in gigi (trans.c) which must be
+ -- kept properly synchronized.
- procedure Propagate_Continue (E : Exception_Id);
- pragma No_Return (Propagate_Continue);
- pragma Export (C, Propagate_Continue, "__gnat_raise_nodefer_with_msg");
- -- A call to this procedure is inserted automatically by GIGI, in order
- -- to continue the propagation when the exception was not handled.
- -- The linkage name is historical.
+ Others_Value : constant Character := 'O';
+ pragma Export (C, Others_Value, "__gnat_others_value");
+
+ All_Others_Value : constant Character := 'A';
+ pragma Export (C, All_Others_Value, "__gnat_all_others_value");
+
+ Unhandled_Others_Value : constant Character := 'U';
+ pragma Export (C, Unhandled_Others_Value, "__gnat_unhandled_others_value");
+ -- Special choice (emitted by gigi) to catch and notify unhandled
+ -- exceptions on targets which always handle exceptions (such as SEH).
+ -- The handler will simply call Unhandled_Except_Handler.
-------------------------
-- Allocate_Occurrence --
-------------------------
function Allocate_Occurrence return EOA is
+ Res : GNAT_GCC_Exception_Access;
+
begin
- return Get_Current_Excep.all;
+ Res := New_Occurrence;
+ Res.Header.Cleanup := GNAT_GCC_Exception_Cleanup'Address;
+ Res.Occurrence.Machine_Occurrence := Res.all'Address;
+
+ return Res.Occurrence'Access;
end Allocate_Occurrence;
+ --------------------------------
+ -- GNAT_GCC_Exception_Cleanup --
+ --------------------------------
+
+ procedure GNAT_GCC_Exception_Cleanup
+ (Reason : Unwind_Reason_Code;
+ Excep : not null GNAT_GCC_Exception_Access)
+ is
+ pragma Unreferenced (Reason);
+
+ procedure Free is new Unchecked_Deallocation
+ (GNAT_GCC_Exception, GNAT_GCC_Exception_Access);
+
+ Copy : GNAT_GCC_Exception_Access := Excep;
+
+ begin
+ -- Simply free the memory
+
+ Free (Copy);
+ end GNAT_GCC_Exception_Cleanup;
+
+ ----------------------------
+ -- Set_Foreign_Occurrence --
+ ----------------------------
+
+ procedure Set_Foreign_Occurrence (Excep : EOA; Mo : System.Address) is
+ begin
+ Excep.all := (
+ Id => Foreign_Exception'Access,
+ Machine_Occurrence => Mo,
+ Msg => <>,
+ Msg_Length => 0,
+ Exception_Raised => True,
+ Pid => Local_Partition_ID,
+ Num_Tracebacks => 0,
+ Tracebacks => <>);
+ end Set_Foreign_Occurrence;
+
+ -------------------------
+ -- Setup_Current_Excep --
+ -------------------------
+
+ function Setup_Current_Excep
+ (GCC_Exception : not null GCC_Exception_Access) return EOA
+ is
+ Excep : constant EOA := Get_Current_Excep.all;
+
+ begin
+ -- Setup the exception occurrence
+
+ if GCC_Exception.Class = GNAT_Exception_Class then
+
+ -- From the GCC exception
+
+ declare
+ GNAT_Occurrence : constant GNAT_GCC_Exception_Access :=
+ To_GNAT_GCC_Exception (GCC_Exception);
+ begin
+ Excep.all := GNAT_Occurrence.Occurrence;
+ return GNAT_Occurrence.Occurrence'Access;
+ end;
+
+ else
+ -- A default one
+
+ Set_Foreign_Occurrence (Excep, GCC_Exception.all'Address);
+
+ return Excep;
+ end if;
+ end Setup_Current_Excep;
+
+ -------------------
+ -- Begin_Handler --
+ -------------------
+
+ procedure Begin_Handler (GCC_Exception : not null GCC_Exception_Access) is
+ pragma Unreferenced (GCC_Exception);
+ begin
+ null;
+ end Begin_Handler;
+
+ -----------------
+ -- End_Handler --
+ -----------------
+
+ procedure End_Handler (GCC_Exception : GCC_Exception_Access) is
+ begin
+ if GCC_Exception /= null then
+
+ -- The exception might have been reraised, in this case the cleanup
+ -- mustn't be called.
+
+ Unwind_DeleteException (GCC_Exception);
+ end if;
+ end End_Handler;
+
+ -----------------------------
+ -- Reraise_GCC_Exception --
+ -----------------------------
+
+ procedure Reraise_GCC_Exception
+ (GCC_Exception : not null GCC_Exception_Access)
+ is
+ begin
+ -- Simply propagate it
+
+ Propagate_GCC_Exception (GCC_Exception);
+ end Reraise_GCC_Exception;
+
+ -----------------------------
+ -- Propagate_GCC_Exception --
+ -----------------------------
+
+ -- Call Unwind_RaiseException to actually throw, taking care of handling
+ -- the two phase scheme it implements.
+
+ procedure Propagate_GCC_Exception
+ (GCC_Exception : not null GCC_Exception_Access)
+ is
+ Excep : EOA;
+
+ begin
+ -- Perform a standard raise first. If a regular handler is found, it
+ -- will be entered after all the intermediate cleanups have run. If
+ -- there is no regular handler, it will return.
+
+ Unwind_RaiseException (GCC_Exception);
+
+ -- If we get here we know the exception is not handled, as otherwise
+ -- Unwind_RaiseException arranges for the handler to be entered. Take
+ -- the necessary steps to enable the debugger to gain control while the
+ -- stack is still intact.
+
+ Excep := Setup_Current_Excep (GCC_Exception);
+ Notify_Unhandled_Exception (Excep);
+
+ -- Now, un a forced unwind to trigger cleanups. Control should not
+ -- resume there, if there are cleanups and in any cases as the
+ -- unwinding hook calls Unhandled_Exception_Terminate when end of
+ -- stack is reached.
+
+ Unwind_ForcedUnwind
+ (GCC_Exception,
+ CleanupUnwind_Handler'Address,
+ System.Null_Address);
+
+ -- We get here in case of error. The debugger has been notified before
+ -- the second step above.
+
+ Unhandled_Except_Handler (GCC_Exception);
+ end Propagate_GCC_Exception;
+
-------------------------
-- Propagate_Exception --
-------------------------
procedure Propagate_Exception (Excep : EOA) is
- Jumpbuf_Ptr : constant Address := Get_Jmpbuf_Address.all;
+ begin
+ Propagate_GCC_Exception (To_GCC_Exception (Excep.Machine_Occurrence));
+ end Propagate_Exception;
+
+ -----------------------------
+ -- Set_Exception_Parameter --
+ -----------------------------
+ procedure Set_Exception_Parameter
+ (Excep : EOA;
+ GCC_Exception : not null GCC_Exception_Access)
+ is
begin
- -- If the jump buffer pointer is non-null, transfer control using
- -- it. Otherwise announce an unhandled exception (note that this
- -- means that we have no finalizations to do other than at the outer
- -- level). Perform the necessary notification tasks in both cases.
+ -- Setup the exception occurrence
+
+ if GCC_Exception.Class = GNAT_Exception_Class then
- if Jumpbuf_Ptr /= Null_Address then
- if not Excep.Exception_Raised then
- Excep.Exception_Raised := True;
- Exception_Traces.Notify_Handled_Exception (Excep);
- end if;
+ -- From the GCC exception
- builtin_longjmp (Jumpbuf_Ptr, 1);
+ declare
+ GNAT_Occurrence : constant GNAT_GCC_Exception_Access :=
+ To_GNAT_GCC_Exception (GCC_Exception);
+ begin
+ Save_Occurrence (Excep.all, GNAT_Occurrence.Occurrence);
+ end;
else
- Exception_Traces.Notify_Unhandled_Exception (Excep);
- Exception_Traces.Unhandled_Exception_Terminate (Excep);
+ -- A default one
+
+ Set_Foreign_Occurrence (Excep, GCC_Exception.all'Address);
end if;
- end Propagate_Exception;
+ end Set_Exception_Parameter;
+
+ ------------------------------
+ -- Unhandled_Except_Handler --
+ ------------------------------
+
+ procedure Unhandled_Except_Handler
+ (GCC_Exception : not null GCC_Exception_Access)
+ is
+ Excep : EOA;
+ begin
+ Excep := Setup_Current_Excep (GCC_Exception);
+ Unhandled_Exception_Terminate (Excep);
+ end Unhandled_Except_Handler;
+
+ -------------
+ -- EID_For --
+ -------------
+
+ function EID_For
+ (GNAT_Exception : not null GNAT_GCC_Exception_Access) return Exception_Id
+ is
+ begin
+ return GNAT_Exception.Occurrence.Id;
+ end EID_For;
+
+ ----------------------
+ -- Foreign_Data_For --
+ ----------------------
+
+ function Foreign_Data_For
+ (E : SSL.Exception_Data_Ptr) return Address
+ is
+ begin
+ return E.Foreign_Data;
+ end Foreign_Data_For;
+
+ --------------------------
+ -- Is_Handled_By_Others --
+ --------------------------
+
+ function Is_Handled_By_Others (E : SSL.Exception_Data_Ptr) return Boolean is
+ begin
+ return not E.all.Not_Handled_By_Others;
+ end Is_Handled_By_Others;
- ------------------------
- -- Propagate_Continue --
- ------------------------
+ ------------------
+ -- Language_For --
+ ------------------
- procedure Propagate_Continue (E : Exception_Id) is
- pragma Unreferenced (E);
+ function Language_For (E : SSL.Exception_Data_Ptr) return Character is
begin
- Propagate_Exception (Get_Current_Excep.all);
- end Propagate_Continue;
+ return E.all.Lang;
+ end Language_For;
end Exception_Propagation;
-- System.Storage_Elements.To_Address
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
- -- Perform object declaration-specific expansion
+ -- Perform object-declaration-specific expansion
procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
-- Perform name evaluation for a renamed object
Qualify_Entity_Names (N);
-- Replace occurrences of System'To_Address by calls to
- -- System.Storage_Elements.To_Address
+ -- System.Storage_Elements.To_Address.
when N_Attribute_Reference =>
Expand_SPARK_N_Attribute_Reference (N);
ada-warn = $(ADA_CFLAGS) $(filter-out -pedantic, $(STRICT_WARN))
# Unresolved warnings in specific files.
ada/adaint.o-warn = -Wno-error
+# For unwind-pe.h
+CFLAGS-ada/raise-gcc.o += -I$(srcdir)/../libgcc -Iinclude
ada/%.o: ada/gcc-interface/%.c
$(COMPILE) $<
# Object files for gnat1 from C sources.
GNAT1_C_OBJS = ada/adadecode.o ada/adaint.o ada/argv.o ada/cio.o \
ada/cstreams.o ada/env.o ada/init.o ada/initialize.o ada/raise.o \
+ ada/raise-gcc.o \
ada/seh_init.o ada/targext.o ada/cuintp.o ada/decl.o ada/rtfinal.o \
ada/rtinit.o ada/misc.o ada/utils.o ada/utils2.o ada/trans.o ada/targtyps.o
ada/a-chlat1.o \
ada/a-elchha.o \
ada/a-except.o \
+ ada/a-exctra.o \
ada/a-ioexce.o \
ada/ada.o \
ada/spark_xrefs.o \
ada/rident.o \
ada/rtsfind.o \
ada/s-addope.o \
+ ada/s-addima.o \
ada/s-assert.o \
ada/s-bitops.o \
ada/s-carun8.o \
ada/s-excdeb.o \
ada/s-except.o \
ada/s-exctab.o \
+ ada/s-excmac.o \
ada/s-htable.o \
ada/s-imenne.o \
ada/s-imgenu.o \
+ ada/s-imgint.o \
ada/s-mastop.o \
ada/s-memory.o \
ada/s-os_lib.o \
ada/s-strhas.o \
ada/s-string.o \
ada/s-strops.o \
+ ada/s-traceb.o \
ada/s-traent.o \
+ ada/s-trasym.o \
ada/s-unstyp.o \
ada/s-utf_32.o \
ada/s-valint.o \
ada/s-wchcnv.o \
ada/s-wchcon.o \
ada/s-wchjis.o \
+ ada/s-wchstw.o \
ada/scans.o \
ada/scil_ll.o \
ada/scn.o \
ada/osint.o \
ada/output.o \
ada/raise.o \
+ ada/raise-gcc.o \
ada/restrict.o \
ada/rident.o \
ada/rtfinal.o \
ada/s-crtl.o \
ada/s-excdeb.o \
ada/s-except.o \
+ ada/s-excmac.o \
ada/s-exctab.o \
ada/s-htable.o \
ada/s-imenne.o \
ada/s-imgenu.o \
+ ada/s-imgint.o \
ada/s-mastop.o \
ada/s-memory.o \
ada/s-os_lib.o \
ada/s-string.o \
ada/s-strops.o \
ada/s-traent.o \
+ ada/s-traceb.o \
ada/s-unstyp.o \
ada/s-utf_32.o \
ada/s-wchcnv.o \
ada/s-wchcon.o \
ada/s-wchjis.o \
+ ada/s-wchstw.o \
ada/scans.o \
ada/scil_ll.o \
ada/scng.o \
# List of target dependent sources, overridden below as necessary
TARGET_ADA_SRCS =
+# Select the right s-excmac according to exception layout (Itanium or arm)
+host_cpu=$(word 1, $(subst -, ,$(host)))
+EH_MECHANISM=-gcc
+ifeq ($(strip $(filter-out arm%,$(host_cpu))),)
+EH_MECHANISM=-arm
+endif
+
+ada/s-excmac.o: ada/s-excmac.ads ada/s-excmac.adb
+
+ada/s-excmac.ads: $(srcdir)/ada/s-excmac$(EH_MECHANISM).ads
+ $(CP) $< $@
+
+ada/s-excmac.adb: $(srcdir)/ada/s-excmac$(EH_MECHANISM).adb
+ $(CP) $< $@
+
# Needs to be built with CC=gcc
# Since the RTL should be built with the latest compiler, remove the
# stamp target in the parent directory whenever gnat1 is rebuilt
# Special flags - see gcc-interface/Makefile.in for the template.
-ada/a-except.o : ada/a-except.adb ada/a-except.ads
+ada/a-except.o : ada/a-except.adb ada/a-except.ads ada/s-excmac.ads ada/s-excmac.adb
$(CC) -c $(ALL_ADAFLAGS) $(FORCE_DEBUG_ADAFLAGS) -O1 -fno-inline \
$(ADA_INCLUDES) $< $(OUTPUT_OPTION)
@$(ADA_DEPS)
-ada/s-excdeb.o : ada/s-excdeb.adb ada/s-excdeb.ads
+ada/s-excdeb.o : ada/s-excdeb.adb ada/s-excdeb.ads
$(CC) -c $(ALL_ADAFLAGS) $(FORCE_DEBUG_ADAFLAGS) -O0 \
$(ADA_INCLUDES) $< $(OUTPUT_OPTION)
@$(ADA_DEPS)
ifeq ($(EH_MECHANISM),-gcc)
LIBGNAT_TARGET_PAIRS += \
- a-exexpr.adb<a-exexpr-gcc.adb \
- s-excmac.ads<s-excmac-gcc.ads
+ s-excmac.ads<s-excmac-gcc.ads \
+ s-excmac.adb<s-excmac-gcc.adb
EXTRA_LIBGNAT_OBJS+=raise-gcc.o
EXTRA_GNATRTL_NONTASKING_OBJS+=g-cppexc.o s-excmac.o
endif
ifeq ($(EH_MECHANISM),-arm)
LIBGNAT_TARGET_PAIRS += \
- a-exexpr.adb<a-exexpr-gcc.adb \
- s-excmac.ads<s-excmac-arm.ads
+ s-excmac.ads<s-excmac-arm.ads \
+ s-excmac.adb<s-excmac-arm.adb
EXTRA_LIBGNAT_OBJS+=raise-gcc.o
EXTRA_GNATRTL_NONTASKING_OBJS+=g-cppexc.o s-excmac.o
endif
-# Use the Ada 2005 version of Ada.Exceptions by default, unless specified
-# explicitly already. The base files (a-except.ad?) are used only for building
-# the compiler and other basic tools.
-# These base versions lack Ada 2005 additions which would cause bootstrap
-# problems if included in the compiler and other basic tools.
-
-ifeq ($(filter a-except%,$(LIBGNAT_TARGET_PAIRS)),)
- LIBGNAT_TARGET_PAIRS += \
- a-except.ads<a-except-2005.ads \
- a-except.adb<a-except-2005.adb
-endif
-
# Configuration of host tools
# Under linux, host tools need to be linked with -ldl
* *
* C Implementation File *
* *
- * Copyright (C) 1992-2016, Free Software Foundation, Inc. *
+ * Copyright (C) 1992-2017, 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- *
/* Code related to the integration of the GCC mechanism for exception
handling. */
-#ifndef IN_RTS
-#error "RTS unit only"
-#endif
-
#ifndef CERT
#include "tconfig.h"
#include "tsystem.h"
#endif
#include <stdarg.h>
+
+#ifdef __cplusplus
+# include <cstdlib>
+#else
typedef char bool;
# define true 1
# define false 0
+#endif
#include "raise.h"
#include "unwind.h"
+#ifdef __cplusplus
+extern "C" {
+#endif
+
typedef struct _Unwind_Context _Unwind_Context;
typedef struct _Unwind_Exception _Unwind_Exception;
__gnat_Unwind_RaiseException (_Unwind_Exception *);
_Unwind_Reason_Code
-__gnat_Unwind_ForcedUnwind (_Unwind_Exception *, void *, void *);
+__gnat_Unwind_ForcedUnwind (_Unwind_Exception *, _Unwind_Stop_Fn, void *);
extern struct Exception_Occurrence *__gnat_setup_current_excep
(_Unwind_Exception *);
}
static void ATTRIBUTE_PRINTF_2
-db (int db_code, char * msg_format, ...)
+db (int db_code, const char * msg_format, ...)
{
if (db_accepted_codes () & db_code)
{
db (DB_CSITE,
"c_site @ %p (+%p), len = %p, lpad @ %p (+%p)\n",
- (void *)region->base + cs_start, (void *)cs_start, (void *)cs_len,
- (void *)region->lp_base + cs_lp, (void *)cs_lp);
+ (char *)region->base + cs_start, (void *)cs_start, (void *)cs_len,
+ (char *)region->lp_base + cs_lp, (void *)cs_lp);
/* The table is sorted, so if we've passed the IP, stop. */
if (ip < region->base + cs_start)
_Unwind_Reason_Code
__gnat_Unwind_ForcedUnwind (_Unwind_Exception *e ATTRIBUTE_UNUSED,
- void *handler ATTRIBUTE_UNUSED,
+ _Unwind_Stop_Fn handler ATTRIBUTE_UNUSED,
void *argument ATTRIBUTE_UNUSED)
{
#ifdef __USING_SJLJ_EXCEPTIONS__
const int __gnat_unwind_exception_size = sizeof (_Unwind_Exception);
#endif
+
+#ifdef __cplusplus
+}
+#endif
* *
* C Implementation File *
* *
- * Copyright (C) 1992-2012, Free Software Foundation, Inc. *
+ * Copyright (C) 1992-2017, 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- *
extern "C" {
#endif
-/* Wrapper to builtin_longjmp. This is for the compiler eh only, as the sjlj
- runtime library interfaces directly to the intrinsic. We can't yet do
- this for the compiler itself, because this capability relies on changes
- made in April 2008 and we need to preserve the possibility to bootstrap
- with an older base version. */
-
-#if defined (IN_GCC) && !defined (IN_RTS)
-void
-_gnat_builtin_longjmp (void *ptr, int flag ATTRIBUTE_UNUSED)
-{
- __builtin_longjmp (ptr, 1);
-}
-#endif
-
/* When an exception is raised for which no handler exists, the procedure
Ada.Exceptions.Unhandled_Exception is called, which performs the call to
adafinal to complete finalization, and then prints out the error messages
__gnat_os_exit (1);
}
+#ifndef IN_RTS
+int
+__gnat_backtrace (void **array ATTRIBUTE_UNUSED,
+ int size ATTRIBUTE_UNUSED,
+ void *exclude_min ATTRIBUTE_UNUSED,
+ void *exclude_max ATTRIBUTE_UNUSED,
+ int skip_frames ATTRIBUTE_UNUSED)
+{
+ return 0;
+}
+
+void
+__gnat_eh_personality (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_04 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_10 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_19 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_20 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_21 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_30 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_31 (void)
+{
+ abort ();
+}
+
+void
+__gnat_rcheck_32 (void)
+{
+ abort ();
+}
+#endif
#ifdef __cplusplus
}
#endif
if No (E) and then Is_Null_Record_Type (T) then
null;
+ -- Do not generate a predicate check if the initialization expression
+ -- is a type conversion because the conversion has been subjected to
+ -- the same check. This is a small optimization which avoid redundant
+ -- checks.
+
+ elsif Present (E) and then Nkind (E) = N_Type_Conversion then
+ null;
+
else
Insert_After (N,
Make_Predicate_Check (T, New_Occurrence_Of (Id, Loc)));
-- see whether an elaboration check is required.
Is_DIC : Boolean;
- -- Flag set when the subprogram being invoked the procedure generated
+ -- Flag set when the subprogram being invoked is the procedure generated
-- for pragma Default_Initial_Condition.
SPARK_Elab_Errors : Boolean;
end;
end if;
- -- Ada 2012: if target type has predicates, the result requires a
- -- predicate check. If the context is a call to another predicate
- -- check we must prevent infinite recursion.
+ -- Ada 2012: once the type conversion is resolved, check whether the
+ -- operand statisfies the static predicate of the target type.
if Has_Predicates (Target_Typ) then
- if Nkind (Parent (N)) = N_Function_Call
- and then Present (Name (Parent (N)))
- and then (Is_Predicate_Function (Entity (Name (Parent (N))))
- or else
- Is_Predicate_Function_M (Entity (Name (Parent (N)))))
- then
- null;
-
- else
- Apply_Predicate_Check (N, Target_Typ);
- end if;
+ Check_Expression_Against_Static_Predicate (N, Target_Typ);
end if;
-- If at this stage we have a real to integer conversion, make sure that
-- S p e c --
-- (Compiler Version) --
-- --
--- Copyright (C) 1992-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
Always_Compatible_Rep : constant Boolean := True;
Suppress_Standard_Library : constant Boolean := False;
Use_Ada_Main_Program_Name : constant Boolean := False;
- Frontend_Exceptions : constant Boolean := True;
- ZCX_By_Default : constant Boolean := False;
+ Frontend_Exceptions : constant Boolean := False;
+ ZCX_By_Default : constant Boolean := True;
-- Obsolete entries, to be removed eventually (bootstrap issues)
Long_Shifts_Inlined : constant Boolean := True;
Functions_Return_By_DSP : constant Boolean := False;
Support_64_Bit_Divides : constant Boolean := True;
- GCC_ZCX_Support : constant Boolean := False;
+ GCC_ZCX_Support : constant Boolean := True;
end System;
git://gcc.gnu.org / gcc.git / commitdiff