diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp index e64314cacec..3f9e4a77349 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp @@ -7,7 +7,12 @@ Author: Diffblue Ltd. \*******************************************************************/ #include + +#include +#include +#include #include +#include SCENARIO("is_clinit_function", "[core][java_static_initializers]") { @@ -52,3 +57,105 @@ SCENARIO( } } } + +SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]") +{ + json_objectt static_values_json{}; + symbol_tablet symbol_table; + const std::size_t max_user_array_length = 100; + std::unordered_map references; + std::unordered_multimap class_to_declared_symbols; + + GIVEN( + "A class which has no entry in the JSON object but a clinit defined " + "in the symbol table") + { + symbolt clinit_symbol; + clinit_symbol.name = "java::TestClass.:()V"; + symbol_table.insert(clinit_symbol); + + const code_blockt clinit_body = get_user_specified_clinit_body( + "java::TestClass", + static_values_json, + symbol_table, + {}, + max_user_array_length, + references, + class_to_declared_symbols); + + THEN("User provided clinit body is composed of one call to clinit") + { + const exprt function_called = + make_query(clinit_body)[0].as().get().function(); + REQUIRE( + make_query(function_called).as().get().get_identifier() == + clinit_symbol.name); + } + } + GIVEN("A class which has no entry in the JSON object and no clinit defined") + { + const auto clinit_body = get_user_specified_clinit_body( + "java::TestClass", + static_values_json, + symbol_table, + {}, + max_user_array_length, + references, + class_to_declared_symbols); + + THEN("User provided clinit body is empty") + { + REQUIRE(clinit_body == code_blockt{}); + } + } + GIVEN("A class which has a static number in the provided JSON") + { + static_values_json["TestClass"] = [] { + json_objectt entry{}; + entry["field_name"] = json_numbert{"42"}; + return entry; + }(); + class_to_declared_symbols.emplace("java::TestClass", [] { + symbolt field_symbol; + field_symbol.base_name = "field_name"; + field_symbol.name = "field_name_for_codet"; + field_symbol.type = java_int_type(); + field_symbol.is_static_lifetime = true; + return field_symbol; + }()); + symbol_table.insert([] { + symbolt clinit_symbol; + clinit_symbol.name = "java::TestClass.:()V"; + set_declaring_class(clinit_symbol, "java::TestClass"); + return clinit_symbol; + }()); + symbol_table.insert([] { + symbolt test_class_symbol; + test_class_symbol.name = "java::TestClass"; + test_class_symbol.type = [] { + java_class_typet type; + type.components().emplace_back("field_name", java_int_type()); + return type; + }(); + return test_class_symbol; + }()); + const auto clinit_body = get_user_specified_clinit_body( + "java::TestClass", + static_values_json, + symbol_table, + {}, + max_user_array_length, + references, + class_to_declared_symbols); + THEN("User provided clinit body set the field to the given value") + { + auto assignment = make_query(clinit_body)[0].as().get(); + REQUIRE( + make_query(assignment.lhs()) + .as() + .get() + .get_identifier() == "field_name_for_codet"); + REQUIRE(assignment.rhs() == from_integer(42, java_int_type())); + } + } +} diff --git a/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt b/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt index 7c65cd85bde..58b93bbf8f1 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt @@ -1,2 +1,3 @@ java_bytecode testing-utils +util diff --git a/unit/testing-utils/expr_query.h b/unit/testing-utils/expr_query.h index 684a6a53e75..41ce00bf410 100644 --- a/unit/testing-utils/expr_query.h +++ b/unit/testing-utils/expr_query.h @@ -54,7 +54,7 @@ class expr_queryt T value; }; -expr_queryt make_query(exprt e) +inline expr_queryt make_query(exprt e) { return expr_queryt(std::move(e)); }