Merge pull request #5295 from thk123/array-equal-type-mismatch

Array equal type mismatch

Author: Thomas Kiley

regression/cbmc/Array_operations1/main.c

@@ -12,6 +12,33 @@ 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");
+  __CPROVER_assert(__CPROVER_array_equal(a1, a2), "expected to fail");
+
+  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");
+  __CPROVER_assert(
+    __CPROVER_array_equal(lost_type1, lost_type3), "expected to fail");
+
+  int a4[10];
+  int a5[10];
+
+  // Here the arrays both can be equal, and be not equal, so both asserts should fail
+  __CPROVER_assert(!__CPROVER_array_equal(a4, a5), "expected to fail");
+  __CPROVER_assert(__CPROVER_array_equal(a4, a5), "expected to fail");
+}
+
 void test_copy()
 {
   char array1[100], array2[100], array3[90];
@@ -54,4 +81,5 @@ int main()
   test_copy();
   test_replace();
   test_set();
+  test_unequal();
 }

regression/cbmc/Array_operations1/test.desc

@@ -4,7 +4,15 @@ 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\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.3\] .* different typed arrays are unequal: SUCCESS
+^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
+^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
+^\*\* 5 of 14 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+Verify the properties of various cprover array primitves

src/goto-symex/symex_other.cpp

@@ -240,7 +240,7 @@ void goto_symext::symex_other(
 
     // check for size (or type) mismatch
     if(array1.type() != array2.type())
-      assignment.lhs() = false_exprt();
+      assignment.rhs() = false_exprt();
 
     symex_assign(state, assignment);
   }