-- --
------------------------------------------------------------------------------
--- Ghost code, loop invariants and assertions in this unit are meant for
+-- Ghost code, loop (in)variants and assertions in this unit are meant for
-- analysis only, not for run-time checking, as it would be too costly
-- otherwise. This is enforced by setting the assertion policy to Ignore.
pragma Assertion_Policy (Ghost => Ignore,
Loop_Invariant => Ignore,
+ Loop_Variant => Ignore,
Assert => Ignore);
with Ada.Strings.Maps; use Ada.Strings.Maps;