Skip to content

Commit

Permalink
Check number of elements in arrays tests
Browse files Browse the repository at this point in the history 
Ref. #487, #509
  • Loading branch information
@treiher
treiher committed Dec 1, 2020
1 parent f119df5 commit 58374e3
Showing 1 changed file with 18 additions and 6 deletions.
24 changes: 18 additions & 6 deletions tests/spark/rflx-arrays_tests.adb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,13 +256,15 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_Modular_Vector (Context, Sequence_Context);

while I <= 10 and then Arrays.Modular_Vector.Has_Element (Sequence_Context) loop
while Arrays.Modular_Vector.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.Modular_Vector.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);

Assert (I <= 2, "Unexpected element");

Arrays.Modular_Vector.Next (Sequence_Context);

Assert (Arrays.Modular_Vector.Valid_Element (Sequence_Context), "Invalid element " & I'Image);
Expand Down Expand Up @@ -300,13 +302,15 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_Range_Vector (Context, Sequence_Context);

while I <= 10 and then Arrays.Range_Vector.Has_Element (Sequence_Context) loop
while Arrays.Range_Vector.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.Range_Vector.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);

Assert (I <= 2, "Unexpected element");

Arrays.Range_Vector.Next (Sequence_Context);

Assert (Arrays.Range_Vector.Valid_Element (Sequence_Context), "Invalid element " & I'Image);
Expand Down Expand Up @@ -344,13 +348,15 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_Enumeration_Vector (Context, Sequence_Context);

while I <= 10 and then Arrays.Enumeration_Vector.Has_Element (Sequence_Context) loop
while Arrays.Enumeration_Vector.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.Enumeration_Vector.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);

Assert (I <= 2, "Unexpected element");

Arrays.Enumeration_Vector.Next (Sequence_Context);

Assert (Arrays.Enumeration_Vector.Valid_Element (Sequence_Context), "Invalid element " & I'Image);
Expand Down Expand Up @@ -390,13 +396,15 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_AV_Enumeration_Vector (Context, Sequence_Context);

while I <= 10 and then Arrays.AV_Enumeration_Vector.Has_Element (Sequence_Context) loop
while Arrays.AV_Enumeration_Vector.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.AV_Enumeration_Vector.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);

Assert (I <= 2, "Unexpected element");

Arrays.AV_Enumeration_Vector.Next (Sequence_Context);

Assert (Arrays.AV_Enumeration_Vector.Valid_Element (Sequence_Context), "Invalid element " & I'Image);
Expand Down Expand Up @@ -847,14 +855,16 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_Messages (Context, Sequence_Context);

while I <= 10 and then Arrays.Inner_Messages.Has_Element (Sequence_Context) loop
while Arrays.Inner_Messages.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.Inner_Messages.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);
pragma Loop_Invariant (not Inner_Message.Has_Buffer (Element_Context));

Assert (I <= 2, "Unexpected element");

Arrays.Inner_Messages.Switch (Sequence_Context, Element_Context);

Inner_Message.Verify_Message (Element_Context);
Expand Down Expand Up @@ -1100,13 +1110,15 @@ package body RFLX.Arrays_Tests is

Message.Switch_To_Vector (Context, Sequence_Context);

while I <= 10 and then Arrays.Modular_Vector.Has_Element (Sequence_Context) loop
while Arrays.Modular_Vector.Has_Element (Sequence_Context) loop
pragma Loop_Invariant (Arrays.Modular_Vector.Has_Buffer (Sequence_Context));
pragma Loop_Invariant (Context.Buffer_First = Sequence_Context.Buffer_First);
pragma Loop_Invariant (Context.Buffer_Last = Sequence_Context.Buffer_Last);
pragma Loop_Invariant (Sequence_Context.First = Sequence_Context.First'Loop_Entry);
pragma Loop_Invariant (Sequence_Context.Last = Sequence_Context.Last'Loop_Entry);

Assert (I <= 2, "Unexpected element");

Arrays.Modular_Vector.Next (Sequence_Context);

Assert (Arrays.Modular_Vector.Valid_Element (Sequence_Context), "Invalid element " & I'Image);
Expand Down

0 comments on commit 58374e3

Please sign in to comment.