path: root/gcc/testsuite/ada/acats-4/support/f732b00.a

-- F732B00.A
--
--                             Grant of Unlimited Rights
--
--     The Ada Conformity Assessment Authority (ACAA) holds unlimited
--     rights in the software and documentation contained herein. Unlimited
--     rights are the same as those granted by the U.S. Government for older
--     parts of the Ada Conformity Assessment Test Suite, and are defined
--     in DFAR 252.227-7013(a)(19). By making this public release, the ACAA
--     intends to confer upon all recipients unlimited rights equal to those
--     held by the ACAA. These rights include rights to use, duplicate,
--     release or disclose the released technical data and computer software
--     in whole or in part, in any manner and for any purpose whatsoever, and
--     to have or permit others to do so.
--
--                                    DISCLAIMER
--
--     ALL MATERIALS OR INFORMATION HEREIN RELEASED, MADE AVAILABLE OR
--     DISCLOSED ARE AS IS. THE ACAA MAKES NO EXPRESS OR IMPLIED
--     WARRANTY AS TO ANY MATTER WHATSOEVER, INCLUDING THE CONDITIONS OF THE
--     SOFTWARE, DOCUMENTATION OR OTHER INFORMATION RELEASED, MADE AVAILABLE
--     OR DISCLOSED, OR THE OWNERSHIP, MERCHANTABILITY, OR FITNESS FOR A
--     PARTICULAR PURPOSE OF SAID MATERIAL.
--
--                                     Notice
--
--     The ACAA has created and maintains the Ada Conformity Assessment Test
--     Suite for the purpose of conformity assessments conducted in accordance
--     with the International Standard ISO/IEC 18009 - Ada: Conformity
--     assessment of a language processor. This test suite should not be used
--     to make claims of conformance unless used in accordance with
--     ISO/IEC 18009 and any applicable ACAA procedures.
--*
--
-- FOUNDATION DESCRIPTION:
--      This foundation provides the basis for testing aspect Type_Invariant
--      on a private type and accesses to that private type.
--
--      Note that a default-initialized object of type
--      Change_Discriminated_Type will always fail an invariant check. We do
--      this to test 7.3.2(10/4).
--
--      This foundation is based on a package for generating "Diagrams" for
--      bellringing. The type invariant is that each bell occurs once and only
--      once.
--
-- CHANGE HISTORY:
--      25 Dec 14   JAC     Initial pre-release version.
--      20 Jan 15   JAC     Second pre-release version.
--      09 Apr 15   RLB     Fixed formatting problems; removed uses of Text_IO.
--      10 Apr 15   RLB     Added operations on access-to-priv.
--
--!
package F732B00 is

   pragma Assertion_Policy (Check);

   Max_No_Of_Bells : constant := 16;

   No_Of_Bells : constant := 8;

   type Bell_Range_Type is range 1 .. Max_No_Of_Bells;

   type Change_Discriminated_Type (No_Of_Bells : Bell_Range_Type) is private
     with
       Type_Invariant => Each_Bell_Occurs_Once (Change_Discriminated_Type) and
                         And_Only_Once         (Change_Discriminated_Type);

   subtype Swappable_Bell_Range_Type is Bell_Range_Type range 1 ..
     No_Of_Bells - 1;

   subtype Number_Of_Pairs_To_Swap_Type is Bell_Range_Type range 1 ..
     No_Of_Bells / 2;

   type Pairs_To_Swap_Type is array (Number_Of_Pairs_To_Swap_Type range <>) of
     Swappable_Bell_Range_Type;

   type Bells_To_Swap_Type
     (Number_Of_Pairs_To_Swap : Number_Of_Pairs_To_Swap_Type) is record
      Pairs_To_Swap : Pairs_To_Swap_Type (1 .. Number_Of_Pairs_To_Swap);
   end record;

   function Each_Bell_Occurs_Once (Change : Change_Discriminated_Type) return
     Boolean;

   function And_Only_Once         (Change : Change_Discriminated_Type) return
     Boolean;

   function Rounds_With_Default_Initialisation
      return Change_Discriminated_Type;

   function Rounds return Change_Discriminated_Type;

   function Invalid_Change return Change_Discriminated_Type;

   procedure Print_Change (Change : Change_Discriminated_Type);

   procedure Hunt_For_One_Change
     (Change       : in out Change_Discriminated_Type;
      Tenor_Behind : in     Boolean := True);

   function At_Lead_End (Change : in Change_Discriminated_Type) return Boolean;

   procedure Grandsire_Change (Change : in out Change_Discriminated_Type)
     with
       Pre => No_Of_Bells >= 5;

   procedure Invalid_Grandsire_Change
     (Change : in out Change_Discriminated_Type)
     with
       Pre => No_Of_Bells >= 5;

   function Swaps_Dont_Overlap (Bells_To_Swap : in Bells_To_Swap_Type) return
     Boolean;

   procedure Swap_Places
     (Change        : in out Change_Discriminated_Type;
      Bells_To_Swap : in     Bells_To_Swap_Type)
     with
       Pre => Swaps_Dont_Overlap (Bells_To_Swap);

   -- Operations to test access-to-private-with-invariants. Note that we
   -- try similar operations with an anonymous access type and with
   -- a named access type.

   type Access_to_Change is access all Change_Discriminated_Type;

   type Change_Kind is (Valid, Invalid);

   procedure Reset_Change (Change : not null access Change_Discriminated_Type;
                           Kind   : in Change_Kind);
      -- Adjust Change as specified by Kind.

   type Get_Change_Kind is (Param_Invalid, Result_Invalid, Result_is_Param,
                            Result_Other_Valid);

   function Get_Change (Change : Access_to_Change;
                        Kind   : in Get_Change_Kind) return Access_to_Change;
      -- Get a Change value, what happens depends on Kind.

   function Create_Change (Kind : in Change_Kind)
      return not null access Change_Discriminated_Type;
      -- Create a Change value as specified by Kind.

