Add test case

petr-bauch · petr-bauch · commit 0d1fbb9b824f · 2019-06-12T16:29:47.000+01:00
also include the range check.
diff --git a/testsuite/gnat2goto/tests/range_check_non_bounded/test.adb b/testsuite/gnat2goto/tests/range_check_non_bounded/test.adb
@@ -0,0 +1,8 @@
+procedure Test is
+   type Uint_8 is mod 2**8;
+   Uint_Var : Uint_8 := 5;
+   Int_Var : Integer;
+begin
+   Int_Var := Integer'(Integer (Uint_Var));
+   pragma Assert (Int_Var = 5);
+end Test;
diff --git a/testsuite/gnat2goto/tests/range_check_non_bounded/test.out b/testsuite/gnat2goto/tests/range_check_non_bounded/test.out
@@ -0,0 +1,3 @@
+[assertion.1] Range Check: SUCCESS
+[1] file test.adb line 7 assertion: SUCCESS
+VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/range_check_non_bounded/test.py b/testsuite/gnat2goto/tests/range_check_non_bounded/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+[assertion.1] Range Check: SUCCESS`
	`2`	`+[1] file test.adb line 7 assertion: SUCCESS`
	`3`	`+VERIFICATION SUCCESSFUL`