Unit test convert_astore

This method was not directly tested

Author: romainbrenguier

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -17,6 +17,7 @@ Author: Diffblue Limited.
 
 #include <java_bytecode/java_bytecode_convert_method_class.h>
 #include <java_bytecode/java_utils.h>
+#include <testing-utils/message.h>
 
 SCENARIO(
   "java_bytecode_convert_bridge_method",
@@ -298,6 +299,15 @@ class java_bytecode_convert_method_unit_testt
   {
     return java_bytecode_convert_methodt::convert_aload(statement, op);
   }
+
+  static code_blockt convert_astore(
+    java_bytecode_convert_methodt &converter,
+    const irep_idt &statement,
+    const exprt::operandst &op,
+    const source_locationt &location)
+  {
+    return converter.convert_astore(statement, op, location);
+  }
 };
 
 SCENARIO(
@@ -397,3 +407,114 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "astore",
+  "[core][java_bytecode][java_bytecode_convert_method][convert_astore]")
+{
+  symbol_tablet symbol_table;
+  java_string_library_preprocesst string_preprocess;
+  const class_hierarchyt class_hierarchy;
+  java_bytecode_convert_methodt converter{symbol_table,
+                                          null_message_handler,
+                                          10,
+                                          true,
+                                          {},
+                                          string_preprocess,
+                                          class_hierarchy,
+                                          false};
+
+  GIVEN("An int array")
+  {
+    const source_locationt location;
+    const typet int_array_type = java_array_type('i');
+    const symbol_exprt int_array{"int_array", int_array_type};
+    const exprt offset = from_integer(3, java_int_type());
+    const exprt value = from_integer(4, java_int_type());
+    WHEN("iastore is called on the int array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "iastore", {int_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form `*(int_array->data + 3) = "
+        "4`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        auto query = make_query(result.statements()[0]).as<code_assignt>();
+        REQUIRE(query[1].get() == value);
+        auto plus = query[0].as<dereference_exprt>()[0].as<plus_exprt>();
+        REQUIRE(plus[1].get() == offset);
+        REQUIRE(
+          plus[0].as<member_exprt>().get().get_component_name() == "data");
+        REQUIRE(
+          plus[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          int_array);
+        THEN("int_array->data has type *int")
+        {
+          REQUIRE(
+            plus[0].as<member_exprt>().get().type() ==
+            pointer_type(java_int_type()));
+        }
+      }
+    }
+  }
+
+  GIVEN("A boolean array")
+  {
+    const source_locationt location;
+    const typet boolean_array_type = java_array_type('z');
+    const symbol_exprt boolean_array{"boolean_array", boolean_array_type};
+    const exprt offset = from_integer(3, java_int_type());
+    const exprt value = from_integer(true, java_boolean_type());
+    WHEN("bastore is called on the boolean array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "bastore", {boolean_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form "
+        "`*(boolean_array->data + 3) = true`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        auto query = make_query(result.statements()[0]).as<code_assignt>();
+        REQUIRE(query[1].get() == value);
+        auto plus = query[0].as<dereference_exprt>()[0].as<plus_exprt>();
+        REQUIRE(plus[1].get() == offset);
+        REQUIRE(
+          plus[0].as<member_exprt>().get().get_component_name() == "data");
+        REQUIRE(
+          plus[0].as<member_exprt>()[0].as<dereference_exprt>()[0].get() ==
+          boolean_array);
+        THEN("boolean_array->data has type *boolean")
+        {
+          REQUIRE(
+            plus[0].as<member_exprt>().get().type() ==
+            pointer_type(java_boolean_type()));
+        }
+      }
+    }
+    WHEN("iastore is called on the boolean array")
+    {
+      const code_blockt result =
+        java_bytecode_convert_method_unit_testt::convert_astore(
+          converter, "iastore", {boolean_array, offset, value}, location);
+      THEN(
+        "The result contains 1 statement of the form "
+        "`*(((int[])boolean_array)->data + offset)`")
+      {
+        REQUIRE(result.statements().size() == 1);
+        REQUIRE(
+          make_query(result.statements()[0])
+            .as<code_assignt>()[0]
+            .as<dereference_exprt>()[0]
+            .as<plus_exprt>()[0]
+            .as<member_exprt>()[0]
+            .as<dereference_exprt>()[0]
+            .as<typecast_exprt>()
+            .get()
+            .type() == java_array_type('i'));
+      }
+    }
+  }
+}