Skip to content

R
riscv-gcc-1
Commit 6cbfce7e by Arnaud Charlet
Options

[multiple changes] 

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.

From-SVN: r247301
parent de3b531c
Showing with 2497 additions and 4099 deletions
gcc/ada/ChangeLog
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,
......
gcc/ada/a-cfdlli.adb
......@@ -497,72 +497,18 @@ is
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;
......@@ -571,36 +517,16 @@ is
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
......@@ -609,7 +535,7 @@ is
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;
......@@ -628,21 +554,21 @@ is
------------------------
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;
......@@ -673,22 +599,25 @@ is
-----------------------
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;
......@@ -708,7 +637,7 @@ is
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;
......@@ -718,18 +647,18 @@ is
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;
......@@ -743,31 +672,33 @@ is
-------------------------
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;
......@@ -788,7 +719,7 @@ is
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;
......@@ -798,13 +729,13 @@ is
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;
......@@ -907,18 +838,18 @@ is
-- 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;
......
gcc/ada/a-cfdlli.ads
......@@ -71,120 +71,59 @@ is
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
......@@ -205,7 +144,7 @@ is
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.
......@@ -218,28 +157,25 @@ is
-- 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;
......@@ -252,40 +188,34 @@ is
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
......@@ -302,7 +232,7 @@ is
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 =>
......@@ -388,12 +318,14 @@ is
-- 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,
......@@ -417,25 +349,35 @@ is
-- 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)
......@@ -468,18 +410,18 @@ is
(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
......@@ -490,26 +432,27 @@ is
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
......@@ -535,7 +478,7 @@ is
-- 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)
......@@ -543,16 +486,16 @@ is
= 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)
......@@ -590,7 +533,7 @@ is
-- 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
......@@ -598,26 +541,26 @@ is
= 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
......@@ -636,9 +579,9 @@ is
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)
......@@ -663,19 +606,19 @@ is
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
......@@ -694,12 +637,23 @@ is
-- 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;
......@@ -715,11 +669,11 @@ is
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
......@@ -741,16 +695,16 @@ is
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)
......@@ -776,11 +730,11 @@ is
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
......@@ -800,9 +754,9 @@ is
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,
......@@ -823,9 +777,9 @@ is
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)
......@@ -849,9 +803,9 @@ is
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)
......@@ -874,8 +828,16 @@ is
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;
......@@ -949,17 +911,17 @@ is
(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)
......@@ -973,25 +935,25 @@ is
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)
......@@ -1021,16 +983,16 @@ is
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)
......@@ -1044,7 +1006,7 @@ is
-- 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)
......@@ -1052,16 +1014,16 @@ is
= 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)
......@@ -1095,16 +1057,16 @@ is
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)
......@@ -1117,45 +1079,45 @@ is
-- 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)
......@@ -1168,10 +1130,10 @@ is
-- 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,
......@@ -1260,18 +1222,18 @@ is
-- 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),
......@@ -1283,12 +1245,12 @@ is
>= 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;
......@@ -1302,18 +1264,18 @@ is
-- 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),
......@@ -1325,42 +1287,42 @@ is
<= 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
......
gcc/ada/a-cofuma.adb
......@@ -38,21 +38,21 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
-- "=" --
---------
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;
......@@ -64,103 +64,185 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
-- 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;
gcc/ada/a-cofuma.ads
......@@ -36,12 +36,8 @@ generic
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,
......@@ -52,100 +48,179 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
-- "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 --
......@@ -153,20 +228,25 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
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
......@@ -193,15 +273,20 @@ 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;
gcc/ada/a-cofuse.adb
......@@ -38,101 +38,107 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
-- "=" --
---------
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;
gcc/ada/a-cofuse.ads
......@@ -34,12 +34,10 @@ private with Ada.Containers.Functional_Base;
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,
......@@ -50,130 +48,154 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
-- "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 --
......@@ -181,20 +203,27 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
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
......@@ -212,15 +241,22 @@ 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;
gcc/ada/a-cofuve.adb
......@@ -34,129 +34,215 @@ 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;
gcc/ada/a-cofuve.ads
......@@ -38,12 +38,8 @@ generic
-- 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.
......@@ -60,178 +56,299 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
-- 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
......@@ -245,22 +362,21 @@ 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;
gcc/ada/a-except-2005.adb deleted 100644 → 0
------------------------------------------------------------------------------
-- --
-- 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;
gcc/ada/a-except-2005.ads deleted 100644 → 0
------------------------------------------------------------------------------
-- --
-- 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;
gcc/ada/a-except.adb
......@@ -6,7 +6,7 @@
-- --
-- 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- --
......@@ -29,8 +29,6 @@
-- --
------------------------------------------------------------------------------
pragma Compiler_Unit_Warning;
pragma Style_Checks (All_Checks);
-- No subprogram ordering check, due to logical grouping
......@@ -39,16 +37,29 @@ pragma Polling (Off);
-- 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 --
......@@ -58,22 +69,47 @@ package body Ada.Exceptions is
-- 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
......@@ -88,22 +124,21 @@ package body Ada.Exceptions 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 --
......@@ -176,14 +211,29 @@ package body Ada.Exceptions is
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
----------------------------------
......@@ -201,18 +251,32 @@ package body Ada.Exceptions 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");
......@@ -222,45 +286,41 @@ package body Ada.Exceptions is
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
......@@ -272,12 +332,9 @@ package body Ada.Exceptions is
(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
......@@ -294,10 +351,10 @@ package body Ada.Exceptions is
-- 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
-- | | | | |
-- +--+ +--+ +---+ | +---+
......@@ -308,23 +365,24 @@ package body Ada.Exceptions is
-- | | | |
-- | | | 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 --
......@@ -334,91 +392,88 @@ package body Ada.Exceptions is
-- 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
......@@ -500,6 +555,15 @@ package body Ada.Exceptions is
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).
......@@ -530,8 +594,8 @@ package body Ada.Exceptions is
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);
......@@ -542,124 +606,10 @@ package body Ada.Exceptions is
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 --
......@@ -727,6 +677,33 @@ package body Ada.Exceptions is
-- 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 --
-------------------
......@@ -752,9 +729,9 @@ package body Ada.Exceptions is
(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;
......@@ -784,9 +761,9 @@ package body Ada.Exceptions is
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;
--------------------
......@@ -797,9 +774,9 @@ package body Ada.Exceptions is
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
......@@ -839,15 +816,49 @@ package body Ada.Exceptions 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 --
......@@ -857,59 +868,13 @@ package body Ada.Exceptions is
-- 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;
--------------------------------
......@@ -917,41 +882,60 @@ package body Ada.Exceptions is
--------------------------------
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 --
......@@ -961,8 +945,7 @@ package body Ada.Exceptions is
(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)
......@@ -972,9 +955,7 @@ package body Ada.Exceptions is
-- 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;
----------------------------
......@@ -985,11 +966,16 @@ package body Ada.Exceptions is
(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;
------------------------------
......@@ -1000,13 +986,14 @@ package body Ada.Exceptions is
(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;
-------------------------------------
......@@ -1019,11 +1006,13 @@ package body Ada.Exceptions 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);
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
......@@ -1053,6 +1042,39 @@ package body Ada.Exceptions is
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 --
-------------------------------
......@@ -1061,11 +1083,9 @@ package body Ada.Exceptions is
(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;
-------------------------
......@@ -1077,8 +1097,7 @@ package body Ada.Exceptions is
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;
-----------------------------
......@@ -1092,7 +1111,7 @@ package body Ada.Exceptions is
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;
-------------------------
......@@ -1104,8 +1123,7 @@ package body Ada.Exceptions is
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;
-----------------------------
......@@ -1119,7 +1137,7 @@ package body Ada.Exceptions is
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;
---------------------------------
......@@ -1130,13 +1148,18 @@ package body Ada.Exceptions is
(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;
--------------------
......@@ -1144,15 +1167,28 @@ package body Ada.Exceptions is
--------------------
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;
-----------------------------------------
......@@ -1163,98 +1199,98 @@ package body Ada.Exceptions is
(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
......@@ -1341,6 +1377,13 @@ package body Ada.Exceptions is
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
......@@ -1355,6 +1398,13 @@ package body Ada.Exceptions 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
......@@ -1369,13 +1419,6 @@ package body Ada.Exceptions 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
......@@ -1404,116 +1447,79 @@ package body Ada.Exceptions 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;
--------------------------------------
......@@ -1522,10 +1528,18 @@ package body Ada.Exceptions is
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;
......@@ -1535,10 +1549,10 @@ package body Ada.Exceptions is
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;
......@@ -1548,9 +1562,11 @@ package body Ada.Exceptions is
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;
---------------------------------
......@@ -1558,9 +1574,12 @@ package body Ada.Exceptions is
---------------------------------
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;
---------------------
......@@ -1572,10 +1591,14 @@ package body Ada.Exceptions is
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);
......@@ -1610,13 +1633,10 @@ package body Ada.Exceptions is
---------------
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
......@@ -1651,4 +1671,78 @@ package body Ada.Exceptions 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;
gcc/ada/a-except.ads
......@@ -6,7 +6,7 @@
-- --
-- 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 --
......@@ -33,24 +33,15 @@
-- --
------------------------------------------------------------------------------
-- 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.
......@@ -62,25 +53,39 @@ with System.Traceback_Entries;
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);
......@@ -105,7 +110,9 @@ package Ada.Exceptions is
-- 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.
......@@ -121,6 +128,22 @@ package Ada.Exceptions is
(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;
......@@ -216,8 +239,8 @@ private
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
......@@ -264,6 +287,10 @@ private
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)
......@@ -295,18 +322,28 @@ private
-- 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;
gcc/ada/a-exexpr-gcc.adb deleted 100644 → 0
------------------------------------------------------------------------------
-- --
-- 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;
gcc/ada/a-exexpr.adb
......@@ -6,7 +6,7 @@
-- --
-- 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- --
......@@ -29,71 +29,411 @@
-- --
------------------------------------------------------------------------------
-- 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;
gcc/ada/exp_spark.adb
......@@ -54,7 +54,7 @@ package body Exp_SPARK is
-- 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
......@@ -86,7 +86,7 @@ package body Exp_SPARK is
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);
......
gcc/ada/gcc-interface/Make-lang.in
......@@ -99,6 +99,8 @@ ADA_TOOLS=gnatbind gnatchop gnat gnatkr gnatlink gnatls gnatmake \
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) $<
......@@ -223,6 +225,7 @@ GCC_LLINK=$(LLINKER) $(GCC_LINKERFLAGS) $(LDFLAGS)
# 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
......@@ -232,6 +235,7 @@ GNAT_ADA_OBJS = \
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 \
......@@ -334,6 +338,7 @@ GNAT_ADA_OBJS = \
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 \
......@@ -351,9 +356,11 @@ GNAT_ADA_OBJS = \
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 \
......@@ -372,7 +379,9 @@ GNAT_ADA_OBJS = \
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 \
......@@ -381,6 +390,7 @@ GNAT_ADA_OBJS = \
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 \
......@@ -514,6 +524,7 @@ GNATBIND_OBJS = \
ada/osint.o \
ada/output.o \
ada/raise.o \
ada/raise-gcc.o \
ada/restrict.o \
ada/rident.o \
ada/rtfinal.o \
......@@ -534,10 +545,12 @@ GNATBIND_OBJS = \
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 \
......@@ -555,11 +568,13 @@ GNATBIND_OBJS = \
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 \
......@@ -594,6 +609,21 @@ ADA_BACKEND = $(BACKEND) attribs.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
......@@ -976,12 +1006,12 @@ ada/sdefault.o : ada/ada.ads ada/a-except.ads ada/a-unccon.ads \
# 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)
......
gcc/ada/gcc-interface/Makefile.in
......@@ -2427,32 +2427,20 @@ endif
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
......
gcc/ada/raise-gcc.c
......@@ -6,7 +6,7 @@
* *
* 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- *
......@@ -32,10 +32,6 @@
/* 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"
......@@ -45,9 +41,14 @@
#endif
#include <stdarg.h>
#ifdef __cplusplus
# include <cstdlib>
#else
typedef char bool;
# define true 1
# define false 0
#endif
#include "raise.h"
......@@ -72,6 +73,10 @@ typedef char bool;
#include "unwind.h"
#ifdef __cplusplus
extern "C" {
#endif
typedef struct _Unwind_Context _Unwind_Context;
typedef struct _Unwind_Exception _Unwind_Exception;
......@@ -79,7 +84,7 @@ _Unwind_Reason_Code
__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 *);
......@@ -209,7 +214,7 @@ db_indent (int requests)
}
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)
{
......@@ -816,8 +821,8 @@ get_call_site_action_for (_Unwind_Ptr ip,
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)
......@@ -1399,7 +1404,7 @@ __gnat_Unwind_RaiseException (_Unwind_Exception *e)
_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__
......@@ -1609,3 +1614,7 @@ __gnat_personality_seh0 (PEXCEPTION_RECORD ms_exc, void *this_frame,
const int __gnat_unwind_exception_size = sizeof (_Unwind_Exception);
#endif
#ifdef __cplusplus
}
#endif
gcc/ada/raise.c
......@@ -6,7 +6,7 @@
* *
* 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- *
......@@ -47,20 +47,6 @@
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
......@@ -84,6 +70,71 @@ __gnat_unhandled_terminate (void)
__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
gcc/ada/sem_ch3.adb
......@@ -4195,6 +4195,14 @@ package body Sem_Ch3 is
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)));
......
gcc/ada/sem_elab.adb
......@@ -688,7 +688,7 @@ package body Sem_Elab is
-- 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;
......
gcc/ada/sem_res.adb
......@@ -11065,22 +11065,11 @@ package body Sem_Res is
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
......
gcc/ada/system.ads
......@@ -7,7 +7,7 @@
-- 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 --
......@@ -163,8 +163,8 @@ private
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)
......@@ -173,6 +173,6 @@ private
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;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment