|
CBMC
|
#include <simplify_expr_class.h>
Inheritance diagram for simplify_exprt:
Collaboration diagram for simplify_exprt:Classes | |
| struct | resultt |
Static Public Member Functions | |
| static resultt | unchanged (exprt expr) |
| static resultt | changed (resultt<> result) |
Public Attributes | |
| bool | do_simplify_if |
Protected Attributes | |
| const namespacet & | ns |
Definition at line 84 of file simplify_expr_class.h.
|
inlineexplicit |
Definition at line 87 of file simplify_expr_class.h.
|
inlinevirtual |
Definition at line 100 of file simplify_expr_class.h.
Definition at line 146 of file simplify_expr_class.h.
Definition at line 3348 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_abs | ( | const abs_exprt & | expr | ) |
Definition at line 65 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_address_of | ( | const address_of_exprt & | expr | ) |
Definition at line 238 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_address_of_arg | ( | const exprt & | expr | ) |
Definition at line 81 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_bitnot | ( | const bitnot_exprt & | expr | ) |
Definition at line 1322 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_bitreverse | ( | const bitreverse_exprt & | expr | ) |
Try to simplify bit-reversing to a constant expression.
Definition at line 2078 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_bitwise | ( | const multi_ary_exprt & | expr | ) |
Definition at line 664 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_boolean | ( | const exprt & | expr | ) |
Definition at line 20 of file simplify_expr_boolean.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_bswap | ( | const bswap_exprt & | expr | ) |
Definition at line 33 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_byte_extract | ( | const byte_extract_exprt & | expr | ) |
Definition at line 1650 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_byte_extract_preorder | ( | const byte_extract_exprt & | expr | ) |
Definition at line 2037 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_byte_update | ( | const byte_update_exprt & | expr | ) |
Definition at line 2072 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_clz | ( | const count_leading_zeros_exprt & | expr | ) |
Try to simplify count-leading-zeros to a constant expression.
Definition at line 151 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_complex | ( | const unary_exprt & | expr | ) |
Definition at line 2519 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_concatenation | ( | const concatenation_exprt & | expr | ) |
Definition at line 871 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_ctz | ( | const count_trailing_zeros_exprt & | expr | ) |
Try to simplify count-trailing-zeros to a constant expression.
Definition at line 177 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_dereference | ( | const dereference_exprt & | expr | ) |
Definition at line 1395 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_dereference_preorder | ( | const dereference_exprt & | expr | ) |
Definition at line 1436 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_div | ( | const div_exprt & | expr | ) |
Definition at line 276 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_extractbit | ( | const extractbit_exprt & | expr | ) |
Definition at line 842 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_extractbits | ( | const extractbits_exprt & | expr | ) |
Simplifies extracting of bits from a constant.
Definition at line 1158 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_ffs | ( | const find_first_set_exprt & | expr | ) |
Try to simplify find-first-set to a constant expression.
Definition at line 203 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_floatbv_op | ( | const ieee_float_op_exprt & | expr | ) |
Definition at line 295 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_floatbv_round_to_integral | ( | const floatbv_round_to_integral_exprt & | expr | ) |
Definition at line 138 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast | ( | const floatbv_typecast_exprt & | expr | ) |
Definition at line 161 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_function_application | ( | const function_application_exprt & | expr | ) |
Attempt to simplify mathematical function applications if we have enough information to do so.
Currently focused on constant comparisons.
Definition at line 700 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_ieee_float_relation | ( | const binary_relation_exprt & | expr | ) |
Definition at line 361 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_if | ( | const if_exprt & | expr | ) |
Definition at line 335 of file simplify_expr_if.cpp.
Definition at line 144 of file simplify_expr_if.cpp.
Definition at line 176 of file simplify_expr_if.cpp.
Definition at line 106 of file simplify_expr_if.cpp.
Definition at line 125 of file simplify_expr_if.cpp.
| bool simplify_exprt::simplify_if_implies | ( | exprt & | expr, |
| const exprt & | cond, | ||
| bool | truth, | ||
| bool & | new_truth | ||
| ) |
Definition at line 15 of file simplify_expr_if.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_if_preorder | ( | const if_exprt & | expr | ) |
Definition at line 241 of file simplify_expr_if.cpp.
Definition at line 74 of file simplify_expr_if.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_index | ( | const index_exprt & | expr | ) |
Definition at line 20 of file simplify_expr_array.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_index_preorder | ( | const index_exprt & | expr | ) |
Definition at line 208 of file simplify_expr_array.cpp.
|
virtual |
simplifies inequalities !=, <=, <, >=, >, and also ==
Reimplemented in simplify_expr_with_value_sett.
Definition at line 1353 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_inequality_address_of | ( | const binary_relation_exprt & | expr | ) |
Definition at line 410 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_inequality_both_constant | ( | const binary_relation_exprt & | expr | ) |
simplifies inequalities for the case in which both sides of the inequality are constants
Definition at line 1449 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_inequality_no_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1609 of file simplify_expr_int.cpp.
|
virtual |
Reimplemented in simplify_expr_with_value_sett.
Definition at line 481 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant | ( | const binary_relation_exprt & | expr | ) |
Definition at line 1733 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object | ( | const unary_exprt & | expr | ) |
Definition at line 558 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer | ( | const unary_exprt & | expr | ) |
Definition at line 607 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_isinf | ( | const unary_exprt & | expr | ) |
Definition at line 23 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_isnan | ( | const unary_exprt & | expr | ) |
Definition at line 37 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_isnormal | ( | const unary_exprt & | expr | ) |
Definition at line 51 of file simplify_expr_floatbv.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_lambda | ( | const lambda_exprt & | expr | ) |
Definition at line 1460 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_member | ( | const member_exprt & | expr | ) |
Definition at line 23 of file simplify_expr_struct.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_member_preorder | ( | const member_exprt & | expr | ) |
Definition at line 279 of file simplify_expr_struct.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_minus | ( | const minus_exprt & | expr | ) |
Definition at line 572 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_mod | ( | const mod_exprt & | expr | ) |
Definition at line 369 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_mult | ( | const mult_exprt & | expr | ) |
Definition at line 165 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_node | ( | const exprt & | node | ) |
Definition at line 2986 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_node_preorder | ( | const exprt & | expr | ) |
Definition at line 2907 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_not | ( | const not_exprt & | expr | ) |
Definition at line 324 of file simplify_expr_boolean.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_object | ( | const exprt & | expr | ) |
Definition at line 1570 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_object_size | ( | const object_size_exprt & | expr | ) |
Definition at line 640 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_overflow_binary | ( | const binary_overflow_exprt & | expr | ) |
Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.
Simplification will be possible when the operands are constants or the types of the operands have infinite domains.
Definition at line 2540 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_overflow_result | ( | const overflow_result_exprt & | expr | ) |
Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl, overflow_result-unary–.
Simplification will be possible when the operands are constants or the types of the operands have infinite domains.
Definition at line 2660 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_overflow_unary | ( | const unary_overflow_exprt & | expr | ) |
Try to simplify overflow-unary-.
Simplification will be possible when the operand is constants or the type of the operand has an infinite domain.
Definition at line 2612 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_plus | ( | const plus_exprt & | expr | ) |
Definition at line 406 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_pointer_object | ( | const pointer_object_exprt & | expr | ) |
Definition at line 526 of file simplify_expr_pointer.cpp.
|
virtual |
Reimplemented in simplify_expr_with_value_sett.
Definition at line 276 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_popcount | ( | const popcount_exprt & | expr | ) |
Definition at line 125 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_power | ( | const power_exprt & | expr | ) |
Definition at line 1131 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_prophecy_pointer_in_range | ( | const prophecy_pointer_in_range_exprt & | expr | ) |
Try to simplify prophecy_pointer_in_range to a constant expression.
Definition at line 697 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_prophecy_r_or_w_ok | ( | const prophecy_r_or_w_ok_exprt & | expr | ) |
Try to simplify prophecy_{r,w,rw}_ok to a constant expression.
Definition at line 687 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_quantifier_expr | ( | const quantifier_exprt & | expr | ) |
Try to simplify exists/forall to a constant expression.
Definition at line 382 of file simplify_expr_boolean.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_rec | ( | const exprt & | expr | ) |
Definition at line 3274 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_shifts | ( | const shift_exprt & | expr | ) |
Definition at line 1023 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_sign | ( | const sign_exprt & | expr | ) |
Definition at line 99 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_typecast | ( | const typecast_exprt & | expr | ) |
Definition at line 757 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_typecast_preorder | ( | const typecast_exprt & | expr | ) |
Definition at line 1366 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_unary_minus | ( | const unary_minus_exprt & | expr | ) |
Definition at line 1262 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_unary_plus | ( | const unary_plus_exprt & | expr | ) |
Definition at line 1255 of file simplify_expr_int.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_unary_pointer_predicate_preorder | ( | const unary_exprt & | expr | ) |
Definition at line 55 of file simplify_expr_pointer.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_update | ( | const update_exprt & | expr | ) |
Definition at line 1522 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_with | ( | const with_exprt & | expr | ) |
Definition at line 1465 of file simplify_expr.cpp.
| simplify_exprt::resultt simplify_exprt::simplify_zero_extend | ( | const zero_extend_exprt & | expr | ) |
Definition at line 1011 of file simplify_expr_int.cpp.
Definition at line 141 of file simplify_expr_class.h.
| bool simplify_exprt::do_simplify_if |
Definition at line 104 of file simplify_expr_class.h.
|
protected |
Definition at line 291 of file simplify_expr_class.h.