10 #ifndef CPROVER_JAVA_BYTECODE_EXPR2JAVA_H 11 #define CPROVER_JAVA_BYTECODE_EXPR2JAVA_H 28 const exprt &src,
unsigned &precedence)
override;
34 const exprt &src,
unsigned &precedence)
override;
45 const std::string &declarator)
override;
58 template <
typename float_type>
61 const bool is_float = std::is_same<float_type, float>::value;
62 const std::string class_name = is_float ?
"Float" :
"Double";
64 return class_name +
".NaN";
65 if(std::isinf(value) && value >= 0.)
66 return class_name +
".POSITIVE_INFINITY";
67 if(std::isinf(value) && value <= 0.)
68 return class_name +
".NEGATIVE_INFINITY";
69 const std::string decimal = [&]() -> std::string {
72 std::ostringstream raw_stream;
74 const auto raw_decimal = raw_stream.str();
75 if(raw_decimal.find(
'.') == std::string::npos)
76 return raw_decimal +
".0";
79 const bool is_lossless = [&] {
80 if(value == std::numeric_limits<float_type>::min())
84 return std::stod(decimal) == value;
86 catch(std::out_of_range &)
91 const std::string lossless = [&]() -> std::string {
94 std::ostringstream stream;
95 stream << std::hexfloat << value;
98 const auto literal = is_float ? lossless +
'f' : lossless;
101 return literal +
" /* " + decimal +
" */";
104 #endif // CPROVER_JAVA_BYTECODE_EXPR2JAVA_H virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
The type of an expression, extends irept.
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
expr2javat(const namespacet &_ns)
std::string convert_java_new(const exprt &src, unsigned precedence)
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
std::string convert_java_instanceof(const exprt &src, unsigned precedence)
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
virtual std::string convert_code(const codet &src, unsigned indent) override
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
A constant literal expression.
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
std::string type2java(const typet &type, const namespacet &ns)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
codet representation of a function call statement.
const std::size_t char_representation_length
floatbv_typet float_type()
virtual std::string convert(const typet &src) override
Base class for all expressions.
std::string expr2java(const exprt &expr, const namespacet &ns)
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Data structure for representing an arbitrary statement in a program.
std::string convert_java_this(const exprt &src, unsigned precedence)