113 for(
const auto &op : src.
operands())
156 return os << src.
pretty();
158 if(src.
op().has_operands())
159 return os <<
'(' <<
format(src.
op()) <<
')';
175 auto type = src.
type().
id();
182 return os <<
"false";
184 return os << src.
pretty();
204 return os <<
"INVALID-POINTER";
220 return os << src.
pretty();
229 os <<
' ' << s.first <<
"=\"" << s.second.id() <<
'"';
236 for(
const auto &op : expr.
operands())
261 std::function<std::ostream &(std::ostream &,
const exprt &)>;
262 using expr_mapt = std::unordered_map<irep_idt, formattert>;
282 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
293 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
308 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
317 auto unary_expr = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
325 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
335 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
346 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
351 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
357 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
363 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
365 <<
format(expr.type()) <<
')';
369 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
377 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
387 auto byte_update = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
399 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
405 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
410 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
417 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
422 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
437 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
458 const auto &values =
let_expr.values();
475 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
495 auto compound = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
500 for(
const auto &op : expr.operands())
517 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
530 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
531 return os <<
'"' << expr.get_string(
ID_value) <<
'"';
535 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
552 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
555 if(dereference_expr.pointer().id() !=
ID_symbol)
556 os <<
'(' <<
format(dereference_expr.pointer()) <<
')';
558 os <<
format(dereference_expr.pointer());
563 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
570 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
577 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
584 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
590 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
596 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
602 fallback = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
API to expression classes for bitvectors.
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for binary expressions.
std::size_t get_width() const
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
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.
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
named_subt & get_named_sub()
A base class for multi-ary expressions Associativity is not specified.
const typet & base_type() const
The type of the data what we point to.
An expression with three operands.
Generic base class for unary expressions.
bool has_prefix(const std::string &s, const std::string &prefix)
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.