Add test for different sized arrays

__CPROVER_array_equal should be able verify that arrays of different
size or type are never equal, and the assert should verify.

Author: Thomas Kiley

regression/cbmc/Array_operations1/main.c

@@ -12,6 +12,23 @@ void test_equal()
   __CPROVER_assert(array1[index] == array2[index], "arrays are equal");
 }
 
+void test_unequal()
+{
+  int a1[10];
+  int a2[16];
+
+  __CPROVER_assert(
+    !__CPROVER_array_equal(a1, a2), "different sizes arrays are unequal");
+
+  float a3[10];
+  void *lost_type1 = a1;
+  void *lost_type3 = a3;
+
+  __CPROVER_assert(
+    !__CPROVER_array_equal(lost_type1, lost_type3),
+    "different typed arrays are unequal");
+}
+
 void test_copy()
 {
   char array1[100], array2[100], array3[90];
@@ -54,4 +71,5 @@ int main()
   test_copy();
   test_replace();
   test_set();
+  test_unequal();
 }

regression/cbmc/Array_operations1/test.desc

@@ -4,7 +4,9 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
-^\*\* 1 of 8 failed
+^\[test_unequal\.assertion\.1\] .* different sizes arrays are unequal: SUCCESS
+^\[test_unequal\.assertion\.2\] .* different typed arrays are unequal: SUCCESS
+^\*\* 1 of 10 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring