Merge pull request #6762 from tautschnig/bugfixes/fs-array_equal

Full slicing: fix bugs in handling array_equal

Author: tautschnig

regression/cbmc/Array_operations1/full-slice.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--full-slice
+^EXIT=10$
+^SIGNAL=0$
+^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
+^\[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/analyses/goto_rw.cpp

@@ -805,11 +805,14 @@ static void goto_rw_other(
   else if(statement == ID_array_equal)
   {
     // mark the dereferenced operands as being read
-    for(const auto &op : code.operands())
-    {
-      rw_set.get_array_objects(
-        function, target, rw_range_sett::get_modet::READ, op);
-    }
+    PRECONDITION(code.operands().size() == 3);
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::READ, code.op0());
+    rw_set.get_array_objects(
+      function, target, rw_range_sett::get_modet::READ, code.op1());
+    // the third operand is the result
+    rw_set.get_objects_rec(
+      function, target, rw_range_sett::get_modet::LHS_W, code.op2());
   }
   else if(statement == ID_array_set)
   {

src/pointer-analysis/value_set.cpp

@@ -1615,8 +1615,7 @@ void value_sett::apply_code_rec(
   {
     // can be ignored, we don't expect side effects here
   }
-  else if(statement=="cpp_delete" ||
-          statement=="cpp_delete[]")
+  else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
   {
     // does nothing
   }
@@ -1653,6 +1652,9 @@ void value_sett::apply_code_rec(
   else if(statement==ID_array_replace)
   {
   }
+  else if(statement == ID_array_equal)
+  {
+  }
   else if(statement==ID_assume)
   {
     guard(to_code_assume(code).assumption(), ns);

src/pointer-analysis/value_set_fi.cpp

@@ -1390,9 +1390,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
   else if(statement==ID_fence)
   {
   }
-  else if(statement==ID_array_copy ||
-          statement==ID_array_replace ||
-          statement==ID_array_set)
+  else if(
+    statement == ID_array_copy || statement == ID_array_replace ||
+    statement == ID_array_set || statement == ID_array_equal)
   {
   }
   else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))