diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 9b6d53841e3..77c6e432e80 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -93,6 +93,7 @@ void java_bytecode_convert_classt::convert(const classt &c) class_type.set_tag(c.name); class_type.set(ID_base_name, c.name); + class_type.set(ID_abstract, c.is_abstract); if(c.is_enum) { class_type.set( diff --git a/src/util/std_types.h b/src/util/std_types.h index 1f5b16ee1ea..5c244e6728e 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -401,6 +401,11 @@ class class_typet:public struct_typet return false; } + + bool is_abstract() const + { + return get_bool(ID_abstract); + } }; /*! \brief Cast a generic typet to a \ref class_typet diff --git a/unit/Makefile b/unit/Makefile index e11ed07e96d..8f428b055d6 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -2,6 +2,7 @@ SRC = unit_tests.cpp \ catch_example.cpp \ + java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ # Empty last line @@ -14,7 +15,9 @@ include ../src/common cprover.dir: $(MAKE) $(MAKEARGS) -C ../src -LIBS += ../src/ansi-c/ansi-c$(LIBEXT) \ +LIBS += ../src/java_bytecode/java_bytecode$(LIBEXT) \ + ../src/miniz/miniz$(OBJEXT) \ + ../src/ansi-c/ansi-c$(LIBEXT) \ ../src/cpp/cpp$(LIBEXT) \ ../src/json/json$(LIBEXT) \ ../src/linking/linking$(LIBEXT) \ diff --git a/unit/java_bytecode/java_bytecode_convert_class/A.class b/unit/java_bytecode/java_bytecode_convert_class/A.class new file mode 100644 index 00000000000..9684f38ea7c Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/A.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/C.class b/unit/java_bytecode/java_bytecode_convert_class/C.class new file mode 100644 index 00000000000..70de87e848a Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/C.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java b/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java new file mode 100644 index 00000000000..a7816923faa --- /dev/null +++ b/unit/java_bytecode/java_bytecode_convert_class/ExampleClasses.java @@ -0,0 +1,32 @@ +interface I +{ + void interface_method(); +} + +abstract class A +{ + abstract void method(); + + int i; +} + +class C +{ + + int j; + void concreteMethod() { + + } +} + +class Extendor extends A { + void method() { + + } +} + +class Implementor implements I { + public void interface_method(){ + + } +} \ No newline at end of file diff --git a/unit/java_bytecode/java_bytecode_convert_class/Extendor.class b/unit/java_bytecode/java_bytecode_convert_class/Extendor.class new file mode 100644 index 00000000000..3986820feee Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/Extendor.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/I.class b/unit/java_bytecode/java_bytecode_convert_class/I.class new file mode 100644 index 00000000000..550de7e7469 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/I.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/Implementor.class b/unit/java_bytecode/java_bytecode_convert_class/Implementor.class new file mode 100644 index 00000000000..1c85bca08ae Binary files /dev/null and b/unit/java_bytecode/java_bytecode_convert_class/Implementor.class differ diff --git a/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp new file mode 100644 index 00000000000..71f39dfc937 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp @@ -0,0 +1,149 @@ +/*******************************************************************\ + + Module: Unit tests for converting abstract classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include +#include + +#include +#include +#include +#include + +SCENARIO("java_bytecode_convert_abstract_class", + "[core][java_bytecode][java_bytecode_convert_class]") +{ + std::unique_ptrjava_lang(new_java_bytecode_language()); + + // Configure the path loading + cmdlinet command_line; + command_line.set( + "java-cp-include-files", + "./java_bytecode/java_bytecode_convert_class"); + config.java.classpath.push_back( + "./java_bytecode/java_bytecode_convert_class"); + + // Configure the language + null_message_handlert message_handler; + java_lang->get_language_options(command_line); + java_lang->set_message_handler(message_handler); + + std::istringstream java_code_stream("ignored"); + + GIVEN("Some class files in the class path") + { + WHEN("Parsing an interface") + { + java_lang->parse(java_code_stream, "I.class"); + + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + + java_lang->final(new_symbol_table); + + REQUIRE(new_symbol_table.has_symbol("java::I")); + THEN("The symbol type should be abstract") + { + const symbolt &class_symbol=new_symbol_table.lookup("java::I"); + const typet &symbol_type=class_symbol.type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + REQUIRE(class_type.is_abstract()); + } + } + WHEN("Parsing an abstract class") + { + java_lang->parse(java_code_stream, "A.class"); + + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + + java_lang->final(new_symbol_table); + + REQUIRE(new_symbol_table.has_symbol("java::A")); + THEN("The symbol type should be abstract") + { + const symbolt &class_symbol=new_symbol_table.lookup("java::A"); + const typet &symbol_type=class_symbol.type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + REQUIRE(class_type.is_abstract()); + } + } + WHEN("Passing a concrete class") + { + java_lang->parse(java_code_stream, "C.class"); + + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + + java_lang->final(new_symbol_table); + + REQUIRE(new_symbol_table.has_symbol("java::C")); + THEN("The symbol type should not be abstract") + { + const symbolt &class_symbol=new_symbol_table.lookup("java::C"); + const typet &symbol_type=class_symbol.type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + REQUIRE_FALSE(class_type.is_abstract()); + } + } + WHEN("Passing a concrete class that implements an interface") + { + java_lang->parse(java_code_stream, "Implementor.class"); + + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + + java_lang->final(new_symbol_table); + + REQUIRE(new_symbol_table.has_symbol("java::Implementor")); + THEN("The symbol type should not be abstract") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::Implementor"); + const typet &symbol_type=class_symbol.type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + REQUIRE_FALSE(class_type.is_abstract()); + } + } + WHEN("Passing a concrete class that extends an abstract class") + { + java_lang->parse(java_code_stream, "Extendor.class"); + + symbol_tablet new_symbol_table; + java_lang->typecheck(new_symbol_table, ""); + + java_lang->final(new_symbol_table); + + REQUIRE(new_symbol_table.has_symbol("java::Extendor")); + THEN("The symbol type should not be abstract") + { + const symbolt &class_symbol= + new_symbol_table.lookup("java::Extendor"); + const typet &symbol_type=class_symbol.type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + REQUIRE_FALSE(class_type.is_abstract()); + } + } + } +}