Go to the documentation of this file.
32 const exprt &src,
unsigned &precedence)
override;
47 const std::string &declarator)
override;
56 if(full_type.
id()!=ID_struct)
61 std::string dest=
"{ ";
66 assert(components.size()==src.
operands().size());
68 exprt::operandst::const_iterator o_it=src.
operands().begin();
73 for(
const auto &c : components)
75 if(c.type().id() == ID_code)
87 if(last_size+40<dest.size())
90 last_size=dest.size();
98 dest += c.get_string(ID_pretty_name);
113 unsigned &precedence)
115 if(src.
type().
id() == ID_c_bool)
130 const std::string &declarator)
132 std::unique_ptr<qualifierst> clone = qualifiers.
clone();
134 new_qualifiers.
read(src);
136 const std::string d = declarator.empty() ? declarator : (
" " + declarator);
149 else if(!src.
get(ID_C_c_type).
empty())
153 if(c_type == ID_bool)
158 else if(src.
id() == ID_struct)
164 else if(src.
get_bool(ID_C_interface))
173 else if(src.
id() == ID_struct_tag)
177 std::string dest = q;
181 else if(src.
get_bool(ID_C_interface))
182 dest +=
"__interface";
186 const irept &tag = struct_type.
find(ID_tag);
189 if(tag.
id() == ID_cpp_name)
199 else if(src.
id() == ID_union_tag)
203 std::string dest = q +
"union";
205 const irept &tag = union_type.
find(ID_tag);
208 if(tag.
id() == ID_cpp_name)
218 else if(src.
id()==ID_constructor)
220 return "constructor ";
222 else if(src.
id()==ID_destructor)
224 return "destructor ";
226 else if(src.
id()==
"cpp-template-type")
230 else if(src.
id()==ID_template)
232 std::string dest=
"template<";
236 for(
auto it = arguments.begin(); it != arguments.end(); ++it)
238 if(it!=arguments.begin())
243 if(argument.
id()==ID_symbol)
248 else if(argument.
id()==ID_type)
262 src.
id() == ID_pointer &&
265 return "std::nullptr_t";
271 member.
swap(tmp.
add(ID_to_member));
277 if(base_type.id() == ID_code)
286 for(code_typet::parameterst::const_iterator it=args.begin();
303 else if(src.
id()==ID_verilog_signedbv ||
304 src.
id()==ID_verilog_unsignedbv)
307 else if(src.
id()==ID_unassigned)
309 else if(src.
id()==ID_code)
316 std::string dest=
"auto";
327 for(code_typet::parameterst::const_iterator
328 it=parameters.begin();
329 it!=parameters.end();
332 if(it!=parameters.begin())
340 if(!parameters.empty())
348 dest+=
" -> "+
convert(return_type);
352 else if(src.
id()==ID_initializer_list)
357 else if(src.
id() == ID_c_bool)
359 return q +
"bool" + d;
374 if(src.
get(ID_statement)==ID_cpp_new_array)
378 std::string tmp_size=
402 std::string dest=
indent_str(indent)+
"delete ";
419 unsigned &precedence)
421 if(src.
id()==
"cpp-this")
426 if(src.
id()==ID_extractbit)
431 else if(src.
id()==ID_extractbits)
436 else if(src.
id()==ID_side_effect &&
437 (src.
get(ID_statement)==ID_cpp_new ||
438 src.
get(ID_statement)==ID_cpp_new_array))
443 else if(src.
id()==ID_side_effect &&
444 src.
get(ID_statement)==ID_throw)
455 else if(src.
id()==ID_unassigned)
457 else if(src.
id() == ID_pod_constructor)
458 return "pod_constructor";
469 if(statement==ID_cpp_delete ||
470 statement==ID_cpp_delete_array)
473 if(statement==ID_cpp_new ||
474 statement==ID_cpp_new_array)
483 return convert(extractbit_expr.op0()) +
"[" +
convert(extractbit_expr.op1()) +
490 return convert(extractbits_expr.src()) +
".range(" +
491 convert(extractbits_expr.upper()) +
"," +
492 convert(extractbits_expr.lower()) +
")";
expr2cppt(const namespacet &_ns)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
std::string MetaString(const std::string &in)
const componentst & components() const
void irep2lisp(const irept &src, lispexprt &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool has_ellipsis() const
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
std::string convert_extractbit(const exprt &src)
std::string convert_code_cpp_new(const exprt &src, unsigned indent)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
The type of an expression, extends irept.
std::vector< parametert > parameterst
const irept & find(const irep_idt &name) const
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Base class for all expressions.
std::vector< componentt > componentst
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string convert_code(const codet &src)
bool is_true() const
Return whether the expression is a constant representing true.
std::string expr2cpp(const exprt &expr, const namespacet &ns)
virtual void read(const typet &src)=0
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
bool is_false() const
Return whether the expression is a constant representing false.
const irep_idt & get(const irep_idt &name) const
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.
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
virtual std::string convert(const typet &src)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::string expr2string() const
std::string convert_struct(const exprt &src, unsigned &precedence) override
const std::string & id2string(const irep_idt &d)
static std::string indent_str(unsigned indent)
std::string type2cpp(const typet &type, const namespacet &ns)
virtual std::unique_ptr< qualifierst > clone() const =0
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const parameterst & parameters() const
std::string convert_cpp_new(const exprt &src)
std::string convert_norep(const exprt &src, unsigned &precedence)
bool is_reference(const typet &type)
Returns true if the type is a reference.
Structure type, corresponds to C style structs.
irept & add(const irep_idt &name)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool is_constant() const
Return whether the expression is a constant.
const typet & base_type() const
The type of the data what we point to.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const typet & return_type() const
There are a large number of kinds of tree structured or tree-like data in CPROVER.
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
virtual std::string as_string() const =0
std::string convert_extractbits(const exprt &src)
template_typet & to_template_type(typet &type)
A constant literal expression.
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
optionalt< std::string > convert_function(const exprt &src)
Returns a string if src is a function with a known conversion, else returns nullopt.
bool get_bool(const irep_idt &name) const
std::string to_string() const
cpp_namet & to_cpp_name(irept &cpp_name)
std::string convert_code(const codet &src, unsigned indent) override
std::string convert_cpp_this()
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.