Go to the documentation of this file.
88 if(has_this && it==arguments.begin())
111 unsigned &precedence)
115 if(full_type.
id()!=ID_struct)
120 std::string dest=
"{ ";
125 assert(components.size()==src.
operands().size());
127 exprt::operandst::const_iterator o_it=src.
operands().begin();
132 for(
const auto &c : components)
134 if(c.type().id() != ID_code)
136 std::string tmp=
convert(*o_it);
143 if(last_size+40<dest.size())
146 last_size=dest.size();
154 irep_idt field_name = c.get_pretty_name();
155 if(field_name.
empty())
156 field_name = c.get_name();
172 unsigned &precedence)
174 if(src.
type().
id()==ID_c_bool)
181 else if(src.
type().
id()==ID_bool)
188 else if(src.
type().
id()==ID_pointer)
199 const char16_t int_value = numeric_cast_v<char16_t>(src);
209 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
210 std::string dest=
"(byte)";
217 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
218 std::string dest=
"(short)";
225 const mp_integer int_value = numeric_cast_v<mp_integer>(src);
247 const std::string &declarator)
249 std::unique_ptr<qualifierst> clone = qualifiers.
clone();
251 new_qualifiers.
read(src);
253 const std::string d = declarator.empty() ? declarator : (
" " + declarator);
273 return q+
"boolean"+d;
276 else if(src.
id()==ID_code)
289 for(java_method_typet::parameterst::const_iterator it = parameters.begin();
290 it != parameters.end();
293 if(it!=parameters.begin())
301 if(!parameters.empty())
309 dest+=
" -> "+
convert(return_type);
326 return convert(instanceof_expr.tested_expr()) +
" instanceof " +
327 convert(instanceof_expr.target_type());
339 if(src.
get(ID_statement)==ID_java_new_array ||
340 src.
get(ID_statement)==ID_java_new_array_data)
344 std::string tmp_size=
363 std::string dest=
indent_str(indent)+
"delete ";
380 unsigned &precedence)
382 if(src.
id()==
"java-this")
387 if(src.
id()==ID_java_instanceof)
392 else if(src.
id()==ID_side_effect &&
393 (src.
get(ID_statement)==ID_java_new ||
394 src.
get(ID_statement)==ID_java_new_array ||
395 src.
get(ID_statement)==ID_java_new_array_data))
400 else if(src.
id()==ID_side_effect &&
401 src.
get(ID_statement)==ID_throw)
406 else if(src.
id()==ID_code &&
407 to_code(src).get_statement()==ID_exception_landingpad)
409 const exprt &catch_expr=
411 return "catch_landingpad("+
417 else if(src.
id()==ID_unassigned)
419 else if(src.
id()==
"pod_constructor")
420 return "pod_constructor";
421 else if(src.
id()==ID_virtual_function)
429 const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))
433 else if(src.
id()==ID_constant)
445 if(statement==ID_java_new ||
446 statement==ID_java_new_array)
449 if(statement==ID_function_call)
std::string MetaString(const std::string &in)
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool has_ellipsis() const
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
std::string convert_java_new(const exprt &src)
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
std::string convert_java_this()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
signedbv_typet java_long_type()
virtual std::string convert(const typet &src) override
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
const irept & find(const irep_namet &name) const
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
Representation of a constant Java string.
std::vector< parametert > parameterst
Base class for all expressions.
std::vector< componentt > componentst
Java-specific exprt subclasses.
std::string convert_code(const codet &src)
bool is_true() const
Return whether the expression is a constant representing true.
virtual void read(const typet &src)=0
std::string convert_java_instanceof(const exprt &src)
bool is_false() const
Return whether the expression is a constant representing false.
const codet & to_code(const exprt &expr)
An expression describing a method on a class.
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
virtual std::string convert(const typet &src)
const std::string & id2string(const irep_idt &d)
static std::string indent_str(unsigned indent)
std::string convert_function(const exprt &src, const std::string &symbol)
virtual std::unique_ptr< qualifierst > clone() const =0
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
signedbv_typet java_int_type()
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
const parameterst & parameters() const
signedbv_typet java_short_type()
const exprt & catch_expr() const
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
signedbv_typet java_byte_type()
std::string convert_norep(const exprt &src, unsigned &precedence)
bool is_zero() const
Return whether the expression is a constant representing 0.
static code_landingpadt & to_code_landingpad(codet &code)
Structure type, corresponds to C style structs.
floatbv_typet java_double_type()
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
virtual std::string convert_code(const codet &src, unsigned indent) override
unsignedbv_typet java_char_type()
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
c_bool_typet java_boolean_type()
const typet & return_type() const
#define forall_expr(it, expr)
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
const java_method_typet & to_java_method_type(const typet &type)
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Escapes non-printable characters, whitespace except for spaces, double- and single-quotes and backsla...
virtual std::string as_string() const =0
A constant literal expression.
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
const std::size_t char_representation_length
API to expression classes.
Java-specific type qualifiers.
floatbv_typet java_float_type()
std::string convert_code_java_new(const exprt &src, unsigned precedence)
Data structure for representing an arbitrary statement in a program.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const std::string integer2string(const mp_integer &n, unsigned base)