Mark abstract classes as such

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(

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

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) \

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(){
+
+  }
+}

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 <catch.hpp>
+
+#include <istream>
+#include <memory>
+
+#include <util/config.h>
+#include <util/language.h>
+#include <util/message.h>
+#include <java_bytecode/java_bytecode_language.h>
+
+SCENARIO("java_bytecode_convert_abstract_class",
+  "[core][java_bytecode][java_bytecode_convert_class]")
+{
+  std::unique_ptr<languaget>java_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());
+      }
+    }
+  }
+}