diff options
| author | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2017-04-27 09:48:45 +0000 |
|---|---|---|
| committer | charlet <charlet@138bc75d-0d04-0410-961f-82ee72b054a4> | 2017-04-27 09:48:45 +0000 |
| commit | 4af1de5b4b45c597d63e935dc3fae6d94b27d39e (patch) | |
| tree | 1b8bba33017bf56868f71410e9917dde0ac8c621 | |
| parent | e309c6a600e5fad060c61ae2d24c4470597abf6d (diff) | |
| download | gcc-4af1de5b4b45c597d63e935dc3fae6d94b27d39e.tar.gz | |
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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@247301 138bc75d-0d04-0410-961f-82ee72b054a4
| -rw-r--r-- | gcc/ada/ChangeLog | 84 | ||||
| -rw-r--r-- | gcc/ada/a-cfdlli.adb | 181 | ||||
| -rw-r--r-- | gcc/ada/a-cfdlli.ads | 640 | ||||
| -rw-r--r-- | gcc/ada/a-cofuma.adb | 216 | ||||
| -rw-r--r-- | gcc/ada/a-cofuma.ads | 243 | ||||
| -rw-r--r-- | gcc/ada/a-cofuse.adb | 110 | ||||
| -rw-r--r-- | gcc/ada/a-cofuse.ads | 214 | ||||
| -rw-r--r-- | gcc/ada/a-cofuve.adb | 246 | ||||
| -rw-r--r-- | gcc/ada/a-cofuve.ads | 346 | ||||
| -rw-r--r-- | gcc/ada/a-except-2005.adb | 1748 | ||||
| -rw-r--r-- | gcc/ada/a-except-2005.ads | 349 | ||||
| -rw-r--r-- | gcc/ada/a-except.adb | 1070 | ||||
| -rw-r--r-- | gcc/ada/a-except.ads | 97 | ||||
| -rw-r--r-- | gcc/ada/a-exexpr-gcc.adb | 439 | ||||
| -rw-r--r-- | gcc/ada/a-exexpr.adb | 410 | ||||
| -rw-r--r-- | gcc/ada/exp_spark.adb | 4 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Make-lang.in | 34 | ||||
| -rw-r--r-- | gcc/ada/gcc-interface/Makefile.in | 20 | ||||
| -rw-r--r-- | gcc/ada/raise-gcc.c | 29 | ||||
| -rw-r--r-- | gcc/ada/raise.c | 81 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_elab.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 17 | ||||
| -rw-r--r-- | gcc/ada/system.ads | 8 |
24 files changed, 2497 insertions, 4099 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c8746dba433..8bffbec10ff 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,87 @@ +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, diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index 52bdc18ea55..d799dccb3fe 100644 --- a/gcc/ada/a-cfdlli.adb +++ b/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; diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 62cdf52028e..0fce67383e0 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/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 diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index e46f9ae85b2..39759f48681 100644 --- a/gcc/ada/a-cofuma.adb +++ b/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; diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index e6da44ae843..89adcb29e51 100644 --- a/gcc/ada/a-cofuma.ads +++ b/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; diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb index 12881753c31..d9b4c1dbe78 100644 --- a/gcc/ada/a-cofuse.adb +++ b/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; diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index 410b1cb3d6f..f9848f9d4ed 100644 --- a/gcc/ada/a-cofuse.ads +++ b/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; diff --git a/gcc/ada/a-cofuve.adb b/gcc/ada/a-cofuve.adb index fdab8c23a50..e8f8757468b 100644 --- a/gcc/ada/a-cofuve.adb +++ b/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; diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads index 74f1bfb4220..ad359b41e10 100644 --- a/gcc/ada/a-cofuve.ads +++ b/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; diff --git a/gcc/ada/a-except-2005.adb b/gcc/ada/a-except-2005.adb deleted file mode 100644 index a346494f6c4..00000000000 --- a/gcc/ada/a-except-2005.adb +++ /dev/null @@ -1,1748 +0,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; diff --git a/gcc/ada/a-except-2005.ads b/gcc/ada/a-except-2005.ads deleted file mode 100644 index cb2b2976e4a..00000000000 --- a/gcc/ada/a-except-2005.ads +++ /dev/null @@ -1,349 +0,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; diff --git a/gcc/ada/a-except.adb b/gcc/ada/a-except.adb index 3b9caeadf8d..1b8e625b51e 100644 --- a/gcc/ada/a-except.adb +++ b/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; diff --git a/gcc/ada/a-except.ads b/gcc/ada/a-except.ads index 79ca6c8558b..ff99e351ab6 100644 --- a/gcc/ada/a-except.ads +++ b/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; diff --git a/gcc/ada/a-exexpr-gcc.adb b/gcc/ada/a-exexpr-gcc.adb deleted file mode 100644 index 91fb5f5cd67..00000000000 --- a/gcc/ada/a-exexpr-gcc.adb +++ /dev/null @@ -1,439 +0,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; diff --git a/gcc/ada/a-exexpr.adb b/gcc/ada/a-exexpr.adb index e2fd7d70e1e..91fb5f5cd67 100644 --- a/gcc/ada/a-exexpr.adb +++ b/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; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 6eee24b65d1..abc79f3df94 100644 --- a/gcc/ada/exp_spark.adb +++ b/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); diff --git a/gcc/ada/gcc-interface/Make-lang.in b/gcc/ada/gcc-interface/Make-lang.in index eb0489b4a50..10c865f457d 100644 --- a/gcc/ada/gcc-interface/Make-lang.in +++ b/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) diff --git a/gcc/ada/gcc-interface/Makefile.in b/gcc/ada/gcc-interface/Makefile.in index 14269e271e1..b65ec2c7506 100644 --- a/gcc/ada/gcc-interface/Makefile.in +++ b/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 diff --git a/gcc/ada/raise-gcc.c b/gcc/ada/raise-gcc.c index 0074ad53fbc..cb35842b061 100644 --- a/gcc/ada/raise-gcc.c +++ b/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 diff --git a/gcc/ada/raise.c b/gcc/ada/raise.c index a61723d10e4..8434b67293d 100644 --- a/gcc/ada/raise.c +++ b/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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 5379a856bd8..316457422e9 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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))); diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index c78a1310553..676c1460161 100644 --- a/gcc/ada/sem_elab.adb +++ b/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; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index de5053c5158..0595b0b0835 100644 --- a/gcc/ada/sem_res.adb +++ b/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 diff --git a/gcc/ada/system.ads b/gcc/ada/system.ads index bab3bd76e85..c35ee7cab27 100644 --- a/gcc/ada/system.ads +++ b/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; |