Skip to content

Commit b45fe75

Browse files
Unit tests conversion from code_typet to java_method_typet
1 parent c652ce6 commit b45fe75

File tree

2 files changed

+36
-0
lines changed

2 files changed

+36
-0
lines changed

jbmc/unit/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \
2121
java_bytecode/java_types/erase_type_arguments.cpp \
2222
java_bytecode/java_types/generic_type_index.cpp \
2323
java_bytecode/java_types/java_generic_symbol_type.cpp \
24+
java_bytecode/java_types/java_method_type.cpp \
2425
java_bytecode/java_types/java_type_from_string.cpp \
2526
java_bytecode/java_utils_test.cpp \
2627
java_bytecode/load_method_by_regex.cpp \
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
/*******************************************************************\
2+
3+
Module: Unit tests for java_types
4+
5+
Author: Diffblue Ltd.
6+
7+
\*******************************************************************/
8+
9+
#include <testing-utils/catch.hpp>
10+
#include <java_bytecode/java_types.h>
11+
12+
SCENARIO("java_method_type", "[core][java_types]")
13+
{
14+
GIVEN("A code_typet")
15+
{
16+
code_typet::parameterst parameters;
17+
typet return_type;
18+
code_typet code_type = code_typet();
19+
THEN("It has id code_typet and not java_method_typet")
20+
{
21+
REQUIRE(code_type.id() == ID_code);
22+
REQUIRE_FALSE(code_type.get_bool(ID_C_java_method_type));
23+
}
24+
25+
WHEN("It is converted to a java_method_typet")
26+
{
27+
THEN("It should have id code_typet and java_method_typet")
28+
{
29+
java_method_typet method_type = to_java_method_type(code_type);
30+
REQUIRE(method_type.id() == ID_code);
31+
REQUIRE(method_type.get_bool(ID_C_java_method_type));
32+
}
33+
}
34+
}
35+
}

0 commit comments

Comments
 (0)