Loading...

Searching...

No Matches

simplify_exprt Class Reference

#include <simplify_expr_class.h>

+ Inheritance diagram for simplify_exprt:

[フレーム]

[legend]

+ Collaboration diagram for simplify_exprt:

[フレーム]

[legend]

Classes

struct resultt

Public Member Functions

simplify_exprt (const namespacet &_ns)

virtual ~simplify_exprt ()

resultt simplify_typecast (const typecast_exprt &)

resultt simplify_typecast_preorder (const typecast_exprt &)

resultt simplify_extractbit (const extractbit_exprt &)

resultt simplify_extractbits (const extractbits_exprt &)

Simplifies extracting of bits from a constant.

resultt simplify_concatenation (const concatenation_exprt &)

resultt simplify_zero_extend (const zero_extend_exprt &)

resultt simplify_mult (const mult_exprt &)

resultt simplify_div (const div_exprt &)

resultt simplify_mod (const mod_exprt &)

resultt simplify_plus (const plus_exprt &)

resultt simplify_minus (const minus_exprt &)

resultt simplify_floatbv_op (const ieee_float_op_exprt &)

resultt simplify_floatbv_round_to_integral (const floatbv_round_to_integral_exprt &)

resultt simplify_floatbv_typecast (const floatbv_typecast_exprt &)

resultt simplify_shifts (const shift_exprt &)

resultt simplify_power (const power_exprt &)

resultt simplify_bitwise (const multi_ary_exprt &)

resultt simplify_if_preorder (const if_exprt &expr)

resultt simplify_if (const if_exprt &)

resultt simplify_bitnot (const bitnot_exprt &)

resultt simplify_not (const not_exprt &)

resultt simplify_boolean (const exprt &)

virtual resultt simplify_inequality (const binary_relation_exprt &)

simplifies inequalities !=, <=, <, >=, >, and also ==

resultt simplify_ieee_float_relation (const binary_relation_exprt &)

resultt simplify_lambda (const lambda_exprt &)

resultt simplify_with (const with_exprt &)

resultt simplify_update (const update_exprt &)

resultt simplify_index (const index_exprt &)

resultt simplify_index_preorder (const index_exprt &)

resultt simplify_member (const member_exprt &)

resultt simplify_member_preorder (const member_exprt &)

resultt simplify_byte_update (const byte_update_exprt &)

resultt simplify_byte_extract (const byte_extract_exprt &)

resultt simplify_byte_extract_preorder (const byte_extract_exprt &)

resultt simplify_pointer_object (const pointer_object_exprt &)

resultt simplify_unary_pointer_predicate_preorder (const unary_exprt &)

resultt simplify_object_size (const object_size_exprt &)

resultt simplify_is_dynamic_object (const unary_exprt &)

resultt simplify_is_invalid_pointer (const unary_exprt &)

resultt simplify_object (const exprt &)

resultt simplify_unary_minus (const unary_minus_exprt &)

resultt simplify_unary_plus (const unary_plus_exprt &)

resultt simplify_dereference (const dereference_exprt &)

resultt simplify_dereference_preorder (const dereference_exprt &)

resultt simplify_address_of (const address_of_exprt &)

virtual resultt simplify_pointer_offset (const pointer_offset_exprt &)

resultt simplify_bswap (const bswap_exprt &)

resultt simplify_isinf (const unary_exprt &)

resultt simplify_isnan (const unary_exprt &)

resultt simplify_isnormal (const unary_exprt &)

resultt simplify_abs (const abs_exprt &)

resultt simplify_sign (const sign_exprt &)

resultt simplify_popcount (const popcount_exprt &)

resultt simplify_complex (const unary_exprt &)

resultt simplify_overflow_binary (const binary_overflow_exprt &)

Try to simplify overflow-+, overflow-*, overflow–, overflow-shl.

resultt simplify_overflow_unary (const unary_overflow_exprt &)

Try to simplify overflow-unary-.

resultt simplify_overflow_result (const overflow_result_exprt &)

Try to simplify overflow_result-+, overflow_result-*, overflow_result–, overflow_result-shl, overflow_result-unary–.

resultt simplify_function_application (const function_application_exprt &)

Attempt to simplify mathematical function applications if we have enough information to do so.

resultt simplify_clz (const count_leading_zeros_exprt &)

