Add unit test of object size tracking

Because we were previously missing unit tests for the tracking of object
sizes. Note that this test includes tracking for when object sizes are
based on symbols rather than statically defined. This is used for
dynamically sized objects such as those pointed to by the return value
of `malloc`.

Author: thomasspriggs

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -2,6 +2,7 @@
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -157,3 +158,44 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
     CHECK(objects_are_already_tracked(compound_expression, object_map));
   }
 }
+
+static symbolt make_size_variable()
+{
+  symbolt size_variable;
+  size_variable.name = "size_variable";
+  size_variable.base_name = "size_variable";
+  size_variable.type = size_type();
+  return size_variable;
+}
+
+TEST_CASE("Tracking object sizes.", "[core][smt2_incremental]")
+{
+  // Configuration needs to be performed before tracking because the size_type()
+  // width depends on the global configuration.
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64();
+  smt_object_mapt object_map = initial_smt_object_map();
+  symbol_tablet symbol_table;
+  const symbolt size_variable = make_size_variable();
+  symbol_table.insert(size_variable);
+  const symbol_exprt size_expr = size_variable.symbol_expr();
+  namespacet ns{symbol_table};
+  exprt base_object;
+  exprt expected_size;
+  using rowt = std::pair<decltype(base_object), decltype(expected_size)>;
+  std::tie(base_object, expected_size) = GENERATE_REF(
+    rowt{from_integer(0, unsignedbv_typet{(8)}), from_integer(1, size_type())},
+    rowt{from_integer(42, signedbv_typet{16}), from_integer(2, size_type())},
+    rowt{from_integer(-24, signedbv_typet{32}), from_integer(4, size_type())},
+    rowt{from_integer(2, unsignedbv_typet{64}), from_integer(8, size_type())},
+    rowt{
+      symbol_exprt{"array", array_typet{unsignedbv_typet{8}, size_expr}},
+      size_expr},
+    rowt{
+      symbol_exprt{"array", array_typet{signedbv_typet{32}, size_expr}},
+      mult_exprt{size_expr, from_integer(4, size_type())}});
+  track_expression_objects(address_of_exprt{base_object}, ns, object_map);
+  const auto object = object_map.find(base_object);
+  REQUIRE(object != object_map.end());
+  REQUIRE(object->second.size == expected_size);
+}