formatter for Java

Author: Daniel Kroening

src/java_bytecode/Makefile

@@ -22,6 +22,7 @@ SRC = bytecode_info.cpp \
       java_class_loader_limit.cpp \
       java_enum_static_init_unwind_handler.cpp \
       java_entry_point.cpp \
+      java_formatter.cpp \
       java_local_variable_table.cpp \
       java_object_factory.cpp \
       java_pointer_casts.cpp \

src/java_bytecode/java_formatter.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "java_formatter.h"
+
+#include "expr2java.h"
+
+#include <ostream>
+
+std::ostream &java_formattert::format(std::ostream &os, const exprt &expr)
+{
+  return os << expr2java(expr, ns);
+}
+
+std::ostream &java_formattert::format(std::ostream &os, const typet &type)
+{
+  return os << type2java(type, ns);
+}
+
+std::ostream &
+java_formattert::format(std::ostream &os, const source_locationt &loc)
+{
+  return os << loc;
+}

src/java_bytecode/java_formatter.h

@@ -0,0 +1,28 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_FORMATTER_H
+#define CPROVER_JAVA_FORMATTER_H
+
+#include <util/formatter.h>
+
+class java_formattert : public formattert
+{
+public:
+  explicit java_formattert(const namespacet &_ns) : ns(_ns)
+  {
+  }
+
+  std::ostream &format(std::ostream &, const exprt &) override;
+  std::ostream &format(std::ostream &, const typet &) override;
+  std::ostream &format(std::ostream &, const source_locationt &) override;
+
+  const namespacet &ns;
+};
+
+#endif // CPROVER_JAVA_FORMATTER_H