41 std::vector<mp_integer> bytes;
44 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
45 bytes.push_back((value >> bit)%
power(2, bits_per_byte));
49 for(std::size_t bit = 0; bit < width; bit += bits_per_byte)
53 "bytes is not empty because we just pushed just as many elements on "
54 "top of it as we are popping now");
55 new_value+=bytes.back()<<bit;
77 type_id == ID_integer || type_id == ID_natural ||
78 type_id == ID_unsignedbv || type_id == ID_signedbv)
87 else if(type_id==ID_rational)
96 else if(type_id==ID_fixedbv)
103 else if(type_id==ID_floatbv)
127 type_id == ID_integer || type_id == ID_natural ||
128 type_id == ID_unsignedbv || type_id == ID_signedbv)
137 else if(type_id==ID_rational)
146 else if(type_id==ID_fixedbv)
153 else if(type_id==ID_floatbv)
175 bool no_change =
true;
178 exprt::operandst::iterator constant;
181 bool constant_found =
false;
183 std::optional<typet> c_sizeof_type;
186 for(exprt::operandst::iterator it = new_operands.begin();
187 it != new_operands.end();)
196 it->type().id()!=ID_floatbv)
202 bool do_erase =
false;
205 if(it->is_constant() && it->type()==expr.
type())
208 if(!c_sizeof_type.has_value())
210 const typet &sizeof_type =
211 static_cast<const typet &
>(it->find(ID_C_c_sizeof_type));
213 c_sizeof_type = sizeof_type;
226 constant_found =
true;
233 it = new_operands.erase(it);
240 if(c_sizeof_type.has_value())
244 "c_sizeof_type is only set to a non-nil value "
245 "if a constant has been found");
246 constant->set(ID_C_c_sizeof_type, *c_sizeof_type);
249 if(new_operands.size() == 1)
251 return new_operands.front();
256 if(constant_found && constant->is_one())
259 new_operands.erase(constant);
262 if(new_operands.size() == 1)
263 return new_operands.front();
272 tmp.
operands() = std::move(new_operands);
273 return std::move(tmp);
284 if(expr_type!=expr.
op0().
type() ||
290 if(expr_type.
id()==ID_signedbv ||
291 expr_type.
id()==ID_unsignedbv ||
292 expr_type.
id()==ID_natural ||
293 expr_type.
id()==ID_integer)
299 if(int_value1.has_value() && *int_value1 == 0)
303 if(int_value1.has_value() && *int_value1 == 1)
309 if(int_value0.has_value() && *int_value0 == 0)
314 if(int_value0.has_value() && int_value1.has_value())
316 mp_integer result = *int_value0 / *int_value1;
320 else if(expr_type.
id()==ID_rational)
328 if(ok1 && rat_value1.
is_zero())
331 if((ok1 && rat_value1.
is_one()) ||
343 return std::move(tmp);
346 else if(expr_type.
id()==ID_fixedbv)
376 if(expr.
type().
id()==ID_signedbv ||
377 expr.
type().
id()==ID_unsignedbv ||
378 expr.
type().
id()==ID_natural ||
379 expr.
type().
id()==ID_integer)
387 if(int_value1.has_value() && *int_value1 == 0)
391 (int_value1.has_value() && *int_value1 == 1) ||
392 (int_value0.has_value() && *int_value0 == 0))
397 if(int_value0.has_value() && int_value1.has_value())
399 mp_integer result = *int_value0 % *int_value1;
413 bool no_change =
true;
420 if(expr.
type().
id() == ID_floatbv)
425 const exprt::operandst::iterator next = std::next(it);
427 if(next != new_operands.end())
429 if(it->type()==next->type() &&
434 new_operands.erase(next);
445 expr.
op0().
id() == ID_plus && expr.
op0().
type().
id() == ID_pointer &&
449 if(
as_const(result).op0().type().
id() != ID_pointer)
453 if(op1.
id() == ID_plus)
472 for(
const auto &op : expr.
operands())
474 if(
is_number(op.type()) && op.is_constant())
481 exprt::operandst::iterator const_sum;
482 bool const_sum_set=
false;
484 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
486 if(
is_number(it->type()) && it->is_constant())
508 typedef std::unordered_map<exprt, exprt::operandst::iterator, irep_hash>
512 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
513 if(it->id() == ID_unary_minus)
519 for(
auto it = new_operands.begin(); it != new_operands.end(); it++)
523 else if(it->id()==ID_unary_minus)
526 expr_mapt::iterator itm=expr_map.find(*it);
528 if(itm!=expr_map.end())
540 for(exprt::operandst::iterator it = new_operands.begin();
541 it != new_operands.end();
544 if(
is_number(it->type()) && it->is_zero())
546 it = new_operands.erase(it);
554 if(new_operands.empty())
558 else if(new_operands.size() == 1)
560 return new_operands.front();
568 tmp.
operands() = std::move(new_operands);
569 return std::move(tmp);
577 if(!
is_number(minus_expr.type()) && minus_expr.type().id() != ID_pointer)
592 minus_expr.type().id() == ID_pointer &&
593 operands[0].type().id() == ID_pointer &&
is_number(operands[1].type()))
603 is_number(minus_expr.type()) && operands[0].type().id() == ID_pointer &&
604 operands[1].type().id() == ID_pointer)
610 if(ptr_op0 == ptr_op1 && address_of)
623 offset_op0.
is_constant() && offset_op1.is_constant() &&
624 object_size.has_value() && element_size.has_value() &&
625 element_size->is_constant() && !element_size->is_zero() &&
652 element_size.has_value() && element_size->is_constant() &&
653 !element_size->is_zero())
676 for(
const auto &op : expr.
operands())
681 else if(op.is_zero() || op.is_one())
693 if(expr.
id()==ID_bitand)
695 else if(expr.
id()==ID_bitor)
697 else if(expr.
id()==ID_bitxor)
699 else if(expr.
id() == ID_bitxnor)
700 new_expr.
id(ID_equal);
706 if(it->id()==ID_typecast)
708 else if(it->is_zero())
710 else if(it->is_one())
721 bool no_change =
true;
722 auto new_expr = expr;
728 while(new_expr.operands().size() >= 2)
730 if(!new_expr.op0().is_constant())
733 if(!new_expr.op1().is_constant())
736 if(new_expr.op0().type() != new_expr.type())
739 if(new_expr.op1().type() != new_expr.type())
745 std::function<bool(
bool,
bool)> f;
747 if(new_expr.id() == ID_bitand)
748 f = [](
bool a,
bool b) {
return a && b; };
749 else if(new_expr.id() == ID_bitor)
750 f = [](
bool a,
bool b) {
return a || b; };
751 else if(new_expr.id() == ID_bitxor)
752 f = [](
bool a,
bool b) {
return a != b; };
753 else if(new_expr.id() == ID_bitxnor)
754 f = [](
bool a,
bool b) {
return a == b; };
759 make_bvrep(width, [&a_val, &b_val, &width, &f](std::size_t i) {
767 new_expr.operands().erase(new_expr.operands().begin());
768 new_expr.op0().swap(new_op);
775 if(new_expr.id() == ID_bitor || new_expr.id() == ID_bitxor)
777 for(exprt::operandst::iterator it = new_expr.operands().begin();
778 it != new_expr.operands().end();)
780 if(it->is_zero() && new_expr.operands().size() > 1)
782 it = new_expr.operands().erase(it);
786 it->is_constant() && it->type().id() == ID_bv &&
788 new_expr.operands().size() > 1)
790 it = new_expr.operands().erase(it);
800 if(new_expr.id() == ID_bitand)
802 const auto all_ones =
power(2, width) - 1;
803 for(exprt::operandst::iterator it = new_expr.operands().begin();
804 it != new_expr.operands().end();)
810 new_expr.operands().size() > 1)
812 it = new_expr.operands().erase(it);
822 if(new_expr.operands().size() == 2 && new_expr.op0() == new_expr.op1())
824 if(new_expr.id() == ID_bitand || new_expr.id() == ID_bitor)
826 return new_expr.op0();
828 else if(new_expr.id() == ID_bitxor)
834 if(new_expr.operands().size() == 1)
835 return new_expr.op0();
840 return std::move(new_expr);
855 !index_converted_to_int.has_value() || *index_converted_to_int < 0 ||
856 *index_converted_to_int >= src_bit_width)
875 bool no_change =
true;
887 const bool value = op.
is_true();
896 while(i < new_expr.
operands().size() - 1)
911 const auto new_width = width_i + width_n;
914 new_width, [&value_i, &value_n, width_i, width_n](std::size_t x) {
964 else if(new_expr.
type().
id() == ID_verilog_unsignedbv)
969 while(i < new_expr.
operands().size() - 1)
980 const std::string new_value=
982 opi.
set(ID_value, new_value);
984 opi.
type().
id(ID_verilog_unsignedbv);
998 return new_expr.
op0();
1009 return std::move(new_expr);
1032 if(!distance.has_value())
1041 !value.has_value() && expr.
op().
type().
id() == ID_bv &&
1049 if(!value.has_value())
1053 expr.
op().
type().
id() == ID_unsignedbv ||
1058 if(expr.
id()==ID_lshr)
1061 if(*distance >= width)
1065 else if(*distance >= 0)
1068 *value +=
power(2, width);
1069 *value /=
power(2, *distance);
1073 else if(expr.
id()==ID_ashr)
1082 else if(expr.
id()==ID_shl)
1085 if(*distance >= width)
1089 else if(*distance >= 0)
1091 *value *=
power(2, *distance);
1097 expr.
op().
type().
id() == ID_integer || expr.
op().
type().
id() == ID_natural)
1099 if(expr.
id()==ID_lshr)
1103 *value /=
power(2, *distance);
1107 else if(expr.
id()==ID_ashr)
1113 if(*value < 0 && new_value == 0)
1119 else if(expr.
id()==ID_shl)
1123 *value *=
power(2, *distance);
1141 if(!exponent.has_value())
1144 if(exponent.value() == 0)
1147 if(exponent.value() == 1)
1150 if(!base.has_value())
1173 if(!end.has_value())
1178 if(!width.has_value())
1183 if(!result_width.has_value())
1186 const auto start = std::optional(*end + *result_width - 1);
1188 if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
1191 DATA_INVARIANT(*start >= *end,
"extractbits must have start >= end");
1197 if(!svalue.has_value() || svalue->size() != *width)
1200 std::string extracted_value = svalue->substr(
1205 if(!result.has_value())
1208 return std::move(*result);
1210 else if(expr.
src().
id() == ID_concatenation)
1220 if(!op_width.has_value() || *op_width <= 0)
1223 if(*start < offset && offset <= *end + *op_width)
1232 offset -= *op_width;
1237 if(eb_src->index().is_constant())
1247 else if(*end == 0 && *start + 1 == *width)
1269 const exprt &operand = expr.
op();
1274 if(operand.
id()==ID_unary_minus)
1287 if(type_id==ID_integer ||
1288 type_id==ID_signedbv ||
1289 type_id==ID_unsignedbv)
1293 if(!int_value.has_value())
1298 else if(type_id==ID_rational)
1306 else if(type_id==ID_fixedbv)
1312 else if(type_id==ID_floatbv)
1328 const auto &type = expr.
type();
1331 type.id() == ID_bv || type.id() == ID_unsignedbv ||
1332 type.id() == ID_signedbv)
1336 if(op.
type() == type)
1341 const auto new_value =
1342 make_bvrep(width, [&value, &width](std::size_t i) {
1368 if((expr.
id()==ID_equal || expr.
id()==ID_notequal) &&
1372 auto new_expr = expr;
1373 new_expr.
op0().
swap(new_expr.op1());
1377 if(tmp0.
id()==ID_if && tmp0.
operands().size()==3)
1391 (expr.
id() == ID_equal || expr.
id() == ID_notequal))
1396 if(tmp0.
id()==ID_pointer_object &&
1397 tmp1.
id()==ID_pointer_object &&
1398 (expr.
id()==ID_equal || expr.
id()==ID_notequal))
1403 if(tmp0.
type().
id()==ID_c_enum_tag)
1406 if(tmp1.
type().
id()==ID_c_enum_tag)
1413 if(tmp0_const && tmp1_const)
1423 if(expr.
id()==ID_ge)
1425 else if(expr.
id()==ID_le)
1427 else if(expr.
id()==ID_gt)
1429 else if(expr.
id()==ID_lt)
1457 if(tmp0.
type().
id() == ID_c_enum_tag)
1460 if(tmp1.
type().
id() == ID_c_enum_tag)
1466 if(expr.
id() == ID_equal || expr.
id() == ID_notequal)
1470 bool equal = (tmp0_const.get_value() == tmp1_const.get_value());
1472 !equal && tmp0_const.type().id() == ID_pointer &&
1473 tmp1_const.type().id() == ID_pointer)
1476 !
config.ansi_c.NULL_is_zero && (tmp0_const.get_value() == ID_NULL ||
1477 tmp1_const.get_value() == ID_NULL))
1483 equal = tmp0_const.is_zero() && tmp1_const.is_zero();
1488 if(tmp0.
type().
id() == ID_fixedbv)
1493 if(expr.
id() == ID_ge)
1495 else if(expr.
id() == ID_le)
1497 else if(expr.
id() == ID_gt)
1499 else if(expr.
id() == ID_lt)
1504 else if(tmp0.
type().
id() == ID_floatbv)
1509 if(expr.
id() == ID_ge)
1511 else if(expr.
id() == ID_le)
1513 else if(expr.
id() == ID_gt)
1515 else if(expr.
id() == ID_lt)
1520 else if(tmp0.
type().
id() == ID_rational)
1530 if(expr.
id() == ID_ge)
1532 else if(expr.
id() == ID_le)
1534 else if(expr.
id() == ID_gt)
1536 else if(expr.
id() == ID_lt)
1553 if(expr.
id() == ID_ge)
1555 else if(expr.
id() == ID_le)
1557 else if(expr.
id() == ID_gt)
1559 else if(expr.
id() == ID_lt)
1577 if(op0.
id()==ID_plus)
1579 bool no_change =
true;
1587 else if(op1.
id()==ID_plus)
1589 bool no_change =
true;
1600 op0.
type().
id()!=ID_complex)
1618 if(expr.
op0().
type().
id() == ID_floatbv)
1621 if(expr.
op0().
type().
id() == ID_pointer)
1626 if(ptr_op0 == ptr_op1)
1632 std::move(offset_op0), expr.
id(), std::move(offset_op1)}));
1635 else if(expr.
id() != ID_equal && expr.
id() != ID_notequal)
1640 expr.
id() == ID_equal && ptr_op0.
id() == ID_address_of &&
1641 ptr_op1.
id() == ID_address_of)
1646 auto in_bounds = [
this](
const exprt &object_ptr,
const exprt &expr_op) {
1653 exprt in_object_bounds =
1655 std::move(offset), ID_lt, std::move(*
object_size)})
1665 in_bounds(ptr_op0, expr.
op0()).is_true() &&
1666 in_bounds(ptr_op1, expr.
op1()).is_true())
1674 if(expr.
id()==ID_notequal)
1676 auto new_rel_expr = expr;
1677 new_rel_expr.
id(ID_equal);
1681 else if(expr.
id()==ID_gt)
1683 auto new_rel_expr = expr;
1684 new_rel_expr.
id(ID_ge);
1686 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1690 else if(expr.
id()==ID_lt)
1692 auto new_rel_expr = expr;
1693 new_rel_expr.
id(ID_ge);
1697 else if(expr.
id()==ID_le)
1699 auto new_rel_expr = expr;
1700 new_rel_expr.
id(ID_ge);
1702 new_rel_expr.lhs().
swap(new_rel_expr.rhs());
1709 expr.
id() == ID_ge || expr.
id() == ID_equal,
1710 "we previously converted all other cases to >= or ==");
1714 if(expr.
op0() == expr.
op1())
1719 if(expr.
id()==ID_equal)
1755 if(expr.
id()==ID_notequal)
1757 auto new_rel_expr = expr;
1758 new_rel_expr.
id(ID_equal);
1764 if(expr.
id() != ID_equal)
1773 if(expr.
op0().
id() == ID_address_of)
1778 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1779 object.
id() == ID_member ||
object.
id() == ID_index ||
1780 object.
id() == ID_string_constant)
1786 expr.
op0().
id() == ID_typecast &&
1790 const auto &
object =
1794 object.
id() == ID_symbol ||
object.
id() == ID_dynamic_object ||
1795 object.
id() == ID_member ||
object.
id() == ID_index ||
1796 object.
id() == ID_string_constant)
1802 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_pointer)
1806 op.
type().
id() != ID_pointer &&
1808 op.
type().
id() == ID_complex))
1815 auto new_expr = expr;
1817 if(new_expr.op0().type().id() != ID_pointer)
1818 new_expr.op1() =
from_integer(0, new_expr.op0().type());
1820 new_expr.op1().type() = new_expr.op0().type();
1823 else if(expr.
op0().
id() == ID_plus)
1855 if(expr.
op0().
id()==ID_plus)
1859 if(expr.
id()==ID_equal || expr.
id()==ID_notequal)
1862 bool op_changed =
false;
1863 auto new_expr = expr;
1867 if(it->is_constant())
1885 new_expr.op1() =
from_integer(i, new_expr.op1().type());
1898 expr.
op0().
id() == ID_typecast && expr.
op0().
type().
id() == ID_floatbv &&
1906 ieee_floatt const_val_converted_back=const_val_converted;
1909 if(const_val_converted_back==const_val)
1914 return std::move(result);
1923 if(expr.
id()==ID_ge &&
1930 auto new_expr = expr;
1933 if(expr.
id()==ID_equal)
1936 if(operand.
id()==ID_unary_minus)
1939 return std::move(new_expr);
1941 else if(operand.
id()==ID_plus)
1946 if(operand_plus_expr.operands().size() == 2)
1949 if(operand_plus_expr.op0().id() == ID_unary_minus)
1950 operand_plus_expr.op0().swap(operand_plus_expr.op1());
1952 if(operand_plus_expr.op1().id() == ID_unary_minus)
1955 operand_plus_expr.op0(),
1964 if(
config.ansi_c.NULL_is_zero)
1967 if(maybe_tc_op.
type().
id() == ID_pointer)
1971 bool bitwidth_unchanged =
true;
1973 while(bitwidth_unchanged && ep->
id() == ID_typecast)
1977 bitwidth_unchanged = t->get_width() == p_type.
get_width();
1980 bitwidth_unchanged =
false;
1985 if(bitwidth_unchanged)
1987 if(expr.
id() == ID_equal || expr.
id() == ID_ge || expr.
id() == ID_le)
2004 expr.
op0().
id() == ID_typecast &&
2018 return lhs_typecast_op;
2022 #define NORMALISE_CONSTANT_TESTS
2023 #ifdef NORMALISE_CONSTANT_TESTS
2025 if(expr.
op0().
type().
id()==ID_unsignedbv ||
2030 if(expr.
id()==ID_notequal)
2032 auto new_rel_expr = expr;
2033 new_rel_expr.
id(ID_equal);
2037 else if(expr.
id()==ID_gt)
2046 auto new_expr = expr;
2049 new_expr.op1() =
from_integer(i, new_expr.op1().type());
2052 else if(expr.
id()==ID_lt)
2054 auto new_rel_expr = expr;
2055 new_rel_expr.
id(ID_ge);
2059 else if(expr.
id()==ID_le)
2068 auto new_rel_expr = expr;
2069 new_rel_expr.
id(ID_ge);
2071 new_rel_expr.op1() =
from_integer(i, new_rel_expr.op1().type());
2088 if(!const_bits_opt.has_value())
2091 std::reverse(const_bits_opt->begin(), const_bits_opt->end());
2098 if(!result.has_value())
2101 return std::move(*result);
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
API to expression classes for bitvectors.
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const integer_bitvector_typet & to_integer_bitvector_type(const typet &type)
Cast a typet to an integer_bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
unsignedbv_typet size_type()
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
A base class for binary expressions.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Bit-wise negation of bit-vectors.
Reverse the order of bits in a bit-vector.
Base class of fixed-width bit-vector types.
void set_width(std::size_t width)
std::size_t get_width() const
The byte swap expression.
std::size_t get_bits_per_byte() const
Concatenation of bit-vector operands.
A constant literal expression.
const irep_idt & get_value() const
void set_value(const irep_idt &value)
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Base class for all expressions.
std::vector< exprt > operandst
bool is_one() const
Return whether the expression is a constant representing 1.
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.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
The Boolean constant false.
constant_exprt to_expr() const
An IEEE 754 floating-point value, including specificiation.
constant_exprt to_expr() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
void change_spec(const ieee_float_spect &dest_spec)
The trinary if-then-else operator.
mp_integer largest() const
Return the largest value that can be represented using this type.
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
A base class for multi-ary expressions Associativity is not specified.
The null pointer constant.
The plus expression Associativity is not specified.
The offset (in bytes) of a pointer relative to the object.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const exprt & base() const
const exprt & exponent() const
A base class for shift and rotate operators.
resultt simplify_bitwise(const multi_ary_exprt &)
resultt simplify_inequality_address_of(const binary_relation_exprt &)
resultt simplify_div(const div_exprt &)
resultt simplify_bitreverse(const bitreverse_exprt &)
Try to simplify bit-reversing to a constant expression.
resultt simplify_bitnot(const bitnot_exprt &)
resultt simplify_zero_extend(const zero_extend_exprt &)
static resultt changed(resultt<> result)
resultt simplify_if(const if_exprt &)
resultt simplify_node(const exprt &)
resultt simplify_minus(const minus_exprt &)
resultt simplify_extractbit(const extractbit_exprt &)
resultt simplify_rec(const exprt &)
resultt simplify_shifts(const shift_exprt &)
resultt simplify_typecast(const typecast_exprt &)
resultt simplify_object(const exprt &)
resultt simplify_mult(const mult_exprt &)
resultt simplify_inequality_rhs_is_constant(const binary_relation_exprt &)
virtual resultt simplify_inequality(const binary_relation_exprt &)
simplifies inequalities !=, <=, <, >=, >, and also ==
resultt simplify_not(const not_exprt &)
resultt simplify_bswap(const bswap_exprt &)
virtual resultt simplify_inequality_pointer_object(const binary_relation_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_extractbits(const extractbits_exprt &)
Simplifies extracting of bits from a constant.
resultt simplify_mod(const mod_exprt &)
virtual resultt simplify_pointer_offset(const pointer_offset_exprt &)
resultt simplify_plus(const plus_exprt &)
resultt simplify_inequality_no_constant(const binary_relation_exprt &)
resultt simplify_unary_plus(const unary_plus_exprt &)
resultt simplify_power(const power_exprt &)
resultt simplify_concatenation(const concatenation_exprt &)
resultt simplify_inequality_both_constant(const binary_relation_exprt &)
simplifies inequalities for the case in which both sides of the inequality are constants
resultt simplify_unary_minus(const unary_minus_exprt &)
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
The unary plus expression.
Fixed-width bit-vector with unsigned binary interpretation.
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
#define Forall_operands(it, expr)
#define Forall_expr(it, expr)
auto type_try_dynamic_cast(TType &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TType >::type
Try to cast a reference to a generic typet to a specific derived class.
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Deprecated expression utility functions.
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
API to expression classes for Pointers.
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.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt object_size(const exprt &pointer)
static bool mul_expr(constant_exprt &dest, const constant_exprt &expr)
static bool sum_expr(constant_exprt &dest, const constant_exprt &expr)
static bool eliminate_common_addends(exprt &op0, exprt &op1)
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
std::optional< std::string > expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.