Added test case enum_range_checks to test using enumeration position..

Using enumeration literal position instead of
enumeration literal representation for enumeration types maintains an order
relation between literals of an enumeration.
This test fails for a number of reasons prior to the mods on this branch.

Author: tjj2017

testsuite/gnat2goto/tests/enum_range_checks/enums.adb

@@ -0,0 +1,31 @@
+procedure Enums is
+   type My_Enum is (one, two, three, four, five);
+
+   subtype Enum_Sub is My_Enum range two .. four;
+
+   VE : My_Enum;
+   VS : Enum_Sub;
+   T  : My_Enum;
+begin
+   VE := one;
+   VS := two;
+   T  := VE;
+   VE := VS;
+   VS := VE;
+   VE := T;
+   pragma Assert (VE in My_Enum);
+   pragma Assert (VE >= My_Enum'First and VE <= My_Enum'Last);
+   pragma Assert (VE >= Enum_Sub'First and VE <= Enum_Sub'Last);
+   pragma Assert (VS in My_Enum);
+   pragma Assert (VS >= My_Enum'First and VS <= My_Enum'Last);
+   pragma Assert (VS >= Enum_Sub'First and VS <= Enum_Sub'Last);
+   pragma Assert (VE <= VS);
+   pragma Assert (VE <= My_Enum'Last);
+   pragma Assert (VE >= My_Enum'First);
+   pragma Assert (VE in Enum_Sub);
+   pragma Assert (VE >= Enum_Sub'First);
+   pragma Assert (VE = one);
+   pragma Assert (VE = T);
+   pragma Assert (VS = two);
+   pragma Assert (T = one);
+end Enums;

testsuite/gnat2goto/tests/enum_range_checks/test.out

@@ -0,0 +1,5 @@
+[enum.assertion.1] line 8 assertion A = Get_A: SUCCESS
+[enum.assertion.2] line 10 assertion B = Get_B: SUCCESS
+[enum.assertion.3] line 12 assertion Get_A /= Get_B: SUCCESS
+[enum.assertion.4] line 14 assertion Get_A = Get_B: FAILURE
+VERIFICATION FAILED

testsuite/gnat2goto/tests/enum_range_checks/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()