83 if(has_this && it==arguments.begin())
117 std::string dest=
"{ ";
123 components.size() == src.
operands().size(),
124 "inconsistent number of components");
126 exprt::operandst::const_iterator
o_it=src.
operands().begin();
131 for(
const auto &
c : components)
134 c.type().id() !=
ID_code,
"struct member must not be of code type");
209 std::string dest=
"(byte)";
217 std::string dest=
"(short)";
246 const std::string &declarator)
248 std::unique_ptr<c_qualifierst> clone =
qualifiers.clone();
252 const std::string d = declarator.empty() ? declarator : (
" " + declarator);
272 return q+
"boolean"+d;
288 for(java_method_typet::parameterst::const_iterator it = parameters.begin();
289 it != parameters.end();
292 if(it!=parameters.begin())
300 if(!parameters.empty())
308 dest+=
" -> "+
convert(return_type);
362 std::string dest=
indent_str(indent)+
"delete ";
381 if(src.
id()==
"java-this")
408 const exprt &catch_expr=
410 return "catch_landingpad("+
418 else if(src.
id()==
"pod_constructor")
419 return "pod_constructor";
std::string MetaString(const std::string &in)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
An expression describing a method on a class.
goto_instruction_codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::optional< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
static std::string indent_str(unsigned indent)
std::string convert_code(const codet &src)
std::string convert_norep(const exprt &src, unsigned &precedence)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
virtual std::string convert(const typet &src)
std::string convert_code_java_new(const exprt &src, unsigned precedence)
std::string convert_java_new(const exprt &src)
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
const std::size_t char_representation_length
virtual std::string convert_code(const codet &src, unsigned indent) override
std::string convert_java_instanceof(const exprt &src)
virtual std::string convert(const typet &src) override
std::string convert_java_this()
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
An IEEE 754 floating-point value, including specificiation.
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
std::vector< parametert > parameterst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
The type of an expression, extends irept.
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
#define forall_expr(it, expr)
const code_function_callt & to_code_function_call(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
Java-specific exprt subclasses.
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
Java-specific type qualifiers.
Representation of a constant Java string.
signedbv_typet java_int_type()
signedbv_typet java_byte_type()
signedbv_typet java_short_type()
floatbv_typet java_double_type()
floatbv_typet java_float_type()
c_bool_typet java_boolean_type()
unsignedbv_typet java_char_type()
signedbv_typet java_long_type()
const java_method_typet & to_java_method_type(const typet &type)
const std::string integer2string(const mp_integer &n, unsigned base)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
static code_landingpadt & to_code_landingpad(codet &code)
const codet & to_code(const exprt &expr)
API to expression classes.
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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...