From 32b67000d4bf725e7fd91426263ee40defcc8fe3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 Mar 2016 22:55:16 +0100 Subject: [PATCH] Java bytecode: use expr2java instead of expr2c, formatting fix --- src/java_bytecode/java_bytecode_typecheck.cpp | 7 +++---- src/java_bytecode/java_entry_point.h | 9 +++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index 9b8d559cddd..ea8d4c6d7f9 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/src/java_bytecode/java_bytecode_typecheck.cpp @@ -10,8 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - +#include "expr2java.h" #include "java_bytecode_typecheck.h" /*******************************************************************\ @@ -28,7 +27,7 @@ Function: java_bytecode_typecheckt::to_string std::string java_bytecode_typecheckt::to_string(const exprt &expr) { - return expr2c(expr, ns); + return expr2java(expr, ns); } /*******************************************************************\ @@ -45,7 +44,7 @@ Function: java_bytecode_typecheckt::to_string std::string java_bytecode_typecheckt::to_string(const typet &type) { - return type2c(type, ns); + return type2java(type, ns); } /*******************************************************************\ diff --git a/src/java_bytecode/java_entry_point.h b/src/java_bytecode/java_entry_point.h index 68a5274783f..52585b52896 100644 --- a/src/java_bytecode/java_entry_point.h +++ b/src/java_bytecode/java_entry_point.h @@ -1,9 +1,10 @@ -/******************************************************************* - Module: +/*******************************************************************\ - Author: Daniel Kroening, kroening@kroening.com +Module: - \*******************************************************************/ +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ #ifndef CPROVER_JAVA_ENTRY_POINT_H #define CPROVER_JAVA_ENTRY_POINT_H