Try to simplify count-leading-zeros to a constant expression.

resultt simplify_ctz (const count_trailing_zeros_exprt &)

Try to simplify count-trailing-zeros to a constant expression.

resultt simplify_bitreverse (const bitreverse_exprt &)

Try to simplify bit-reversing to a constant expression.

resultt simplify_ffs (const find_first_set_exprt &)

Try to simplify find-first-set to a constant expression.

resultt simplify_prophecy_r_or_w_ok (const prophecy_r_or_w_ok_exprt &)

Try to simplify prophecy_{r,w,rw}_ok to a constant expression.

resultt simplify_prophecy_pointer_in_range (const prophecy_pointer_in_range_exprt &)

Try to simplify prophecy_pointer_in_range to a constant expression.

resultt simplify_quantifier_expr (const quantifier_exprt &)

Try to simplify exists/forall to a constant expression.

bool simplify_if_implies (exprt &expr, const exprt &cond, bool truth, bool &new_truth)

bool simplify_if_recursive (exprt &expr, const exprt &cond, bool truth)

bool simplify_if_conj (exprt &expr, const exprt &cond)

bool simplify_if_disj (exprt &expr, const exprt &cond)

bool simplify_if_branch (exprt &trueexpr, exprt &falseexpr, const exprt &cond)

bool simplify_if_cond (exprt &expr)

