diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5a9966ece1..4d9cc0dba9 100644 --- a/jbmc/unit/Makefile +++ b/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 \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class new file mode 100644 index 0000000000..47961b187b Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java new file mode 100644 index 0000000000..382b93b21f --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java @@ -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; } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp b/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp new file mode 100644 index 0000000000..1c39c2a758 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp @@ -0,0 +1,98 @@ +/*******************************************************************\ + +Module: Unit tests for java_bytecode_language. + +Author: Diffblue Limited. + +\*******************************************************************/ + +#include + +#include + +#include +#include + +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") + { + const auto public_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPublicInstance:()I"); + REQUIRE(public_instance_symbol); + const auto public_instance_type = + type_try_dynamic_cast(public_instance_symbol->type); + + const auto private_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPrivateStatic:()I"); + REQUIRE(private_static_symbol); + const auto private_static_type = + type_try_dynamic_cast(private_static_symbol->type); + + const auto protected_final_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testProtectedFinalInstance:()I"); + REQUIRE(protected_final_instance_symbol); + const auto protected_final_instance_type = + type_try_dynamic_cast( + protected_final_instance_symbol->type); + + const auto default_final_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testDefaultFinalStatic:()I"); + REQUIRE(default_final_static_symbol); + const auto default_final_static_type = + type_try_dynamic_cast( + default_final_static_symbol->type); + THEN( + "Symbol values for excluded methods are nil as the lazy_goto_modelt " + "for unit tests does not generate stub/exclude bodies.") + { + REQUIRE(public_instance_symbol->value.is_nil()); + REQUIRE(private_static_symbol->value.is_nil()); + REQUIRE(protected_final_instance_symbol->value.is_nil()); + REQUIRE(default_final_static_symbol->value.is_nil()); + } + THEN( + "Types of excluded methods are stored as java_method_typets in the " + "symbol table.") + { + REQUIRE(public_instance_type); + REQUIRE(private_static_type); + REQUIRE(protected_final_instance_type); + REQUIRE(default_final_static_type); + } + THEN("Access modifiers of excluded methods are preserved.") + { + REQUIRE(public_instance_type->get_access() == ID_public); + REQUIRE(private_static_type->get_access() == ID_private); + REQUIRE(protected_final_instance_type->get_access() == ID_protected); + REQUIRE(default_final_static_type->get_access() == ID_default); + } + THEN("Static/Instance meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_bool(ID_is_static)); + REQUIRE(private_static_type->get_bool(ID_is_static)); + REQUIRE_FALSE(protected_final_instance_type->get_bool(ID_is_static)); + REQUIRE(default_final_static_type->get_bool(ID_is_static)); + } + THEN("Final/Non-final meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_is_final()); + REQUIRE_FALSE(private_static_type->get_is_final()); + REQUIRE(protected_final_instance_type->get_is_final()); + REQUIRE(default_final_static_type->get_is_final()); + } + } + } +}