Refine tests to one crashing and one demonstrating fix

Author: NlightNFotis

testsuite/gnat2goto/tests/object_declaration_statement/object_declaration_statement.adb

@@ -5,7 +5,7 @@ procedure Object_Declaration_Statement is
     Index : Range_Type := 0;
   begin
     if A > 10 then
-      for I in Range_Type range (Index + 1) .. Range_Type'Last
+      for I in Range_Type range (Index + 1) .. 10
       loop
         pragma Assert (I < 70);
       end loop;

testsuite/gnat2goto/tests/object_declaration_statement/test.out

@@ -0,0 +1,3 @@
+[callit.assertion.1] line 10 assertion I < 70: SUCCESS
+[callit.assertion.2] line 13 assertion A < -5: FAILURE
+VERIFICATION FAILED

testsuite/gnat2goto/tests/object_declaration_statement_bounds_crashing/object_declaration_statement_bounds_crashing.adb

@@ -0,0 +1,18 @@
+procedure Object_Declaration_Statement_Bounds_Crashing is
+  procedure Callit (A : Integer) is
+    -- Base Index type
+    type Range_Type is range 0 .. 79;
+    Index : Range_Type := 0;
+  begin
+    if A > 10 then
+      for I in Range_Type range (Index + 1) .. Range_Type'Last
+      loop
+        pragma Assert (I < 70);
+      end loop;
+      -- Intentional false assert
+      pragma Assert (A < -5);
+    end if;
+  end Callit;
+begin
+  Callit(12);
+end Object_Declaration_Statement_Bounds_Crashing;

testsuite/gnat2goto/tests/object_declaration_statement/test.opt renamed to testsuite/gnat2goto/tests/object_declaration_statement_bounds_crashing/test.opt

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