Merge pull request #328 from spanners/loop_range_test

Add test for N_Loop_Parameter_Specification #28

Author: martin-cs

testsuite/gnat2goto/tests/ukni_loop_parameter_specification/test.adb

@@ -0,0 +1,13 @@
+procedure Test is
+
+   type Unsigned_16 is mod 2 ** 16;
+   for Unsigned_16'Size use 16;
+
+   RAM_Start : constant Unsigned_16 := 16#0200#;
+   RAM_End   : constant Unsigned_16 := 16#2199#;
+
+begin
+   for I in Unsigned_16 range RAM_Start .. RAM_End loop
+      pragma Assert (I < 16#2200#);
+   end loop;
+end Test;

testsuite/gnat2goto/tests/ukni_loop_parameter_specification/test.out

@@ -0,0 +1,2 @@
+[test.assertion.1] line 11 assertion I < 16#2200#: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/ukni_loop_parameter_specification/test.py

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