resultt simplify_address_of_arg (const 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_inequality_no_constant (const binary_relation_exprt &)

resultt simplify_inequality_rhs_is_constant (const binary_relation_exprt &)

resultt simplify_inequality_address_of (const binary_relation_exprt &)

virtual resultt simplify_inequality_pointer_object (const binary_relation_exprt &)

resultt simplify_node (const exprt &)

resultt simplify_node_preorder (const exprt &)

resultt simplify_rec (const exprt &)

virtual bool simplify (exprt &expr)

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

Detailed Description

Definition at line 84 of file simplify_expr_class.h.

Constructor & Destructor Documentation

◆ simplify_exprt()

simplify_exprt::simplify_exprt ( const namespacet & _ns )

inlineexplicit

Definition at line 87 of file simplify_expr_class.h.

◆ ~simplify_exprt()

virtual simplify_exprt::~simplify_exprt ( )

inlinevirtual

Definition at line 100 of file simplify_expr_class.h.

Member Function Documentation

◆ changed()

static resultt simplify_exprt::changed ( resultt<> result )

inlinestatic

Definition at line 146 of file simplify_expr_class.h.

◆ simplify()

bool simplify_exprt::simplify ( exprt & expr )

virtual

Returns: returns true if expression unchanged; returns false if changed

Definition at line 3386 of file simplify_expr.cpp.

◆ simplify_abs()

simplify_exprt::resultt simplify_exprt::simplify_abs ( const abs_exprt & expr )

Definition at line 65 of file simplify_expr.cpp.

◆ simplify_address_of()

simplify_exprt::resultt simplify_exprt::simplify_address_of ( const address_of_exprt & expr )

Definition at line 238 of file simplify_expr_pointer.cpp.

◆ simplify_address_of_arg()

simplify_exprt::resultt simplify_exprt::simplify_address_of_arg ( const exprt & expr )

Definition at line 81 of file simplify_expr_pointer.cpp.

◆ simplify_bitnot()

simplify_exprt::resultt simplify_exprt::simplify_bitnot ( const bitnot_exprt & expr )

Definition at line 1348 of file simplify_expr_int.cpp.

◆ simplify_bitreverse()

simplify_exprt::resultt simplify_exprt::simplify_bitreverse ( const bitreverse_exprt & expr )

Try to simplify bit-reversing to a constant expression.

Definition at line 2104 of file simplify_expr_int.cpp.

◆ simplify_bitwise()

simplify_exprt::resultt simplify_exprt::simplify_bitwise ( const multi_ary_exprt & expr )

Definition at line 664 of file simplify_expr_int.cpp.

◆ simplify_boolean()

simplify_exprt::resultt simplify_exprt::simplify_boolean ( const exprt & expr )

Definition at line 20 of file simplify_expr_boolean.cpp.

◆ simplify_bswap()

simplify_exprt::resultt simplify_exprt::simplify_bswap ( const bswap_exprt & expr )

Definition at line 33 of file simplify_expr_int.cpp.

◆ simplify_byte_extract()

simplify_exprt::resultt simplify_exprt::simplify_byte_extract ( const byte_extract_exprt & expr )

Definition at line 1688 of file simplify_expr.cpp.

◆ simplify_byte_extract_preorder()

simplify_exprt::resultt simplify_exprt::simplify_byte_extract_preorder ( const byte_extract_exprt & expr )

Definition at line 2075 of file simplify_expr.cpp.

◆ simplify_byte_update()

simplify_exprt::resultt simplify_exprt::simplify_byte_update ( const byte_update_exprt & expr )

Definition at line 2110 of file simplify_expr.cpp.

◆ simplify_clz()

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_complex()

simplify_exprt::resultt simplify_exprt::simplify_complex ( const unary_exprt & expr )

Definition at line 2557 of file simplify_expr.cpp.

◆ simplify_concatenation()

simplify_exprt::resultt simplify_exprt::simplify_concatenation ( const concatenation_exprt & expr )

Definition at line 897 of file simplify_expr_int.cpp.

◆ simplify_ctz()

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_dereference()

simplify_exprt::resultt simplify_exprt::simplify_dereference ( const dereference_exprt & expr )

Definition at line 1433 of file simplify_expr.cpp.

◆ simplify_dereference_preorder()

simplify_exprt::resultt simplify_exprt::simplify_dereference_preorder ( const dereference_exprt & expr )

Definition at line 1474 of file simplify_expr.cpp.

◆ simplify_div()

simplify_exprt::resultt simplify_exprt::simplify_div ( const div_exprt & expr )

Definition at line 276 of file simplify_expr_int.cpp.

◆ simplify_extractbit()

simplify_exprt::resultt simplify_exprt::simplify_extractbit ( const extractbit_exprt & expr )

Definition at line 868 of file simplify_expr_int.cpp.

◆ simplify_extractbits()

simplify_exprt::resultt simplify_exprt::simplify_extractbits ( const extractbits_exprt & expr )

Simplifies extracting of bits from a constant.

Definition at line 1184 of file simplify_expr_int.cpp.

◆ simplify_ffs()

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_floatbv_op()

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_floatbv_round_to_integral()

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_floatbv_typecast()

simplify_exprt::resultt simplify_exprt::simplify_floatbv_typecast ( const floatbv_typecast_exprt & expr )

Definition at line 161 of file simplify_expr_floatbv.cpp.

◆ simplify_function_application()

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_ieee_float_relation()

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_if()

simplify_exprt::resultt simplify_exprt::simplify_if ( const if_exprt & expr )

Definition at line 335 of file simplify_expr_if.cpp.

◆ simplify_if_branch()

bool simplify_exprt::simplify_if_branch ( exprt & trueexpr,

exprt & falseexpr,

const exprt & cond

)

Definition at line 144 of file simplify_expr_if.cpp.

◆ simplify_if_cond()

bool simplify_exprt::simplify_if_cond ( exprt & expr )

Definition at line 176 of file simplify_expr_if.cpp.

◆ simplify_if_conj()

bool simplify_exprt::simplify_if_conj ( exprt & expr,

const exprt & cond

)

Definition at line 106 of file simplify_expr_if.cpp.

◆ simplify_if_disj()

bool simplify_exprt::simplify_if_disj ( exprt & expr,

const exprt & cond

)

Definition at line 125 of file simplify_expr_if.cpp.

◆ simplify_if_implies()

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_if_preorder()

simplify_exprt::resultt simplify_exprt::simplify_if_preorder ( const if_exprt & expr )

Definition at line 241 of file simplify_expr_if.cpp.

◆ simplify_if_recursive()

bool simplify_exprt::simplify_if_recursive ( exprt & expr,

const exprt & cond,

bool truth

)

Definition at line 74 of file simplify_expr_if.cpp.

◆ simplify_index()

simplify_exprt::resultt simplify_exprt::simplify_index ( const index_exprt & expr )

Definition at line 20 of file simplify_expr_array.cpp.

◆ simplify_index_preorder()

simplify_exprt::resultt simplify_exprt::simplify_index_preorder ( const index_exprt & expr )

Definition at line 208 of file simplify_expr_array.cpp.

◆ simplify_inequality()

simplify_exprt::resultt simplify_exprt::simplify_inequality ( const binary_relation_exprt & expr )

virtual

simplifies inequalities !=, <=, <, >=, >, and also ==

Reimplemented in simplify_expr_with_value_sett.

Definition at line 1379 of file simplify_expr_int.cpp.

◆ simplify_inequality_address_of()

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_inequality_both_constant()

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 1475 of file simplify_expr_int.cpp.

◆ simplify_inequality_no_constant()

simplify_exprt::resultt simplify_exprt::simplify_inequality_no_constant ( const binary_relation_exprt & expr )

Definition at line 1635 of file simplify_expr_int.cpp.

◆ simplify_inequality_pointer_object()

simplify_exprt::resultt simplify_exprt::simplify_inequality_pointer_object ( const binary_relation_exprt & expr )

virtual

Reimplemented in simplify_expr_with_value_sett.

Definition at line 481 of file simplify_expr_pointer.cpp.

◆ simplify_inequality_rhs_is_constant()

simplify_exprt::resultt simplify_exprt::simplify_inequality_rhs_is_constant ( const binary_relation_exprt & expr )

expr: an inequality where the RHS is a constant: and the LHS is not

Definition at line 1759 of file simplify_expr_int.cpp.

◆ simplify_is_dynamic_object()

simplify_exprt::resultt simplify_exprt::simplify_is_dynamic_object ( const unary_exprt & expr )

Definition at line 558 of file simplify_expr_pointer.cpp.

◆ simplify_is_invalid_pointer()

simplify_exprt::resultt simplify_exprt::simplify_is_invalid_pointer ( const unary_exprt & expr )

Definition at line 607 of file simplify_expr_pointer.cpp.

◆ simplify_isinf()

simplify_exprt::resultt simplify_exprt::simplify_isinf ( const unary_exprt & expr )

Definition at line 23 of file simplify_expr_floatbv.cpp.

◆ simplify_isnan()

simplify_exprt::resultt simplify_exprt::simplify_isnan ( const unary_exprt & expr )

Definition at line 37 of file simplify_expr_floatbv.cpp.

◆ simplify_isnormal()

simplify_exprt::resultt simplify_exprt::simplify_isnormal ( const unary_exprt & expr )

Definition at line 51 of file simplify_expr_floatbv.cpp.

◆ simplify_lambda()

simplify_exprt::resultt simplify_exprt::simplify_lambda ( const lambda_exprt & expr )

Definition at line 1498 of file simplify_expr.cpp.

◆ simplify_member()

simplify_exprt::resultt simplify_exprt::simplify_member ( const member_exprt & expr )

Definition at line 23 of file simplify_expr_struct.cpp.

◆ simplify_member_preorder()

simplify_exprt::resultt simplify_exprt::simplify_member_preorder ( const member_exprt & expr )

Definition at line 279 of file simplify_expr_struct.cpp.

◆ simplify_minus()

simplify_exprt::resultt simplify_exprt::simplify_minus ( const minus_exprt & expr )

Definition at line 572 of file simplify_expr_int.cpp.

◆ simplify_mod()

simplify_exprt::resultt simplify_exprt::simplify_mod ( const mod_exprt & expr )

Definition at line 369 of file simplify_expr_int.cpp.

◆ simplify_mult()

simplify_exprt::resultt simplify_exprt::simplify_mult ( const mult_exprt & expr )

Definition at line 165 of file simplify_expr_int.cpp.

◆ simplify_node()

simplify_exprt::resultt simplify_exprt::simplify_node ( const exprt & node )

Definition at line 3024 of file simplify_expr.cpp.

◆ simplify_node_preorder()

simplify_exprt::resultt simplify_exprt::simplify_node_preorder ( const exprt & expr )

Definition at line 2945 of file simplify_expr.cpp.

◆ simplify_not()

simplify_exprt::resultt simplify_exprt::simplify_not ( const not_exprt & expr )

Definition at line 324 of file simplify_expr_boolean.cpp.

◆ simplify_object()

simplify_exprt::resultt simplify_exprt::simplify_object ( const exprt & expr )

Definition at line 1608 of file simplify_expr.cpp.

◆ simplify_object_size()

simplify_exprt::resultt simplify_exprt::simplify_object_size ( const object_size_exprt & expr )

Definition at line 640 of file simplify_expr_pointer.cpp.

◆ simplify_overflow_binary()

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 2578 of file simplify_expr.cpp.

◆ simplify_overflow_result()

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 2698 of file simplify_expr.cpp.

◆ simplify_overflow_unary()

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 2650 of file simplify_expr.cpp.

◆ simplify_plus()

simplify_exprt::resultt simplify_exprt::simplify_plus ( const plus_exprt & expr )

Definition at line 406 of file simplify_expr_int.cpp.

◆ simplify_pointer_object()

simplify_exprt::resultt simplify_exprt::simplify_pointer_object ( const pointer_object_exprt & expr )

Definition at line 526 of file simplify_expr_pointer.cpp.

◆ simplify_pointer_offset()

simplify_exprt::resultt simplify_exprt::simplify_pointer_offset ( const pointer_offset_exprt & expr )

virtual

Reimplemented in simplify_expr_with_value_sett.

Definition at line 276 of file simplify_expr_pointer.cpp.

◆ simplify_popcount()

simplify_exprt::resultt simplify_exprt::simplify_popcount ( const popcount_exprt & expr )

Definition at line 125 of file simplify_expr.cpp.

◆ simplify_power()

simplify_exprt::resultt simplify_exprt::simplify_power ( const power_exprt & expr )

Definition at line 1157 of file simplify_expr_int.cpp.

◆ simplify_prophecy_pointer_in_range()

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_prophecy_r_or_w_ok()

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_quantifier_expr()

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_rec()

simplify_exprt::resultt simplify_exprt::simplify_rec ( const exprt & expr )

Definition at line 3312 of file simplify_expr.cpp.

◆ simplify_shifts()

simplify_exprt::resultt simplify_exprt::simplify_shifts ( const shift_exprt & expr )

Definition at line 1049 of file simplify_expr_int.cpp.

◆ simplify_sign()

simplify_exprt::resultt simplify_exprt::simplify_sign ( const sign_exprt & expr )

Definition at line 99 of file simplify_expr.cpp.

◆ simplify_typecast()

simplify_exprt::resultt simplify_exprt::simplify_typecast ( const typecast_exprt & expr )

Definition at line 757 of file simplify_expr.cpp.

◆ simplify_typecast_preorder()

simplify_exprt::resultt simplify_exprt::simplify_typecast_preorder ( const typecast_exprt & expr )

Definition at line 1404 of file simplify_expr.cpp.

◆ simplify_unary_minus()

simplify_exprt::resultt simplify_exprt::simplify_unary_minus ( const unary_minus_exprt & expr )

Definition at line 1288 of file simplify_expr_int.cpp.

◆ simplify_unary_plus()

simplify_exprt::resultt simplify_exprt::simplify_unary_plus ( const unary_plus_exprt & expr )

Definition at line 1281 of file simplify_expr_int.cpp.

◆ simplify_unary_pointer_predicate_preorder()

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_update()

simplify_exprt::resultt simplify_exprt::simplify_update ( const update_exprt & expr )

Definition at line 1560 of file simplify_expr.cpp.

◆ simplify_with()

simplify_exprt::resultt simplify_exprt::simplify_with ( const with_exprt & expr )

Definition at line 1503 of file simplify_expr.cpp.

◆ simplify_zero_extend()

simplify_exprt::resultt simplify_exprt::simplify_zero_extend ( const zero_extend_exprt & expr )

Definition at line 1037 of file simplify_expr_int.cpp.

◆ unchanged()

static resultt simplify_exprt::unchanged ( exprt expr )

inlinestatic

Definition at line 141 of file simplify_expr_class.h.

Member Data Documentation

◆ do_simplify_if

bool simplify_exprt::do_simplify_if

Definition at line 104 of file simplify_expr_class.h.

◆ ns

const namespacet& simplify_exprt::ns

protected

Definition at line 291 of file simplify_expr_class.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/util/simplify_expr_class.h
/home/runner/work/cbmc/cbmc/src/util/simplify_expr.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_array.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_boolean.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_floatbv.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_if.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_int.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_pointer.cpp
/home/runner/work/cbmc/cbmc/src/util/simplify_expr_struct.cpp