private

   type Change_Array_Type is array (Bell_Range_Type range <>) of
     Bell_Range_Type
      with Default_Component_Value => Bell_Range_Type'First;
      -- Note: Any default-initialized object will fail an invariant check,
      -- no matter where it is used.

   type Change_Discriminated_Type (No_Of_Bells : Bell_Range_Type) is record
      Change : Change_Array_Type (Bell_Range_Type range 1 .. No_Of_Bells);
   end record
     with Dynamic_Predicate =>
       (for all Bell_Number in Bell_Range_Type range 1 .. No_Of_Bells =>
          Change_Discriminated_Type.Change (Bell_Number) <= No_Of_Bells);

end F732B00;

with Report;

package body F732B00 is

   pragma Assertion_Policy (Check);

   Change_Number : Natural := 0;

   function Each_Bell_Occurs_Once (Change : Change_Discriminated_Type) return
     Boolean is
     (for all Bell_Number in 1 .. Change.No_Of_Bells =>
        (for some Bell in 1 .. Change.No_Of_Bells =>
            Change.Change (Bell) = Bell_Number
        )
     );

   function And_Only_Once         (Change : Change_Discriminated_Type) return
     Boolean is
     (not
        (for some Bell in 1 .. Change.No_Of_Bells -1 =>
            (for some Other_Bell in Bell + 1 .. Change.No_Of_Bells =>
               Change.Change (Bell) = Change.Change (Other_Bell)
            )
        )
     );

   function Rounds_With_Default_Initialisation
      return Change_Discriminated_Type is

      -- Default initialisation checks the type invariant even within the
      -- package, RM 7.3.2(10/3)

      Change : Change_Discriminated_Type (No_Of_Bells);

   begin

      for Bell in 1 .. Change.No_Of_Bells loop

         Change.Change (Bell) := Bell;

      end loop;

      return Change;

   end Rounds_With_Default_Initialisation;

   function Rounds return Change_Discriminated_Type is

      -- Can knowingly set to something that breaches the type invariant, but
      -- can't use default initialisation as that still checks the type
      -- invariant, RM 7.3.2(10/3) doesn't exclude within the package.

      Change : Change_Discriminated_Type :=
                            (No_Of_Bells => No_Of_Bells,
                             Change      => (others => Bell_Range_Type'First));

   begin

      for Bell in 1 .. Change.No_Of_Bells loop

         Change.Change (Bell) := Bell;

      end loop;

      return Change;

   end Rounds;

   function Invalid_Change return Change_Discriminated_Type is

      -- Can knowingly set to something that breaches the type invariant
      -- within the package.

      Change : constant Change_Discriminated_Type :=
                            (No_Of_Bells => No_Of_Bells,
                             Change      => (others => Bell_Range_Type'First));

   begin

      return Change;

   end Invalid_Change;

   procedure Print_Change (Change : Change_Discriminated_Type) is
     Result : String (1 .. Natural(Change.No_Of_Bells*3));
   begin

      for Place in 1 .. Change.No_Of_Bells loop

         if Change.Change (Place) < 10 then
            Result (Natural(Place*3-2)) := ' ';
            Result (Natural(Place*3-1)) :=
               Character'Val(Change.Change (Place) + Character'Pos('0'));
         else
            Result (Natural(Place*3-2)) := '1';
            Result (Natural(Place*3-1)) :=
               Character'Val(Change.Change (Place) - 10 + Character'Pos('0'));
         end if;
         Result (Natural(Place*3)) := ' ';

      end loop;

      Report.Comment ("Change: " & Result);

   end Print_Change;

   procedure Swap_Bell_With_Following_Bell
     (Change       : in out Change_Discriminated_Type;
      Bell_To_Swap : in     Swappable_Bell_Range_Type) is

      Temp : Bell_Range_Type;

   begin

      Temp := Change.Change (Bell_To_Swap);
      Change.Change (Bell_To_Swap) := Change.Change (Bell_To_Swap + 1);
      Change.Change (Bell_To_Swap + 1) := Temp;

   end Swap_Bell_With_Following_Bell;

   procedure Hunt_For_One_Change
     (Change       : in out Change_Discriminated_Type;
      Tenor_Behind : in     Boolean := True) is

      Hunt_On_How_Many : constant Bell_Range_Type :=
                       (if Tenor_Behind then No_Of_Bells - 1 else No_Of_Bells);

   begin

      -- If Even Change_Number
      if Change_Number mod 2 = 0 then

         for Place in 1 .. Hunt_On_How_Many - 1 loop

            -- If Odd Place
            if Place mod 2 = 1 then

               Swap_Bell_With_Following_Bell
                (Change       => Change,
                 Bell_To_Swap => Place);

            end if;

         end loop;

      else -- Odd Change_Number

         for Place in 1 .. Hunt_On_How_Many - 1 loop

            -- If Even Place
            if Place mod 2 = 0 then

               Swap_Bell_With_Following_Bell
                (Change       => Change,
                 Bell_To_Swap => Place);

            end if;

         end loop;

      end if;

      Change_Number := Change_Number + 1;

   end Hunt_For_One_Change;

   function At_Lead_End (Change : in Change_Discriminated_Type) return Boolean
     is
      (Change.Change (1) = 1);

   procedure Grandsire_Change (Change : in out Change_Discriminated_Type) is
   begin

      Swap_Bell_With_Following_Bell
        (Change       => Change,
         Bell_To_Swap => 1);

      for Place in Bell_Range_Type range 4 .. No_Of_Bells - 1 loop

         if Place mod 2 = 0 then

            Swap_Bell_With_Following_Bell
             (Change       => Change,
              Bell_To_Swap => Place);

         end if;

      end loop;

      Change_Number := Change_Number + 1;

   end Grandsire_Change;

   procedure Broken_Swap_Bell_With_Following_Bell
     (Change       : in out Change_Discriminated_Type;
      Bell_To_Swap : in     Swappable_Bell_Range_Type) is

      Temp : Bell_Range_Type;

   begin

      Temp := Change.Change (Bell_To_Swap);
      Change.Change (Bell_To_Swap) := Change.Change (Bell_To_Swap + 1);
      -- Last line of swap missing.

   end Broken_Swap_Bell_With_Following_Bell;

   procedure Invalid_Grandsire_Change
     (Change : in out Change_Discriminated_Type) is
      -- A routine that uses a buggy Swap routine to make a mess.
      -- Note that the local broken swap does NOT check the invariant after
      -- each call; if we cleaned up the mess before the end of this routine,
      -- there would be no problem.
   begin

      Broken_Swap_Bell_With_Following_Bell
        (Change       => Change,
         Bell_To_Swap => 1);

      for Place in Bell_Range_Type range 4 .. No_Of_Bells - 1 loop

         if Place mod 2 = 0 then

            Broken_Swap_Bell_With_Following_Bell
             (Change       => Change,
              Bell_To_Swap => Place);

         end if;

      end loop;

      Change_Number := Change_Number + 1;

   end Invalid_Grandsire_Change;

   function Swaps_Dont_Overlap (Bells_To_Swap : in Bells_To_Swap_Type) return
     Boolean is
     (for all Pair_To_Swap in 1 .. Bells_To_Swap.Number_Of_Pairs_To_Swap - 1 =>
         Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap + 1) >=
         Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap) + 2
     );

   procedure Swap_Places
    (Change        : in out Change_Discriminated_Type;
     Bells_To_Swap : in     Bells_To_Swap_Type) is
   begin

      for Pair_To_Swap in 1 .. Bells_To_Swap.Number_Of_Pairs_To_Swap loop

         Swap_Bell_With_Following_Bell
          (Change       => Change,
           Bell_To_Swap => Bells_To_Swap.Pairs_To_Swap (Pair_To_Swap));

      end loop;

      Change_Number := Change_Number + 1;

   end Swap_Places;


   procedure Reset_Change (Change : not null access Change_Discriminated_Type;
                           Kind   : in Change_Kind) is
      -- Adjust Change as specified by Kind.
   begin
      if Kind = Valid then
         Change.all := Rounds;
      else -- Kind = Invalid then
         -- Note: We can't call a public routine here, or that would make
         -- and fail the invariant check and we would not test our objectives.
         Change.Change := (others => Bell_Range_Type'First);
      end if;
   end Reset_Change;

   Temp : aliased Change_Discriminated_Type (No_Of_Bells) :=
       Rounds; -- Have to initialize, else will fail invariant check.

   function Get_Change (Change : Access_to_Change;
                        Kind   : in Get_Change_Kind) return Access_to_Change is
      -- Get a Change value, what happens depends on Kind.
   begin
      if Kind = Param_Invalid then
         -- Note: We can't call a public routine here, or that would make
         -- and fail the invariant check and we would not test our objectives.
         Change.Change := (others => Bell_Range_Type'First);
         return null;
      elsif Kind = Result_Invalid then
         -- See note above.
         Temp.Change := (others => Bell_Range_Type'Last);
         return Temp'Access;
      elsif Kind = Result_is_Param then
         return Change;
      else --if Kind = Result_Other_Valid then
         Temp.Change := Rounds.Change;
         return Temp'Access;
      end if;
   end Get_Change;

   function Create_Change (Kind : in Change_Kind)
      return not null access Change_Discriminated_Type is
      -- Create a Change value as specified by Kind.
   begin
      if Kind = Valid then
         Temp.Change := Rounds.Change;
         return Temp'Access;
      else -- Kind = Invalid then
         -- Note: We can't call a public routine here, or that would make
         -- and fail the invariant check and we would not test our objectives.
         Temp.Change := (others => Bell_Range_Type'Last);
         return Temp'Access;
      end if;
   end Create_Change;

end F732B00;