Test expansion for range check

Author: Petr Bauch

testsuite/gnat2goto/tests/ranges/ranges.adb

@@ -3,9 +3,13 @@ procedure Ranges is
    type Int2 is new Int1 range 2 .. 9;
    subtype Int3 is Int1 range 3 .. 8;
    A : Int1 := 5;
+   AA : Int1 := 10;
    B : Int2;
    C : Int3;
+   CC : Int3 := 4;
 begin
    B := Int2(A);
    C := A;
+   C := AA;
+   A := CC;
 end;

testsuite/gnat2goto/tests/ranges/test.out

@@ -1 +1,3 @@
-VERIFICATION SUCCESSFUL
+[assertion.1] Range Check: FAILURE
+[assertion.2] Range Check: FAILURE
+VERIFICATION FAILED