46 const std::string &declarator)
override;
61 std::string dest=
"{ ";
67 components.size() == src.
operands().size(),
"component count mismatch");
69 exprt::operandst::const_iterator
o_it=src.
operands().begin();
74 for(
const auto &
c : components)
99 if(!
c.get_pretty_name().empty())
134 const std::string &declarator)
136 std::unique_ptr<c_qualifierst> clone =
qualifiers.clone();
140 const std::string d = declarator.empty() ? declarator : (
" " + declarator);
181 std::string dest =
q;
186 dest +=
"__interface";
191 if(!tag.
id().empty())
207 std::string dest =
q +
"union";
210 if(!tag.
id().empty())
224 return "constructor ";
228 return "destructor ";
230 else if(src.
id()==
"cpp-template-type")
236 std::string dest=
"template<";
240 for(
auto it = arguments.begin(); it != arguments.end(); ++it)
242 if(it!=arguments.begin())
269 return "std::nullptr_t";
277 std::string dest =
"(" +
convert(member) +
":: *)";
285 dest =
convert(return_type) +
" " + dest;
290 for(code_typet::parameterst::const_iterator it=args.begin();
303 dest =
convert(base_type) +
" " + dest + d;
320 std::string dest=
"auto";
331 for(code_typet::parameterst::const_iterator
332 it=parameters.begin();
333 it!=parameters.end();
336 if(it!=parameters.begin())
344 if(!parameters.empty())
352 dest+=
" -> "+
convert(return_type);
363 return q +
"bool" + d;
406 std::string dest=
indent_str(indent)+
"delete ";
425 if(src.
id()==
"cpp-this")
457 return "pod_constructor";
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::string MetaString(const std::string &in)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::vector< parametert > parameterst
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
std::string to_string() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
std::string convert_struct(const exprt &src, unsigned &precedence) override
std::string convert_code_cpp_new(const exprt &src, unsigned indent)
std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
expr2cppt(const namespacet &_ns)
std::string convert_code(const codet &src, unsigned indent) override
std::string convert_extractbit(const exprt &src)
std::string convert_cpp_new(const exprt &src)
std::string convert_cpp_this()
std::string convert_code_cpp_delete(const exprt &src, unsigned indent)
std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator) override
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)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
bool get_bool(const irep_idt &name) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
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.
cpp_namet & to_cpp_name(irept &cpp_name)
template_typet & to_template_type(typet &type)
std::string type2cpp(const typet &type, const namespacet &ns)
std::string expr2cpp(const exprt &expr, const namespacet &ns)
const std::string & id2string(const irep_idt &d)
void irep2lisp(const irept &src, lispexprt &dest)
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
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,...
API to expression classes.
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 code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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.