Add unit tests for preserving meta-information of excluded methods

These unit tests complement the regression tests in
jbmc/regression/jbmc/context-include-exclude
that were added in a previous commit to check for properties of excluded
methods. Some properties, like information about accessibility and final
and static status, is easier to check in unit-style tests.

Author: antlechner

jbmc/unit/Makefile

@@ -22,6 +22,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_bytecode_convert_method/convert_method.cpp \
        java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \
        java_bytecode/java_bytecode_language/language.cpp \
+       java_bytecode/java_bytecode_language/context_excluded.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \
        java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \

jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class

@@ -0,0 +1,18 @@
+public class ClassWithDifferentModifiers {
+
+  public static void main(String[] args) {
+    ClassWithDifferentModifiers guineaPig = new ClassWithDifferentModifiers();
+    assert guineaPig.testPublicInstance() == 1;
+    assert guineaPig.testPrivateStatic() == 2;
+    assert guineaPig.testProtectedFinalInstance() == 3;
+    assert guineaPig.testDefaultFinalStatic() == 4;
+  }
+
+  public int testPublicInstance() { return 1; }
+
+  private static int testPrivateStatic() { return 2; }
+
+  protected final int testProtectedFinalInstance() { return 3; }
+
+  final static int testDefaultFinalStatic() { return 4; }
+}

jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java

@@ -0,0 +1,84 @@
+/*******************************************************************\
+
+Module: Unit tests for java_bytecode_language.
+
+Author: Diffblue Limited.
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+
+#include <util/symbol_table.h>
+
+#include <java-testing-utils/load_java_class.h>
+#include <java-testing-utils/require_type.h>
+
+SCENARIO(
+  "Exclude a method using context-include/exclude",
+  "[core][java_bytecode][java_bytecode_language]")
+{
+  GIVEN("A class with all methods excluded except for main")
+  {
+    const symbol_tablet symbol_table =
+      load_goto_model_from_java_class(
+        "ClassWithDifferentModifiers",
+        "./java_bytecode/java_bytecode_language",
+        {},
+        {{"context-include", "ClassWithDifferentModifiers.main"}})
+        .get_symbol_table();
+
+    WHEN("Converting the methods of this class")
+    {
+      THEN(
+        "Meta-information of excluded methods is preserved. Symbol values are "
+        "nil as the lazy_goto_modelt for unit tests does not generate "
+        "stub/exclude bodies.")
+      {
+        const auto &public_instance_symbol = symbol_table.lookup_ref(
+          "java::ClassWithDifferentModifiers.testPublicInstance:()I");
+        REQUIRE(public_instance_symbol.value.is_nil());
+        const auto public_instance_type =
+          type_try_dynamic_cast<java_method_typet>(public_instance_symbol.type);
+        REQUIRE(public_instance_type);
+        REQUIRE(id2string(public_instance_type->get(ID_access)) == "public");
+        REQUIRE_FALSE(public_instance_type->get_bool(ID_is_static));
+        REQUIRE_FALSE(public_instance_type->get_is_final());
+
+        const auto &private_static_symbol = symbol_table.lookup_ref(
+          "java::ClassWithDifferentModifiers.testPrivateStatic:()I");
+        REQUIRE(private_static_symbol.value.is_nil());
+        const auto private_static_type =
+          type_try_dynamic_cast<java_method_typet>(private_static_symbol.type);
+        REQUIRE(private_static_type);
+        REQUIRE(id2string(private_static_type->get(ID_access)) == "private");
+        REQUIRE(private_static_type->get_bool(ID_is_static));
+        REQUIRE_FALSE(private_static_type->get_is_final());
+
+        const auto &protected_final_instance_symbol = symbol_table.lookup_ref(
+          "java::ClassWithDifferentModifiers.testProtectedFinalInstance:()I");
+        REQUIRE(protected_final_instance_symbol.value.is_nil());
+        const auto protected_final_instance_type =
+          type_try_dynamic_cast<java_method_typet>(
+            protected_final_instance_symbol.type);
+        REQUIRE(protected_final_instance_type);
+        REQUIRE(
+          id2string(protected_final_instance_type->get(ID_access)) ==
+          "protected");
+        REQUIRE_FALSE(protected_final_instance_type->get_bool(ID_is_static));
+        REQUIRE(protected_final_instance_type->get_is_final());
+
+        const auto &default_final_static_symbol = symbol_table.lookup_ref(
+          "java::ClassWithDifferentModifiers.testDefaultFinalStatic:()I");
+        REQUIRE(default_final_static_symbol.value.is_nil());
+        const auto default_final_static_type =
+          type_try_dynamic_cast<java_method_typet>(
+            default_final_static_symbol.type);
+        REQUIRE(default_final_static_type);
+        REQUIRE(
+          id2string(default_final_static_type->get(ID_access)) == "default");
+        REQUIRE(default_final_static_type->get_bool(ID_is_static));
+        REQUIRE(default_final_static_type->get_is_final());
+      }
+    }
+  }
+}