From fae5c0b5f1a1e9cdf326781f0818070d055cc0f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 Jul 2025 18:33:06 +0000 Subject: [PATCH 1/5] operator== for exprt and bool, int, nullptr_t Introduces comparison operators for more concise code, and deprecates `exprt::is_{true,false,zero,one}` in favour of these. --- src/util/expr.cpp | 87 ++----------------------- src/util/expr.h | 5 ++ src/util/std_expr.cpp | 143 ++++++++++++++++++++++++++++++++++++++++++ src/util/std_expr.h | 32 ++++++++++ 4 files changed, 184 insertions(+), 83 deletions(-) diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 6e1d5fb15ac..3442ca8a003 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -26,14 +26,14 @@ Author: Daniel Kroening, kroening@kroening.com /// \return True if is a Boolean constant representing `true`, false otherwise. bool exprt::is_true() const { - return is_constant() && is_boolean() && get(ID_value) != ID_false; + return *this == true; } /// Return whether the expression is a constant representing `false`. /// \return True if is a Boolean constant representing `false`, false otherwise. bool exprt::is_false() const { - return is_constant() && is_boolean() && get(ID_value) == ID_false; + return *this == false; } /// Return whether the expression is a constant representing 0. @@ -46,45 +46,7 @@ bool exprt::is_false() const /// \return True if has value 0, false otherwise. bool exprt::is_zero() const { - if(is_constant()) - { - const constant_exprt &constant=to_constant_expr(*this); - const irep_idt &type_id=type().id_string(); - - if(type_id==ID_integer || type_id==ID_natural) - { - return constant.value_is_zero_string(); - } - else if(type_id==ID_rational) - { - rationalt rat_value; - if(to_rational(*this, rat_value)) - CHECK_RETURN(false); - return rat_value.is_zero(); - } - else if( - type_id == ID_unsignedbv || type_id == ID_signedbv || - type_id == ID_c_bool || type_id == ID_c_bit_field) - { - return constant.value_is_zero_string(); - } - else if(type_id==ID_fixedbv) - { - if(fixedbvt(constant)==0) - return true; - } - else if(type_id==ID_floatbv) - { - if(ieee_float_valuet(constant) == 0) - return true; - } - else if(type_id==ID_pointer) - { - return constant.is_null_pointer(); - } - } - - return false; + return *this == 0; } /// Return whether the expression is a constant representing 1. @@ -95,48 +57,7 @@ bool exprt::is_zero() const /// \return True if has value 1, false otherwise. bool exprt::is_one() const { - if(is_constant()) - { - const auto &constant_expr = to_constant_expr(*this); - const irep_idt &type_id = type().id(); - - if(type_id==ID_integer || type_id==ID_natural) - { - mp_integer int_value = - string2integer(id2string(constant_expr.get_value())); - if(int_value==1) - return true; - } - else if(type_id==ID_rational) - { - rationalt rat_value; - if(to_rational(*this, rat_value)) - CHECK_RETURN(false); - return rat_value.is_one(); - } - else if( - type_id == ID_unsignedbv || type_id == ID_signedbv || - type_id == ID_c_bool || type_id == ID_c_bit_field) - { - const auto width = to_bitvector_type(type()).get_width(); - mp_integer int_value = - bvrep2integer(id2string(constant_expr.get_value()), width, false); - if(int_value==1) - return true; - } - else if(type_id==ID_fixedbv) - { - if(fixedbvt(constant_expr) == 1) - return true; - } - else if(type_id==ID_floatbv) - { - if(ieee_float_valuet(constant_expr) == 1) - return true; - } - } - - return false; + return *this == 1; } /// Get a \ref source_locationt from the expression or from its operands diff --git a/src/util/expr.h b/src/util/expr.h index 08e1d57a7e0..36c05f2bc2d 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_EXPR_H #include "as_const.h" +#include "deprecate.h" #include "type.h" #include "validate_expressions.h" #include "validate_types.h" @@ -214,9 +215,13 @@ class exprt:public irept return id() == ID_constant; } + DEPRECATED(SINCE(2025, 7, 5, "use expr == true instead")) bool is_true() const; + DEPRECATED(SINCE(2025, 7, 5, "use expr == false instead")) bool is_false() const; + DEPRECATED(SINCE(2025, 7, 5, "use expr == 0 instead")) bool is_zero() const; + DEPRECATED(SINCE(2025, 7, 5, "use expr == 1 instead")) bool is_one() const; /// Return whether the expression represents a Boolean. diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 826bc7fffbf..1b63013109d 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -8,10 +8,17 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_expr.h" +#include "arith_tools.h" #include "config.h" +#include "expr_util.h" +#include "fixedbv.h" +#include "ieee_float.h" +#include "mathematical_types.h" #include "namespace.h" #include "pointer_expr.h" #include "range.h" +#include "rational.h" +#include "rational_tools.h" #include "substitute_symbols.h" #include @@ -22,6 +29,130 @@ bool constant_exprt::value_is_zero_string() const return val.find_first_not_of('0')==std::string::npos; } +bool operator==(const exprt &lhs, bool rhs) +{ + return lhs.is_constant() && to_constant_expr(lhs) == rhs; +} + +bool operator!=(const exprt &lhs, bool rhs) +{ + return !lhs.is_constant() || to_constant_expr(lhs) != rhs; +} + +bool operator==(const constant_exprt &lhs, bool rhs) +{ + return lhs.is_boolean() && (lhs.get_value() != ID_false) == rhs; +} + +bool operator!=(const constant_exprt &lhs, bool rhs) +{ + return !lhs.is_boolean() || (lhs.get_value() != ID_false) != rhs; +} + +bool operator==(const exprt &lhs, int rhs) +{ + if(lhs.is_constant()) + return to_constant_expr(lhs) == rhs; + else + return false; +} + +bool operator==(const constant_exprt &lhs, int rhs) +{ + if(rhs == 0) + { + const irep_idt &type_id = lhs.type().id(); + + if(type_id == ID_integer) + { + return integer_typet{}.zero_expr() == lhs; + } + else if(type_id == ID_natural) + { + return natural_typet{}.zero_expr() == lhs; + } + else if(type_id == ID_real) + { + return real_typet{}.zero_expr() == lhs; + } + else if(type_id == ID_rational) + { + rationalt rat_value; + if(to_rational(lhs, rat_value)) + CHECK_RETURN(false); + return rat_value.is_zero(); + } + else if( + type_id == ID_unsignedbv || type_id == ID_signedbv || + type_id == ID_c_bool || type_id == ID_c_bit_field) + { + return lhs.value_is_zero_string(); + } + else if(type_id == ID_fixedbv) + { + return fixedbvt(lhs).is_zero(); + } + else if(type_id == ID_floatbv) + { + return ieee_float_valuet(lhs).is_zero(); + } + else if(type_id == ID_pointer) + { + return lhs == nullptr; + } + else + return false; + } + else if(rhs == 1) + { + const irep_idt &type_id = lhs.type().id(); + + if(type_id == ID_integer) + { + return integer_typet{}.one_expr() == lhs; + } + else if(type_id == ID_natural) + { + return natural_typet{}.one_expr() == lhs; + } + else if(type_id == ID_real) + { + return real_typet{}.one_expr() == lhs; + } + else if(type_id == ID_rational) + { + rationalt rat_value; + if(to_rational(lhs, rat_value)) + CHECK_RETURN(false); + return rat_value.is_one(); + } + else if( + type_id == ID_unsignedbv || type_id == ID_signedbv || + type_id == ID_c_bool || type_id == ID_c_bit_field) + { + const auto width = to_bitvector_type(lhs.type()).get_width(); + mp_integer int_value = + bvrep2integer(id2string(lhs.get_value()), width, false); + return int_value == 1; + } + else if(type_id == ID_fixedbv) + { + fixedbv_spect spec{to_fixedbv_type(lhs.type())}; + fixedbvt one{spec}; + one.from_integer(1); + return one == fixedbvt{lhs}; + } + else if(type_id == ID_floatbv) + { + return ieee_float_valuet(lhs) == 1; + } + else + return false; + } + else + PRECONDITION(false); +} + bool constant_exprt::is_null_pointer() const { if(type().id() != ID_pointer) @@ -38,6 +169,18 @@ bool constant_exprt::is_null_pointer() const return false; } +bool operator==(const exprt &lhs, std::nullptr_t rhs) +{ + (void)rhs; // unused parameter + return lhs.is_constant() && to_constant_expr(lhs).is_null_pointer(); +} + +bool operator==(const constant_exprt &lhs, std::nullptr_t rhs) +{ + (void)rhs; // unused parameter + return lhs.is_null_pointer(); +} + void constant_exprt::check(const exprt &expr, const validation_modet vm) { nullary_exprt::check(expr, vm); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 90cac8a1d8d..2ce43a6f63d 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3189,6 +3189,38 @@ inline constant_exprt &to_constant_expr(exprt &expr) return static_cast(expr); } +/// Return whether the expression \p lhs is a constant of Boolean type that is +/// representing the Boolean value \p rhs. +bool operator==(const exprt &lhs, bool rhs); +/// \copydoc operator==(const exprt &, bool) +bool operator==(const constant_exprt &lhs, bool rhs); + +/// Return whether the expression \p lhs is not a constant of Boolean type or is +/// not representing the Boolean value \p rhs. +bool operator!=(const exprt &lhs, bool rhs); +/// \copydoc operator!=(const exprt &, bool) +bool operator!=(const constant_exprt &lhs, bool rhs); + +/// Return whether the expression \p lhs is a constant representing the numeric +/// value \p rhs; only values 0 and 1 are supported for \p rhs. +/// For value 0 we consider the following types: ID_integer, ID_natural, +/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, +/// ID_fixedbv, ID_floatbv, ID_pointer.
+/// For ID_pointer, returns true iff the value is a zero string or a null +/// pointer.
+/// For value 1 we consider the following types: ID_integer, ID_natural, +/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, +/// ID_fixedbv, ID_floatbv.
+/// For all other types, return false. +bool operator==(const exprt &lhs, int rhs); +/// \copydoc operator==(const exprt &, int) +bool operator==(const constant_exprt &lhs, int rhs); + +/// Return whether the expression \p lhs is a constant representing the NULL +/// pointer. +bool operator==(const exprt &lhs, std::nullptr_t); +/// \copydoc operator==(const exprt &, std::nullptr_t) +bool operator==(const constant_exprt &lhs, std::nullptr_t); /// \brief The Boolean constant true class true_exprt:public constant_exprt From fba2cce7dff9620cfe5cb64f409edf68785a5df8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 Jul 2025 09:47:43 +0000 Subject: [PATCH 2/5] Make constant_exprt variant of operator== member functions This provides access to methods that may eventually become private. --- src/util/std_expr.cpp | 52 +++++++++++++++++++++---------------------- src/util/std_expr.h | 19 +++++++++------- 2 files changed, 37 insertions(+), 34 deletions(-) diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 1b63013109d..a7cc221fd3e 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -39,14 +39,14 @@ bool operator!=(const exprt &lhs, bool rhs) return !lhs.is_constant() || to_constant_expr(lhs) != rhs; } -bool operator==(const constant_exprt &lhs, bool rhs) +bool constant_exprt::operator==(bool rhs) const { - return lhs.is_boolean() && (lhs.get_value() != ID_false) == rhs; + return is_boolean() && (get_value() != ID_false) == rhs; } -bool operator!=(const constant_exprt &lhs, bool rhs) +bool constant_exprt::operator!=(bool rhs) const { - return !lhs.is_boolean() || (lhs.get_value() != ID_false) != rhs; + return !is_boolean() || (get_value() != ID_false) != rhs; } bool operator==(const exprt &lhs, int rhs) @@ -57,28 +57,28 @@ bool operator==(const exprt &lhs, int rhs) return false; } -bool operator==(const constant_exprt &lhs, int rhs) +bool constant_exprt::operator==(int rhs) const { if(rhs == 0) { - const irep_idt &type_id = lhs.type().id(); + const irep_idt &type_id = type().id(); if(type_id == ID_integer) { - return integer_typet{}.zero_expr() == lhs; + return integer_typet{}.zero_expr() == *this; } else if(type_id == ID_natural) { - return natural_typet{}.zero_expr() == lhs; + return natural_typet{}.zero_expr() == *this; } else if(type_id == ID_real) { - return real_typet{}.zero_expr() == lhs; + return real_typet{}.zero_expr() == *this; } else if(type_id == ID_rational) { rationalt rat_value; - if(to_rational(lhs, rat_value)) + if(to_rational(*this, rat_value)) CHECK_RETURN(false); return rat_value.is_zero(); } @@ -86,43 +86,43 @@ bool operator==(const constant_exprt &lhs, int rhs) type_id == ID_unsignedbv || type_id == ID_signedbv || type_id == ID_c_bool || type_id == ID_c_bit_field) { - return lhs.value_is_zero_string(); + return value_is_zero_string(); } else if(type_id == ID_fixedbv) { - return fixedbvt(lhs).is_zero(); + return fixedbvt(*this).is_zero(); } else if(type_id == ID_floatbv) { - return ieee_float_valuet(lhs).is_zero(); + return ieee_float_valuet(*this).is_zero(); } else if(type_id == ID_pointer) { - return lhs == nullptr; + return *this == nullptr; } else return false; } else if(rhs == 1) { - const irep_idt &type_id = lhs.type().id(); + const irep_idt &type_id = type().id(); if(type_id == ID_integer) { - return integer_typet{}.one_expr() == lhs; + return integer_typet{}.one_expr() == *this; } else if(type_id == ID_natural) { - return natural_typet{}.one_expr() == lhs; + return natural_typet{}.one_expr() == *this; } else if(type_id == ID_real) { - return real_typet{}.one_expr() == lhs; + return real_typet{}.one_expr() == *this; } else if(type_id == ID_rational) { rationalt rat_value; - if(to_rational(lhs, rat_value)) + if(to_rational(*this, rat_value)) CHECK_RETURN(false); return rat_value.is_one(); } @@ -130,21 +130,21 @@ bool operator==(const constant_exprt &lhs, int rhs) type_id == ID_unsignedbv || type_id == ID_signedbv || type_id == ID_c_bool || type_id == ID_c_bit_field) { - const auto width = to_bitvector_type(lhs.type()).get_width(); + const auto width = to_bitvector_type(type()).get_width(); mp_integer int_value = - bvrep2integer(id2string(lhs.get_value()), width, false); + bvrep2integer(id2string(get_value()), width, false); return int_value == 1; } else if(type_id == ID_fixedbv) { - fixedbv_spect spec{to_fixedbv_type(lhs.type())}; + fixedbv_spect spec{to_fixedbv_type(type())}; fixedbvt one{spec}; one.from_integer(1); - return one == fixedbvt{lhs}; + return one == fixedbvt{*this}; } else if(type_id == ID_floatbv) { - return ieee_float_valuet(lhs) == 1; + return ieee_float_valuet(*this) == 1; } else return false; @@ -175,10 +175,10 @@ bool operator==(const exprt &lhs, std::nullptr_t rhs) return lhs.is_constant() && to_constant_expr(lhs).is_null_pointer(); } -bool operator==(const constant_exprt &lhs, std::nullptr_t rhs) +bool constant_exprt::operator==(std::nullptr_t rhs) const { (void)rhs; // unused parameter - return lhs.is_null_pointer(); + return is_null_pointer(); } void constant_exprt::check(const exprt &expr, const validation_modet vm) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 2ce43a6f63d..31a08d1be71 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -3144,6 +3144,17 @@ class constant_exprt : public nullary_exprt /// false in all other cases. bool is_null_pointer() const; + using irept::operator==; + using irept::operator!=; + /// \copydoc operator==(const exprt &, bool) + bool operator==(bool rhs) const; + /// \copydoc operator!=(const exprt &, bool) + bool operator!=(bool rhs) const; + /// \copydoc operator==(const exprt &, int) + bool operator==(int rhs) const; + /// \copydoc operator==(const exprt &, std::nullptr_t) + bool operator==(std::nullptr_t) const; + static void check( const exprt &expr, const validation_modet vm = validation_modet::INVARIANT); @@ -3192,14 +3203,10 @@ inline constant_exprt &to_constant_expr(exprt &expr) /// Return whether the expression \p lhs is a constant of Boolean type that is /// representing the Boolean value \p rhs. bool operator==(const exprt &lhs, bool rhs); -/// \copydoc operator==(const exprt &, bool) -bool operator==(const constant_exprt &lhs, bool rhs); /// Return whether the expression \p lhs is not a constant of Boolean type or is /// not representing the Boolean value \p rhs. bool operator!=(const exprt &lhs, bool rhs); -/// \copydoc operator!=(const exprt &, bool) -bool operator!=(const constant_exprt &lhs, bool rhs); /// Return whether the expression \p lhs is a constant representing the numeric /// value \p rhs; only values 0 and 1 are supported for \p rhs. @@ -3213,14 +3220,10 @@ bool operator!=(const constant_exprt &lhs, bool rhs); /// ID_fixedbv, ID_floatbv.
/// For all other types, return false. bool operator==(const exprt &lhs, int rhs); -/// \copydoc operator==(const exprt &, int) -bool operator==(const constant_exprt &lhs, int rhs); /// Return whether the expression \p lhs is a constant representing the NULL /// pointer. bool operator==(const exprt &lhs, std::nullptr_t); -/// \copydoc operator==(const exprt &, std::nullptr_t) -bool operator==(const constant_exprt &lhs, std::nullptr_t); /// \brief The Boolean constant true class true_exprt:public constant_exprt From 706c1ee912b471ca7e888307e502c260e8234c85 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 5 Jul 2025 18:34:52 +0000 Subject: [PATCH 3/5] Use operator==(exprt, bool) Replaces uses of `is_true` and `is_false`. --- jbmc/src/java_bytecode/expr2java.cpp | 4 +- .../src/java_bytecode/java_object_factory.cpp | 2 +- ...ove_virtual_functions_without_fallback.cpp | 6 +-- src/analyses/constant_propagator.cpp | 6 +-- src/analyses/custom_bitvector_analysis.cpp | 10 ++--- src/analyses/goto_rw.cpp | 8 ++-- src/analyses/guard_bdd.cpp | 2 +- src/analyses/guard_expr.cpp | 8 ++-- src/analyses/guard_expr.h | 6 +-- src/analyses/interval_analysis.cpp | 4 +- src/analyses/interval_domain.cpp | 4 +- src/analyses/invariant_set.cpp | 10 ++--- src/analyses/local_cfg.cpp | 2 +- .../abstract_environment.cpp | 8 ++-- .../abstract_value_object.cpp | 4 +- .../full_array_abstract_object.cpp | 2 +- .../full_struct_abstract_object.cpp | 2 +- .../interval_abstract_value.cpp | 6 +-- .../value_set_abstract_object.cpp | 4 +- src/ansi-c/c_typecheck_code.cpp | 4 +- src/ansi-c/c_typecheck_expr.cpp | 6 +-- src/ansi-c/c_typecheck_type.cpp | 8 ++-- src/ansi-c/expr2c.cpp | 4 +- src/ansi-c/goto-conversion/goto_check_c.cpp | 4 +- .../goto-conversion/goto_clean_expr.cpp | 2 +- src/ansi-c/goto-conversion/goto_convert.cpp | 12 ++--- .../goto_convert_functions.cpp | 2 +- src/cpp/cpp_instantiate_template.cpp | 4 +- src/cpp/cpp_typecheck_static_assert.cpp | 2 +- src/cpp/expr2cpp.cpp | 4 +- src/cprover/inductiveness.cpp | 4 +- src/cprover/instrument_contracts.cpp | 6 +-- src/cprover/may_alias.cpp | 2 +- src/cprover/simplify_state_expr.cpp | 8 ++-- src/cprover/state_encoding.cpp | 6 +-- src/goto-analyzer/static_verifier.cpp | 4 +- src/goto-analyzer/taint_analysis.cpp | 2 +- src/goto-checker/bmc_util.cpp | 9 ++-- .../counterexample_beautification.cpp | 6 +-- .../goto_symex_fault_localizer.cpp | 4 +- .../goto_symex_property_decider.cpp | 8 +--- src/goto-checker/symex_bmc.cpp | 6 +-- src/goto-instrument/accelerate/accelerate.cpp | 2 +- .../accelerate/acceleration_utils.cpp | 2 +- .../accelerate/cone_of_influence.cpp | 6 +-- .../disjunctive_polynomial_acceleration.cpp | 4 +- .../accelerate/polynomial_accelerator.cpp | 2 +- .../accelerate/sat_path_enumerator.cpp | 4 +- src/goto-instrument/call_sequences.cpp | 2 +- src/goto-instrument/contracts/contracts.cpp | 6 +-- .../dfcc_check_loop_normal_form.cpp | 2 +- .../contracts/instrument_spec_assigns.cpp | 8 ++-- src/goto-instrument/contracts/utils.cpp | 4 +- src/goto-instrument/cover_basic_blocks.cpp | 4 +- .../cover_instrument_branch.cpp | 3 +- src/goto-instrument/dot.cpp | 6 +-- src/goto-instrument/full_slicer.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 44 +++++++++---------- src/goto-instrument/horn_encoding.cpp | 6 +-- src/goto-instrument/unwind.cpp | 4 +- src/goto-programs/cfg.h | 4 +- .../ensure_one_backedge_per_target.cpp | 2 +- src/goto-programs/goto_program.cpp | 6 +-- src/goto-programs/goto_program.h | 4 +- src/goto-programs/goto_trace.cpp | 2 +- src/goto-programs/graphml_witness.cpp | 4 +- src/goto-programs/interpreter_evaluate.cpp | 2 +- src/goto-programs/json_expr.cpp | 4 +- src/goto-programs/remove_skip.cpp | 4 +- src/goto-programs/vcd_goto_trace.cpp | 4 +- src/goto-programs/xml_expr.cpp | 4 +- src/goto-symex/build_goto_trace.cpp | 10 ++--- src/goto-symex/goto_symex_state.cpp | 8 ++-- src/goto-symex/memory_model_sc.cpp | 4 +- src/goto-symex/memory_model_tso.cpp | 2 +- src/goto-symex/partial_order_concurrency.cpp | 4 +- src/goto-symex/postcondition.cpp | 4 +- src/goto-symex/precondition.cpp | 2 +- src/goto-symex/shadow_memory_util.cpp | 16 +++---- src/goto-symex/show_program.cpp | 4 +- .../simplify_expr_with_value_set.cpp | 4 +- src/goto-symex/solver_hardness.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 2 +- src/goto-symex/symex_goto.cpp | 14 +++--- src/goto-symex/symex_main.cpp | 10 ++--- src/linking/linking.cpp | 2 +- src/solvers/flattening/boolbv_quantifier.cpp | 2 +- src/solvers/prop/bdd_expr.cpp | 2 +- src/solvers/prop/cover_goals.cpp | 4 +- src/solvers/prop/prop_conv_solver.cpp | 8 ++-- src/solvers/smt2/smt2_conv.cpp | 12 ++--- src/solvers/smt2/smt2_format.cpp | 4 +- .../smt2_incremental/convert_expr_to_smt.cpp | 2 +- .../strings/string_builtin_function.cpp | 2 +- src/solvers/strings/string_refinement.cpp | 8 ++-- src/util/expr_util.cpp | 4 +- src/util/format_expr.cpp | 4 +- src/util/interval.cpp | 10 ++--- src/util/simplify_expr.cpp | 12 ++--- src/util/simplify_expr_array.cpp | 4 +- src/util/simplify_expr_boolean.cpp | 14 +++--- src/util/simplify_expr_if.cpp | 15 +++---- src/util/simplify_expr_int.cpp | 6 +-- src/util/simplify_expr_pointer.cpp | 4 +- src/util/std_expr.cpp | 4 +- .../value_expression_evaluation/assume.cpp | 4 +- .../assume_prune.cpp | 2 +- unit/goto-symex/shadow_memory_util.cpp | 2 +- unit/util/interval/get_extreme.cpp | 6 +-- unit/util/simplify_expr.cpp | 2 +- 110 files changed, 291 insertions(+), 300 deletions(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 67d3f33fdd0..41e40925f4e 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -179,9 +179,9 @@ std::string expr2javat::convert_constant( } else if(src.is_boolean()) { - if(src.is_true()) + if(src == true) return "true"; - else if(src.is_false()) + else if(src == false) return "false"; } else if(src.type().id()==ID_pointer) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 9675e9a9c31..3ea4bab11eb 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -1087,7 +1087,7 @@ void java_object_factoryt::gen_nondet_init( else { exprt within_bounds = interval.make_contains_expr(expr); - if(!within_bounds.is_true()) + if(within_bounds != true) assignments.add(code_assumet(std::move(within_bounds))); } diff --git a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp index ae9f2272db1..af01baa8159 100644 --- a/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp @@ -69,7 +69,7 @@ static bool is_call_to( static bool is_assume_false(goto_programt::const_targett inst) { - return inst->is_assume() && inst->condition().is_false(); + return inst->is_assume() && inst->condition() == false; } /// Interpret `program`, resolving classid comparisons assuming any actual @@ -90,12 +90,12 @@ static goto_programt::const_targett interpret_classid_comparison( { exprt guard = pc->condition(); guard = resolve_classid_test(guard, actual_class_id, ns); - if(guard.is_true()) + if(guard == true) { REQUIRE(pc->targets.begin() != pc->targets.end()); pc = *(pc->targets.begin()); } - else if(guard.is_false()) + else if(guard == false) ++pc; else { diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 80b9c778a45..c57466bea2c 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -183,8 +183,8 @@ void constant_propagator_domaint::transform( else g = not_exprt(from->condition()); partial_evaluate(values, g, ns); - if(g.is_false()) - values.set_to_bottom(); + if(g == false) + values.set_to_bottom(); else two_way_propagate_rec(g, ns, cp); } @@ -376,7 +376,7 @@ bool constant_propagator_domaint::two_way_propagate_rec( // x != FALSE ==> x == TRUE - if(rhs.is_zero() || rhs.is_false()) + if(rhs == 0 || rhs == false) rhs = from_integer(1, rhs.type()); else rhs = from_integer(0, rhs.type()); diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index a6d252f99e6..c56d92f431f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -530,7 +530,7 @@ void custom_bitvector_domaint::transform( const exprt result2 = simplify_expr(eval(guard, cba), ns); - if(result2.is_false()) + if(result2 == false) make_bottom(); } break; @@ -814,9 +814,9 @@ void custom_bitvector_analysist::check( if(use_xml) { out << "expr = expr; @@ -198,7 +198,7 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2) if(tmp != and_expr1) { - if(and_expr1.is_true() || and_expr2.is_true()) + if(and_expr1 == true || and_expr2 == true) { } else diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h index ea5d227eee7..fbcbc00f1f7 100644 --- a/src/analyses/guard_expr.h +++ b/src/analyses/guard_expr.h @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_GUARD_EXPR_H #define CPROVER_ANALYSES_GUARD_EXPR_H -#include +#include /// This is unused by this implementation of guards, but can be used by other /// implementations of the same interface. @@ -59,12 +59,12 @@ class guard_exprt bool is_true() const { - return expr.is_true(); + return expr == true; } bool is_false() const { - return expr.is_false(); + return expr == false; } friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2); diff --git a/src/analyses/interval_analysis.cpp b/src/analyses/interval_analysis.cpp index f9cc3cf1906..a41e2aa9920 100644 --- a/src/analyses/interval_analysis.cpp +++ b/src/analyses/interval_analysis.cpp @@ -46,7 +46,7 @@ void instrument_intervals( { goto_programt::const_targett previous = std::prev(i_it); - if(previous->is_goto() && !previous->condition().is_true()) + if(previous->is_goto() && previous->condition() != true) { // we follow a branch, instrument } @@ -69,7 +69,7 @@ void instrument_intervals( for(const auto &symbol_expr : symbols) { exprt tmp=d.make_expression(symbol_expr); - if(!tmp.is_true()) + if(tmp != true) assertion.push_back(tmp); } diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index ed1fb8acd1f..d6bd97d28ba 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -501,7 +501,7 @@ bool interval_domaint::ai_simplify( // of when condition is true if(!a.join(d)) // If d (this) is included in a... { // Then the condition is always true - unchanged=condition.is_true(); + unchanged = condition == true; condition = true_exprt(); } } @@ -514,7 +514,7 @@ bool interval_domaint::ai_simplify( d.assume(not_exprt(condition), ns); // Restrict to when condition is false if(d.is_bottom()) // If there there are none... { // Then the condition is always true - unchanged=condition.is_true(); + unchanged = condition == true; condition = true_exprt(); } } diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp index f05476766e7..f369177b886 100644 --- a/src/analyses/invariant_set.cpp +++ b/src/analyses/invariant_set.cpp @@ -394,11 +394,11 @@ void invariant_sett::strengthen_rec(const exprt &expr) return; } - if(expr.is_true()) + if(expr == true) { // do nothing, it's useless } - else if(expr.is_false()) + else if(expr == false) { // wow, that's strong make_false(); @@ -596,7 +596,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const if(is_false) // can't get any stronger return tvt(true); - if(expr.is_true()) + if(expr == true) return tvt(true); else if(expr.id()==ID_not) { @@ -701,12 +701,12 @@ void invariant_sett::nnf(exprt &expr, bool negate) if(!expr.is_boolean()) throw "nnf: non-Boolean expression"; - if(expr.is_true()) + if(expr == true) { if(negate) expr=false_exprt(); } - else if(expr.is_false()) + else if(expr == false) { if(negate) expr=true_exprt(); diff --git a/src/analyses/local_cfg.cpp b/src/analyses/local_cfg.cpp index 60bcabb783f..fdf1c764a24 100644 --- a/src/analyses/local_cfg.cpp +++ b/src/analyses/local_cfg.cpp @@ -35,7 +35,7 @@ void local_cfgt::build(const goto_programt &goto_program) switch(instruction.type()) { case GOTO: - if(!instruction.condition().is_true()) + if(instruction.condition() != true) node.successors.push_back(loc_nr+1); for(const auto &target : instruction.targets) diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index c692c526b58..ab06589e902 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -275,7 +275,7 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns) // Should be of the right type INVARIANT(assumption.is_boolean(), "simplification preserves type"); - if(assumption.is_false()) + if(assumption == false) { bool currently_bottom = is_bottom(); make_bottom(); @@ -582,7 +582,7 @@ static exprt invert_result(const exprt &result) if(!result.is_boolean()) return result; - if(result.is_true()) + if(result == true) return false_exprt(); return true_exprt(); } @@ -640,7 +640,7 @@ exprt assume_and( for(auto const &operand : and_expr.operands()) { auto result = env.do_assume(operand, ns); - if(result.is_false()) + if(result == false) return result; nil |= result.is_nil(); } @@ -833,7 +833,7 @@ exprt assume_less_than( auto reduced_le_expr = binary_relation_exprt(left_lower, expr.id(), right_upper); auto result = env.eval(reduced_le_expr, ns)->to_constant(); - if(result.is_true()) + if(result == true) { if(is_assignable(operands.lhs)) { diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index 2b339a3f5f3..480c46073a8 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -664,8 +664,8 @@ class value_set_evaluator for(const auto &v : condition) { auto expr = v->to_constant(); - all_true = all_true && expr.is_true(); - all_false = all_false && expr.is_false(); + all_true = all_true && expr == true; + all_false = all_false && expr == false; } auto indeterminate = !all_true && !all_false; diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 1d766adf82a..cfce4a122e8 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -426,7 +426,7 @@ exprt full_array_abstract_objectt::to_predicate_internal( auto index = index_exprt(name, ii); auto field_expr = field.second->to_predicate(index); - if(!field_expr.is_true()) + if(field_expr != true) all_predicates.push_back(field_expr); } diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index ab1ae403d46..02390b8f78e 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -312,7 +312,7 @@ exprt full_struct_abstract_objectt::to_predicate_internal( member_exprt(name, compound_type.get_component(field.first)); auto field_expr = field.second->to_predicate(field_name); - if(!field_expr.is_true()) + if(field_expr != true) all_predicates.push_back(field_expr); } diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 51f738c5109..94e4218442b 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -45,8 +45,8 @@ class interval_index_ranget : public index_range_implementationt { index = next; next = next_element(next, ns); - return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns) - .is_true(); + return simplify_expr(binary_predicate_exprt(index, ID_le, upper), ns) == + true; } index_range_implementation_ptrt reset() const override @@ -239,7 +239,7 @@ bool new_interval_is_top(const constant_interval_exprt &e) if(e.is_top()) return true; - if(e.get_lower().is_false() && e.get_upper().is_true()) + if(e.get_lower() == false && e.get_upper() == true) return true; if( e.type().id() == ID_c_bool && e.get_lower().is_zero() && diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 5357fc3046a..51009dbb849 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -441,11 +441,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set) set, [](const abstract_value_objectt &value) { auto c = value.to_constant(); - return c.is_false() || (c.id() == ID_min_value); + return c == false || (c.id() == ID_min_value); }, [](const abstract_value_objectt &value) { auto c = value.to_constant(); - return c.is_true() || (c.id() == ID_max_value); + return c == true || (c.id() == ID_max_value); }); } diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index c969bf12575..9b2e3723627 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -116,7 +116,7 @@ void c_typecheck_baset::typecheck_code(codet &code) implicit_typecast_bool(code.op0()); make_constant(code.op0()); - if(code.op0().is_false()) + if(code.op0() == false) { // failed error().source_location = code.find_source_location(); @@ -951,7 +951,7 @@ void c_typecheck_baset::typecheck_conditional_targets( auto &condition = conditional_target_group.condition(); typecheck_spec_condition(condition); - if(condition.is_true()) + if(condition == true) { // if the condition is trivially true, // simplify expr and expose the bare expressions diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 1534260a50e..f381a2ccc12 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -3635,9 +3635,9 @@ exprt c_typecheck_baset::do_special_functions( mp_integer arg1; - if(expr.arguments()[1].is_true()) + if(expr.arguments()[1] == true) arg1=1; - else if(expr.arguments()[1].is_false()) + else if(expr.arguments()[1] == false) arg1=0; else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1)) { @@ -3679,7 +3679,7 @@ exprt c_typecheck_baset::do_special_functions( typecast_exprt::conditional_cast(expr.arguments()[0], bool_typet()); make_constant(arg0); - if(arg0.is_true()) + if(arg0 == true) return expr.arguments()[1]; else return expr.arguments()[2]; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index d80669f5f42..1228509d742 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -1129,12 +1129,12 @@ void c_typecheck_baset::typecheck_compound_body( assertion = typecast_exprt(assertion, bool_typet()); make_constant(assertion); - if(assertion.is_false()) + if(assertion == false) { throw errort().with_location(it->source_location()) << "failed _Static_assert"; } - else if(!assertion.is_true()) + else if(assertion != true) { // should warn/complain } @@ -1303,9 +1303,9 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) typecheck_expr(tmp_v); add_rounding_mode(tmp_v); simplify(tmp_v, *this); - if(tmp_v.is_true()) + if(tmp_v == true) value=1; - else if(tmp_v.is_false()) + else if(tmp_v == false) value=0; else if( tmp_v.is_constant() && !to_integer(to_constant_expr(tmp_v), value)) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 705936ad81d..58260d26282 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1856,7 +1856,7 @@ std::string expr2ct::convert_constant( } else if(type.id()==ID_bool) { - dest=convert_constant_bool(src.is_true()); + dest = convert_constant_bool(src == true); } else if(type.id()==ID_unsignedbv || type.id()==ID_signedbv || @@ -3559,7 +3559,7 @@ std::string expr2ct::convert_conditional_target_group(const exprt &src) std::string dest; unsigned p; const auto &cond = src.operands().front(); - if(!cond.is_true()) + if(cond != true) { dest += convert_with_precedence(cond, p); dest += ": "; diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 6ff092e2555..8db7d255030 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -1776,7 +1776,7 @@ void goto_check_ct::add_guarded_property( enable_simplify ? simplify_expr(asserted_expr, ns) : asserted_expr; // throw away trivial properties? - if(!retain_trivial && simplified_expr.is_true()) + if(!retain_trivial && simplified_expr == true) return; // add the guard @@ -2245,7 +2245,7 @@ void goto_check_ct::goto_check( // These are further 'exit points' of the program const exprt simplified_guard = simplify_expr(i.condition(), ns); if( - enable_memory_cleanup_check && simplified_guard.is_false() && + enable_memory_cleanup_check && simplified_guard == false && (function_identifier == "abort" || function_identifier == "exit" || function_identifier == "_Exit" || (i.labels.size() == 1 && i.labels.front() == "__VERIFIER_abort"))) diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp index 5e49ce90f98..5cb721e8734 100644 --- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp +++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp @@ -215,7 +215,7 @@ static exprt convert_statement_expression( { exprt condition = current_it->condition(); replace_expr(value_map, condition); - if(!condition.is_true()) + if(condition != true) { auto next_it = current_it->targets.front(); exprt copy_path_condition = path_condition; diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp index 382c5725af3..60674e6e430 100644 --- a/src/ansi-c/goto-conversion/goto_convert.cpp +++ b/src/ansi-c/goto-conversion/goto_convert.cpp @@ -419,7 +419,7 @@ void goto_convertt::optimize_guarded_gotos(goto_programt &dest) if( it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() || - !it_goto_y->condition().is_true() || it_goto_y->is_target()) + it_goto_y->condition() != true || it_goto_y->is_target()) { continue; } @@ -702,7 +702,7 @@ void goto_convertt::convert( typecast_exprt::conditional_cast(code.op0(), bool_typet()); simplify(assertion, ns); INVARIANT_WITH_DIAGNOSTICS( - !assertion.is_false(), + assertion != false, "static assertion is false", code.op0().find_source_location()); } @@ -745,7 +745,7 @@ void goto_convertt::convert_block( // in a prior break/continue/return already, don't create dead code if( !dest.empty() && dest.instructions.back().is_goto() && - dest.instructions.back().condition().is_true()) + dest.instructions.back().condition() == true) { // don't do destructors when we are unreachable } @@ -1776,7 +1776,7 @@ void goto_convertt::generate_ifthenelse( // do guarded assertions directly if( is_size_one(true_case) && true_case.instructions.back().is_assert() && - true_case.instructions.back().condition().is_false() && + true_case.instructions.back().condition() == false && true_case.instructions.back().labels.empty()) { // The above conjunction deliberately excludes the instance @@ -1794,7 +1794,7 @@ void goto_convertt::generate_ifthenelse( // similarly, do guarded assertions directly if( is_size_one(false_case) && false_case.instructions.back().is_assert() && - false_case.instructions.back().condition().is_false() && + false_case.instructions.back().condition() == false && false_case.instructions.back().labels.empty()) { // The above conjunction deliberately excludes the instance @@ -1814,7 +1814,7 @@ void goto_convertt::generate_ifthenelse( if( is_empty(false_case) && true_case.instructions.size() == 2 && true_case.instructions.front().is_assert() && - simplify_expr(true_case.instructions.front().condition(), ns).is_false() && + simplify_expr(true_case.instructions.front().condition(), ns) == false && true_case.instructions.front().labels.empty() && true_case.instructions.back().is_other() && true_case.instructions.back().get_other().get_statement() == diff --git a/src/ansi-c/goto-conversion/goto_convert_functions.cpp b/src/ansi-c/goto-conversion/goto_convert_functions.cpp index 07a3c3713e1..8c24dedeee9 100644 --- a/src/ansi-c/goto-conversion/goto_convert_functions.cpp +++ b/src/ansi-c/goto-conversion/goto_convert_functions.cpp @@ -108,7 +108,7 @@ void goto_convert_functionst::add_return( while(true) { // unconditional goto, say from while(1)? - if(last_instruction->is_goto() && last_instruction->condition().is_true()) + if(last_instruction->is_goto() && last_instruction->condition() == true) { return; } diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index 4328428b326..c773b91108f 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -67,9 +67,9 @@ std::string cpp_typecheckt::template_suffix( // this must be a constant, which includes true/false mp_integer i; - if(e.is_true()) + if(e == true) i=1; - else if(e.is_false()) + else if(e == false) i=0; else if(to_integer(to_constant_expr(e), i)) { diff --git a/src/cpp/cpp_typecheck_static_assert.cpp b/src/cpp/cpp_typecheck_static_assert.cpp index a792c010355..49d2cd7dad4 100644 --- a/src/cpp/cpp_typecheck_static_assert.cpp +++ b/src/cpp/cpp_typecheck_static_assert.cpp @@ -21,7 +21,7 @@ void cpp_typecheckt::convert(cpp_static_assertt &cpp_static_assert) implicit_typecast_bool(cpp_static_assert.op0()); make_constant(cpp_static_assert.op0()); - if(cpp_static_assert.op0().is_false()) + if(cpp_static_assert.op0() == false) { // failed error().source_location=cpp_static_assert.source_location(); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index f562d5fe4ca..17c92ffdd34 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -119,9 +119,9 @@ std::string expr2cppt::convert_constant( if(src.type().id() == ID_c_bool) { // C++ has built-in Boolean constants, in contrast to C - if(src.is_true()) + if(src == true) return "true"; - else if(src.is_false()) + else if(src == false) return "false"; } diff --git a/src/cprover/inductiveness.cpp b/src/cprover/inductiveness.cpp index 6f4484fae12..aa2e07719e2 100644 --- a/src/cprover/inductiveness.cpp +++ b/src/cprover/inductiveness.cpp @@ -36,7 +36,7 @@ bool is_subsumed( bool verbose, const namespacet &ns) { - if(b.is_true()) + if(b == true) return true; // anything subsumes 'true' if(a1.find(false_exprt()) != a1.end()) @@ -161,7 +161,7 @@ inductiveness_resultt inductiveness_check( << frame_ref.index << consolet::reset << ' '; // trivially true? - if(invariant.is_true()) + if(invariant == true) { if(solver_options.verbose) std::cout << "trivial\n"; diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp index 88dc0f22ef0..7440a7a0153 100644 --- a/src/cprover/instrument_contracts.cpp +++ b/src/cprover/instrument_contracts.cpp @@ -110,12 +110,12 @@ exprt assigns_match(const exprt &assigns, const exprt &lhs) if(lhs.id() == ID_member) { - if(assigns_match(assigns, to_member_expr(lhs).struct_op()).is_true()) + if(assigns_match(assigns, to_member_expr(lhs).struct_op()) == true) return true_exprt(); } else if(lhs.id() == ID_index) { - if(assigns_match(assigns, to_index_expr(lhs).array()).is_true()) + if(assigns_match(assigns, to_index_expr(lhs).array()) == true) return true_exprt(); } @@ -169,7 +169,7 @@ static exprt make_assigns_assertion( auto match = assigns_match(a, lhs); // trivial? - if(match.is_true()) + if(match == true) return true_exprt(); disjuncts.push_back(std::move(match)); diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp index 046fbbcd84c..036ace61a22 100644 --- a/src/cprover/may_alias.cpp +++ b/src/cprover/may_alias.cpp @@ -179,7 +179,7 @@ same_address(const exprt &a, const exprt &b, const namespacet &ns) CHECK_RETURN(base_same_address.has_value()); - if(base_same_address->is_false()) + if(*base_same_address == false) return false_expr; else { diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp index d11f031a8b5..1d3770ba68c 100644 --- a/src/cprover/simplify_state_expr.cpp +++ b/src/cprover/simplify_state_expr.cpp @@ -73,7 +73,7 @@ exprt simplify_evaluate_update( if(may_alias.has_value()) { // 'simple' case - if(may_alias->is_true()) + if(*may_alias == true) { // The object is known to be the same. // (ς[A:=V])(A) --> V @@ -83,7 +83,7 @@ exprt simplify_evaluate_update( address_taken, ns); } - else if(may_alias->is_false()) + else if(*may_alias == false) { // The object is known to be different. // (ς[❝x❞:=V])(❝y❞) --> ς(❝y❞) @@ -680,7 +680,7 @@ exprt simplify_is_cstring_expr( auto may_alias = ::may_alias(pointer, update_state_expr.address(), address_taken, ns); - if(may_alias.has_value() && may_alias->is_false()) + if(may_alias.has_value() && *may_alias == false) { // different objects // cstring(s[x:=v], p) --> cstring(s, p) @@ -776,7 +776,7 @@ exprt simplify_cstrlen_expr( auto may_be_same_object = ::may_be_same_object( pointer, update_state_expr.address(), address_taken, ns); - if(may_be_same_object.is_false()) + if(may_be_same_object == false) { // different objects // cstrlen(s[x:=v], p) --> cstrlen(s, p) diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 56ef744c049..3ebd8f42f41 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -134,7 +134,7 @@ std::vector state_encodingt::incoming_symbols(loct loc) const // conditional jump from loc_in to loc? if( - loc_in->is_goto() && !loc_in->condition().is_true() && + loc_in->is_goto() && loc_in->condition() != true && loc != std::next(loc_in)) { suffix = "T"; @@ -617,7 +617,7 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function) forall_goto_program_instructions(it, goto_function.body) { auto next = std::next(it); - if(it->is_goto() && it->condition().is_true()) + if(it->is_goto() && it->condition() == true) { } else if(next != goto_function.body.instructions.end()) @@ -1013,7 +1013,7 @@ void state_encodingt::encode( // We produce ∅ when the 'other' branch is taken. Get the condition. const auto &condition = loc->condition(); - if(condition.is_true()) + if(condition == true) { dest << equal_exprt(out_state_expr(loc), in_state_expr(loc)); } diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp index 9e9282f6de7..73a16bb50a8 100644 --- a/src/goto-analyzer/static_verifier.cpp +++ b/src/goto-analyzer/static_verifier.cpp @@ -92,11 +92,11 @@ check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns) } domain.ai_simplify(e, ns); - if(e.is_true()) + if(e == true) { return ai_verifier_statust::TRUE; } - else if(e.is_false()) + else if(e == false) { return ai_verifier_statust::FALSE_IF_REACHABLE; } diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 55726c91e2b..33da2e6640f 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -343,7 +343,7 @@ bool taint_analysist::operator()( continue; exprt result = custom_bitvector_analysis.eval(i_it->condition(), i_it); - if(simplify_expr(std::move(result), ns).is_true()) + if(simplify_expr(std::move(result), ns) == true) continue; if(first) diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index 6e31d312d77..421b5d016c6 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -55,9 +55,10 @@ ssa_step_matches_failing_property(const irep_idt &property_id) { return [property_id]( symex_target_equationt::SSA_stepst::const_iterator step, - const decision_proceduret &decision_procedure) { + const decision_proceduret &decision_procedure) + { return step->is_assert() && step->property_id == property_id && - decision_procedure.get(step->cond_handle).is_false(); + decision_procedure.get(step->cond_handle) == false; }; } @@ -250,8 +251,8 @@ void update_properties_status_from_symex_target_equation( // Don't update status of properties that are constant 'false'; // we wouldn't have traces for them. - const auto status = step.cond_expr.is_true() ? property_statust::PASS - : property_statust::UNKNOWN; + const auto status = step.cond_expr == true ? property_statust::PASS + : property_statust::UNKNOWN; auto emplace_result = properties.emplace( property_id, property_infot{step.source.pc, step.comment, status}); diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp index 34bc7b0c191..a40d9d41581 100644 --- a/src/goto-checker/counterexample_beautification.cpp +++ b/src/goto-checker/counterexample_beautification.cpp @@ -37,7 +37,7 @@ void counterexample_beautificationt::get_minimization_list( it->is_assignment() && it->assignment_type == symex_targett::assignment_typet::STATE) { - if(!prop_conv.get(it->guard_handle).is_false()) + if(prop_conv.get(it->guard_handle) != false) { const typet &type = it->ssa_lhs.type(); @@ -76,8 +76,8 @@ counterexample_beautificationt::get_failed_property( it++) { if( - it->is_assert() && prop_conv.get(it->guard_handle).is_true() && - prop_conv.get(it->cond_handle).is_false()) + it->is_assert() && prop_conv.get(it->guard_handle) == true && + prop_conv.get(it->cond_handle) == false) { return it; } diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp index 7e70100657c..bd7200e3fec 100644 --- a/src/goto-checker/goto_symex_fault_localizer.cpp +++ b/src/goto-checker/goto_symex_fault_localizer.cpp @@ -108,11 +108,11 @@ void goto_symex_fault_localizert::update_scores( for(auto &l : localization_points) { auto &score = l.second->second; - if(solver.get(l.first).is_true()) + if(solver.get(l.first) == true) { score++; } - else if(solver.get(l.first).is_false() && score > 0) + else if(solver.get(l.first) == false && score > 0) { score--; } diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/src/goto-checker/goto_symex_property_decider.cpp index 7dcc0fe1c40..51bcd5575c3 100644 --- a/src/goto-checker/goto_symex_property_decider.cpp +++ b/src/goto-checker/goto_symex_property_decider.cpp @@ -88,9 +88,7 @@ void goto_symex_property_decidert::add_constraint_from_goals( for(const auto &goal_pair : goal_map) { - if( - select_property(goal_pair.first) && - !goal_pair.second.condition.is_false()) + if(select_property(goal_pair.first) && goal_pair.second.condition != false) { disjuncts.push_back(goal_pair.second.condition); } @@ -143,9 +141,7 @@ void goto_symex_property_decidert::update_properties_status_from_goals( { auto &status = properties.at(goal_pair.first).status; if( - solver->decision_procedure() - .get(goal_pair.second.condition) - .is_true() && + solver->decision_procedure().get(goal_pair.second.condition) == true && status != property_statust::FAIL) { status |= property_statust::FAIL; diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index de4ecdd28b4..b23ae91e81b 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -59,7 +59,7 @@ void symex_bmct::symex_step( if( !state.guard.is_false() && state.source.pc->is_assume() && - simplify_expr(state.source.pc->condition(), ns).is_false()) + simplify_expr(state.source.pc->condition(), ns) == false) { log.statistics() << "aborting path on assume(false) at " << state.source.pc->source_location() << " thread " @@ -88,7 +88,7 @@ void symex_bmct::symex_step( // sure the goto is considered covered if( cur_pc->is_goto() && cur_pc->get_target() != state.source.pc && - cur_pc->condition().is_true()) + cur_pc->condition() == true) symex_coverage.covered(cur_pc, cur_pc->get_target()); else if(!state.guard.is_false()) symex_coverage.covered(cur_pc, state.source.pc); @@ -111,7 +111,7 @@ void symex_bmct::merge_goto( // could the branch possibly be taken? !prev_guard.is_false() && !state.guard.is_false() && // branches only, no single-successor goto - !prev_pc->condition().is_true()) + prev_pc->condition() != true) symex_coverage.covered(prev_pc, state.source.pc); } diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 9fbeaa5875b..c4ecf3063b9 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -44,7 +44,7 @@ goto_programt::targett acceleratet::find_back_jump( for(const auto &t : loop) { if( - t->is_goto() && t->condition().is_true() && t->targets.size() == 1 && + t->is_goto() && t->condition() == true && t->targets.size() == 1 && t->targets.front() == loop_header && t->location_number > back_jump->location_number) { diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index a0a6dcd37ad..723dd60dd1f 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -256,7 +256,7 @@ exprt acceleration_utilst::precondition(patht &path) // Ignore. } - if(!r_it->guard.is_true() && !r_it->guard.is_nil()) + if(r_it->guard != true && !r_it->guard.is_nil()) { // The guard isn't constant true, so we need to accumulate that too. ret=implies_exprt(r_it->guard, ret); diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp index 43256e6fc1a..4b8cf7291e9 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.cpp +++ b/src/goto-instrument/accelerate/cone_of_influence.cpp @@ -89,7 +89,7 @@ void cone_of_influencet::get_succs( if(rit->is_goto()) { - if(!rit->condition().is_false()) + if(rit->condition() != false) { // Branch can be taken. for(goto_programt::targetst::const_iterator t=rit->targets.begin(); @@ -102,14 +102,14 @@ void cone_of_influencet::get_succs( } } - if(rit->condition().is_true()) + if(rit->condition() == true) { return; } } else if(rit->is_assume() || rit->is_assert()) { - if(rit->condition().is_false()) + if(rit->condition() == false) { return; } diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 954be5565e6..7b30906e310 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -789,7 +789,7 @@ void disjunctive_polynomial_accelerationt::build_path( for(const auto &succ : succs) { exprt &distinguisher=distinguishing_points[succ]; - bool taken=scratch_program.eval(distinguisher).is_true(); + bool taken = scratch_program.eval(distinguisher) == true; if(taken) { @@ -992,7 +992,7 @@ void disjunctive_polynomial_accelerationt::record_path( it != distinguishers.end(); ++it) { - path_val[*it]=program.eval(*it).is_true(); + path_val[*it] = program.eval(*it) == true; } accelerated_paths.push_back(path_val); diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 41a88788c58..bb288bd7f75 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -785,7 +785,7 @@ exprt polynomial_acceleratort::precondition(patht &path) // Ignore. } - if(!r_it->guard.is_true() && !r_it->guard.is_nil()) + if(r_it->guard != true && !r_it->guard.is_nil()) { // The guard isn't constant true, so we need to accumulate that too. ret=implies_exprt(r_it->guard, ret); diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index eb645a5a9b1..2b856221488 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -136,7 +136,7 @@ void sat_path_enumeratort::build_path( for(const auto &succ : succs) { exprt &distinguisher=distinguishing_points[succ]; - bool taken=scratch_program.eval(distinguisher).is_true(); + bool taken = scratch_program.eval(distinguisher) == true; if(taken) { @@ -335,7 +335,7 @@ void sat_path_enumeratort::record_path(scratch_programt &program) distinguish_valuest path_val; for(const auto &expr : distinguishers) - path_val[expr]=program.eval(expr).is_true(); + path_val[expr] = program.eval(expr) == true; accelerated_paths.push_back(path_val); } diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index ddbc688aa47..40d5c667c8b 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -231,7 +231,7 @@ void check_call_sequencet::operator()() { goto_programt::const_targett t=e.pc->get_target(); - if(e.pc->condition().is_true()) + if(e.pc->condition() == true) e.pc=t; else { diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 8cb69c96ed8..7dc900daa9c 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -375,7 +375,7 @@ void code_contractst::check_apply_loop_contracts( } // TODO: Fix loop contract handling for do/while loops. - if(loop_end->is_goto() && !loop_end->condition().is_true()) + if(loop_end->is_goto() && loop_end->condition() != true) { log.error() << "Loop contracts are unsupported on do/while loops: " << loop_head_location << messaget::eom; @@ -782,7 +782,7 @@ void code_contractst::apply_function_contract( // Generate: assume(ensures) for(auto &clause : instantiated_ensures_clauses) { - if(clause.is_false()) + if(clause == false) { throw invalid_input_exceptiont( std::string("Attempt to assume false at ") @@ -1353,7 +1353,7 @@ void code_contractst::add_contract_check( { auto instantiated_clause = to_lambda_expr(clause).application(instantiation_values); - if(instantiated_clause.is_false()) + if(instantiated_clause == false) { throw invalid_input_exceptiont( std::string("Attempt to assume false at ") diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp index 505ca6c6695..a3105efe47b 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp @@ -156,7 +156,7 @@ void dfcc_check_loop_normal_form(goto_programt &goto_program, messaget &log) // IF TRUE GOTO HEAD // EXIT: SKIP // ``` - if(latch->has_condition() && !latch->condition().is_true()) + if(latch->has_condition() && latch->condition() != true) { const source_locationt &loc = latch->source_location(); const auto &exit = diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index b620714c78e..c3b6d2efa1a 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -585,8 +585,8 @@ car_exprt instrument_spec_assignst::create_car_expr( valid_var, lower_bound_var, upper_bound_var, - is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN - : car_havoc_methodt::HAVOC_SLICE}; + is_ptr_to_ptr == true ? car_havoc_methodt::NONDET_ASSIGN + : car_havoc_methodt::HAVOC_SLICE}; } } } @@ -685,7 +685,7 @@ void instrument_spec_assignst::target_validity_assertion( std::string comment = "Check that "; comment += from_expr(ns, "", car.target()); comment += " is valid"; - if(!car.condition().is_true()) + if(car.condition() != true) { comment += " when "; comment += from_expr(ns, "", car.condition()); @@ -719,7 +719,7 @@ void instrument_spec_assignst::inclusion_check_assertion( std::string comment = "Check that "; if(!is_assigns_clause_replacement_tracking_comment(orig_comment)) { - if(!car.condition().is_true()) + if(car.condition() != true) comment += from_expr(ns, "", car.condition()) + ": "; comment += from_expr(ns, "", car.target()); } diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp index da3b06dfa86..ecd6e779b72 100644 --- a/src/goto-instrument/contracts/utils.cpp +++ b/src/goto-instrument/contracts/utils.cpp @@ -151,7 +151,7 @@ void havoc_assigns_targetst::append_havoc_code_for_expr( { const auto &ptr = funcall.arguments().at(0); const auto &size = funcall.arguments().at(1); - if(funcall.arguments().at(2).is_true()) + if(funcall.arguments().at(2) == true) { append_havoc_pointer_code(expr.source_location(), ptr, dest); } @@ -263,7 +263,7 @@ void simplify_gotos(goto_programt &goto_program, const namespacet &ns) { if( instruction.is_goto() && - simplify_expr(instruction.condition(), ns).is_false()) + simplify_expr(instruction.condition(), ns) == false) instruction.turn_into_skip(); } } diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index 36af6b16964..23df805b4dc 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -21,9 +21,7 @@ std::optional cover_basic_blockst::continuation_of_block( return {}; const goto_programt::targett in_t = *instruction->incoming_edges.cbegin(); - if( - in_t->is_goto() && !in_t->is_backwards_goto() && - in_t->condition().is_true()) + if(in_t->is_goto() && !in_t->is_backwards_goto() && in_t->condition() == true) return block_map[in_t]; return {}; diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp index efec9d5409c..803b4f4b78c 100644 --- a/src/goto-instrument/cover_instrument_branch.cpp +++ b/src/goto-instrument/cover_instrument_branch.cpp @@ -25,8 +25,7 @@ void cover_branch_instrumentert::instrument( const bool is_function_entry_point = i_it == goto_program.instructions.begin(); - const bool is_conditional_goto = - i_it->is_goto() && !i_it->condition().is_true(); + const bool is_conditional_goto = i_it->is_goto() && i_it->condition() != true; if(!is_function_entry_point && !is_conditional_goto) return; diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp index 770a52a5f26..45da7c038cb 100644 --- a/src/goto-instrument/dot.cpp +++ b/src/goto-instrument/dot.cpp @@ -108,7 +108,7 @@ void dott::write_dot_subgraph( std::stringstream tmp; if(it->is_goto()) { - if(it->condition().is_true()) + if(it->condition() == true) tmp.str("Goto"); else { @@ -320,13 +320,13 @@ void dott::find_next( std::set &tres, std::set &fres) { - if(it->is_goto() && !it->condition().is_false()) + if(it->is_goto() && it->condition() != false) { for(const auto &target : it->targets) tres.insert(target); } - if(it->is_goto() && it->condition().is_true()) + if(it->is_goto() && it->condition() == true) return; goto_programt::const_targett next = it; next++; diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index f8b8c8a6414..1e2b29f125d 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -281,7 +281,7 @@ void full_slicert::operator()( else if(implicit(instruction)) add_to_queue(queue, instruction_node_index, instruction); else if( - (instruction->is_goto() && instruction->condition().is_true()) || + (instruction->is_goto() && instruction->condition() == true) || instruction->is_throw()) jumps.push_back(instruction_node_index); else if(instruction->is_decl()) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 87edc71b678..87eee70ed89 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -550,7 +550,7 @@ goto_programt::const_targett goto_program2codet::convert_goto( (upper_bound==goto_program.instructions.end() || upper_bound->location_number > loop_entry->second->location_number)) return convert_goto_while(target, loop_entry->second, dest); - else if(!target->condition().is_true()) + else if(target->condition() != true) return convert_goto_switch(target, upper_bound, dest); else if(!loop_last_stack.empty()) return convert_goto_break_continue(target, upper_bound, dest); @@ -580,7 +580,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_while( w.cond() = not_exprt(target->condition()); simplify(w.cond(), ns); } - else if(target->condition().is_true()) + else if(target->condition() == true) { target = convert_goto_goto(target, to_code_block(w.body())); } @@ -597,11 +597,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_while( loop_last_stack.pop_back(); convert_labels(loop_end, to_code_block(w.body())); - if(loop_end->condition().is_false()) + if(loop_end->condition() == false) { to_code_block(w.body()).add(code_breakt()); } - else if(!loop_end->condition().is_true()) + else if(loop_end->condition() != true) { code_ifthenelset i(not_exprt(loop_end->condition()), code_breakt()); simplify(i.cond(), ns); @@ -624,15 +624,15 @@ goto_programt::const_targett goto_program2codet::convert_goto_while( f.swap(w); } - else if(w.body().has_operands() && - w.cond().is_true()) + else if(w.body().has_operands() && w.cond() == true) { const codet &back=to_code(w.body().operands().back()); - if(back.get_statement()==ID_break || - (back.get_statement()==ID_ifthenelse && - to_code_ifthenelse(back).cond().is_true() && - to_code_ifthenelse(back).then_case().get_statement()==ID_break)) + if( + back.get_statement() == ID_break || + (back.get_statement() == ID_ifthenelse && + to_code_ifthenelse(back).cond() == true && + to_code_ifthenelse(back).then_case().get_statement() == ID_break)) { w.body().operands().pop_back(); code_dowhilet d(false_exprt(), w.body()); @@ -667,7 +667,7 @@ goto_programt::const_targett goto_program2codet::get_cases( { if( cases_it->is_goto() && !cases_it->is_backwards_goto() && - cases_it->condition().is_true()) + cases_it->condition() == true) { default_target=cases_it->get_target(); @@ -834,7 +834,7 @@ bool goto_program2codet::remove_default( next_case != goto_program.instructions.end() && next_case == default_target && (!it->case_last->is_goto() || - (it->case_last->condition().is_true() && + (it->case_last->condition() == true && it->case_last->get_target() == default_target))) { // if there is no goto here, yet we got here, all others would @@ -845,7 +845,7 @@ bool goto_program2codet::remove_default( // jumps to default are ok if( - it->case_last->is_goto() && it->case_last->condition().is_true() && + it->case_last->is_goto() && it->case_last->condition() == true && it->case_last->get_target() == default_target) continue; @@ -1059,7 +1059,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if( has_else = before_else->is_goto() && before_else->get_target()->location_number > end_if->location_number && - before_else->condition().is_true() && + before_else->condition() == true && (upper_bound == goto_program.instructions.end() || upper_bound->location_number >= before_else->get_target()->location_number); @@ -1145,7 +1145,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( copy_source_location(target, i); - if(i.cond().is_true()) + if(i.cond() == true) dest.add(std::move(i.then_case())); else dest.add(std::move(i)); @@ -1169,7 +1169,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( copy_source_location(target, i); - if(i.cond().is_true()) + if(i.cond() == true) dest.add(std::move(i.then_case())); else dest.add(std::move(i)); @@ -1227,7 +1227,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto( copy_source_location(target, i); - if(i.cond().is_true()) + if(i.cond() == true) dest.add(std::move(i.then_case())); else dest.add(std::move(i)); @@ -1292,7 +1292,7 @@ goto_programt::const_targett goto_program2codet::convert_start_thread( // 2: code in existing thread /* check the structure and compute the iterators */ DATA_INVARIANT( - next->is_goto() && next->condition().is_true(), "START THREAD pattern"); + next->is_goto() && next->condition() == true, "START THREAD pattern"); DATA_INVARIANT(!next->is_backwards_goto(), "START THREAD pattern"); DATA_INVARIANT( thread_start->location_number < next->get_target()->location_number, @@ -1508,8 +1508,8 @@ void goto_program2codet::cleanup_code( if(do_while.body().get_statement()==ID_skip) do_while.set_statement(ID_while); // do stmt while(false) is just stmt - else if(do_while.cond().is_false() && - do_while.body().get_statement()!=ID_block) + else if( + do_while.cond() == false && do_while.body().get_statement() != ID_block) code=do_while.body(); } } @@ -1692,13 +1692,13 @@ void goto_program2codet::cleanup_code_ifthenelse( // assert(false) expands to if(true) assert(false), simplify again (and also // simplify other cases) if( - cond.is_true() && + cond == true && (i_t_e.else_case().is_nil() || !has_labels(i_t_e.else_case()))) { codet tmp = i_t_e.then_case(); code.swap(tmp); } - else if(cond.is_false() && !has_labels(i_t_e.then_case())) + else if(cond == false && !has_labels(i_t_e.then_case())) { if(i_t_e.else_case().is_nil()) code=code_skipt(); diff --git a/src/goto-instrument/horn_encoding.cpp b/src/goto-instrument/horn_encoding.cpp index 4d316fe47bd..d0202e60d64 100644 --- a/src/goto-instrument/horn_encoding.cpp +++ b/src/goto-instrument/horn_encoding.cpp @@ -428,7 +428,7 @@ std::vector state_encodingt::incoming_symbols(loct loc) const // conditional jump from loc_in to loc? if( - loc_in->is_goto() && !loc_in->condition().is_true() && + loc_in->is_goto() && loc_in->condition() != true && loc != std::next(loc_in)) { suffix = "T"; @@ -688,7 +688,7 @@ void state_encodingt::setup_incoming(const goto_functiont &goto_function) forall_goto_program_instructions(it, goto_function.body) { auto next = std::next(it); - if(it->is_goto() && it->condition().is_true()) + if(it->is_goto() && it->condition() == true) { } else if(next != goto_function.body.instructions.end()) @@ -921,7 +921,7 @@ void state_encodingt::encode( // We produce ∅ when the 'other' branch is taken. Get the condition. const auto &condition = loc->condition(); - if(condition.is_true()) + if(condition == true) { dest << equal_exprt(out_state_expr(loc), in_state_expr(loc)); } diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index c99e19f2280..88936c78983 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -140,7 +140,7 @@ void goto_unwindt::unwind( exprt exit_cond = false_exprt(); // default is false - if(!t->condition().is_true()) // cond in backedge + if(t->condition() != true) // cond in backedge { exit_cond = boolean_negate(t->condition()); } @@ -190,7 +190,7 @@ void goto_unwindt::unwind( goto_programt::const_targett t_before=loop_exit; t_before--; - if(!t_before->is_goto() || !t_before->condition().is_true()) + if(!t_before->is_goto() || t_before->condition() != true) { goto_programt::targett t_goto = goto_program.insert_before( loop_exit, diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index e271d761b19..22e6c44abd8 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -320,7 +320,7 @@ void cfg_baset::compute_edges_goto( { if( next_PC != goto_program.instructions.end() && - !instruction.condition().is_true()) + instruction.condition() != true) { this->add_edge(entry, entry_map[next_PC]); } @@ -501,7 +501,7 @@ void cfg_baset::compute_edges( case ASSUME: // false guard -> no successor - if(instruction.condition().is_false()) + if(instruction.condition() == false) break; case ASSIGN: diff --git a/src/goto-programs/ensure_one_backedge_per_target.cpp b/src/goto-programs/ensure_one_backedge_per_target.cpp index f9f3c2c6d1e..295788c7010 100644 --- a/src/goto-programs/ensure_one_backedge_per_target.cpp +++ b/src/goto-programs/ensure_one_backedge_per_target.cpp @@ -57,7 +57,7 @@ bool ensure_one_backedge_per_target( // If the last backedge is a conditional jump, add an extra unconditional // backedge after it: - if(!last_backedge->condition().is_true()) + if(last_backedge->condition() != true) { auto new_goto = goto_program.insert_after(last_backedge, goto_programt::make_goto(it)); diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index db89fd0f4fd..2539394b69a 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -79,7 +79,7 @@ std::ostream &goto_programt::instructiont::output(std::ostream &out) const case GOTO: case INCOMPLETE_GOTO: - if(!condition().is_true()) + if(condition() != true) { out << "IF " << format(condition()) << " THEN "; } @@ -525,7 +525,7 @@ std::string as_string( return "(NO INSTRUCTION TYPE)"; case GOTO: - if(!i.condition().is_true()) + if(i.condition() != true) { result += "IF " + from_expr(ns, function, i.condition()) + " THEN "; } @@ -742,7 +742,7 @@ void goto_programt::copy_from(const goto_programt &src) bool goto_programt::has_assertion() const { for(const auto &i : instructions) - if(i.is_assert() && !i.condition().is_true()) + if(i.is_assert() && i.condition() != true) return true; return false; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 94d87c8fdfe..234d759f6c9 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -1136,7 +1136,7 @@ std::list goto_programt::get_successors( { std::list successors(i.targets.begin(), i.targets.end()); - if(!i.condition().is_true() && next != instructions.end()) + if(i.condition() != true && next != instructions.end()) successors.push_back(next); return successors; @@ -1166,7 +1166,7 @@ std::list goto_programt::get_successors( if(i.is_assume()) { - return !i.condition().is_false() && next != instructions.end() + return i.condition() != false && next != instructions.end() ? std::list{next} : std::list(); } diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 417c4cbfe7f..c3e283978fa 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -227,7 +227,7 @@ std::string trace_numeric_value( } else if(type.id()==ID_bool) { - return expr.is_true()?"1":"0"; + return expr == true ? "1" : "0"; } else if(type.id()==ID_integer) { diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index e0aef679768..2c0722d50a4 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -238,7 +238,7 @@ static bool filter_out( prev_it->pc->source_location() == it->pc->source_location()) return true; - if(it->is_goto() && it->pc->condition().is_true()) + if(it->is_goto() && it->pc->condition() == true) return true; const source_locationt &source_location = it->pc->source_location(); @@ -546,7 +546,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) if( it->hidden || (!it->is_assignment() && !it->is_goto() && !it->is_assert()) || - (it->is_goto() && it->source.pc->condition().is_true()) || + (it->is_goto() && it->source.pc->condition() == true) || source_location.is_nil() || source_location.is_built_in() || source_location.get_line().empty()) { diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index 72707e3692f..3590fe63190 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -382,7 +382,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr) } else if(expr.is_boolean()) { - return {expr.is_true()}; + return {expr == true}; } else if(expr.type().id()==ID_string) { diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp index 6331ebe2f6a..d3473b9d65d 100644 --- a/src/goto-programs/json_expr.cpp +++ b/src/goto-programs/json_expr.cpp @@ -288,8 +288,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode) else if(type.id() == ID_bool) { result["name"] = json_stringt("boolean"); - result["binary"] = json_stringt(expr.is_true() ? "1" : "0"); - result["data"] = jsont::json_boolean(expr.is_true()); + result["binary"] = json_stringt(expr == true ? "1" : "0"); + result["data"] = jsont::json_boolean(expr == true); } else if(type.id() == ID_string) { diff --git a/src/goto-programs/remove_skip.cpp b/src/goto-programs/remove_skip.cpp index 8ca1aea3787..008b3fa39d1 100644 --- a/src/goto-programs/remove_skip.cpp +++ b/src/goto-programs/remove_skip.cpp @@ -37,7 +37,7 @@ bool is_skip( if(it->is_goto()) { - if(it->condition().is_false()) + if(it->condition() == false) return true; goto_programt::const_targett next_it = it; @@ -48,7 +48,7 @@ bool is_skip( // A branch to the next instruction is a skip // We also require the guard to be 'true' - return it->condition().is_true() && it->get_target() == next_it; + return it->condition() == true && it->get_target() == next_it; } if(it->is_other()) diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp index fe2e8b94130..aecd889d802 100644 --- a/src/goto-programs/vcd_goto_trace.cpp +++ b/src/goto-programs/vcd_goto_trace.cpp @@ -131,10 +131,10 @@ void output_vcd( // booleans are special in VCD if(type.id() == ID_bool) { - if(step.full_lhs_value.is_true()) + if(step.full_lhs_value == true) out << "1" << "V" << number << "\n"; - else if(step.full_lhs_value.is_false()) + else if(step.full_lhs_value == false) out << "0" << "V" << number << "\n"; else diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp index 2cf54e5261f..50ee90fdd61 100644 --- a/src/goto-programs/xml_expr.cpp +++ b/src/goto-programs/xml_expr.cpp @@ -226,8 +226,8 @@ xmlt xml(const exprt &expr, const namespacet &ns) else if(type.id() == ID_bool) { result.name = "boolean"; - result.set_attribute("binary", constant_expr.is_true() ? "1" : "0"); - result.data = constant_expr.is_true() ? "TRUE" : "FALSE"; + result.set_attribute("binary", constant_expr == true ? "1" : "0"); + result.data = constant_expr == true ? "TRUE" : "FALSE"; } else { diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp index 7e4013f5b6e..f4ba87c77ed 100644 --- a/src/goto-symex/build_goto_trace.cpp +++ b/src/goto-symex/build_goto_trace.cpp @@ -84,9 +84,9 @@ static exprt build_full_lhs_rec( exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond()); - if(tmp.is_true()) + if(tmp == true) return tmp2.true_case(); - else if(tmp.is_false()) + else if(tmp == false) return tmp2.false_case(); else return std::move(tmp2); @@ -241,7 +241,7 @@ void build_goto_trace( const SSA_stept &SSA_step = *it; - if(!decision_procedure.get(SSA_step.guard_handle).is_true()) + if(decision_procedure.get(SSA_step.guard_handle) != true) continue; if(it->is_constraint() || @@ -410,7 +410,7 @@ void build_goto_trace( goto_trace_step.cond_expr = SSA_step.cond_expr; goto_trace_step.cond_value = - decision_procedure.get(SSA_step.cond_handle).is_true(); + decision_procedure.get(SSA_step.cond_handle) == true; } if(SSA_step.source.pc->is_assert() || SSA_step.source.pc->is_assume()) @@ -446,7 +446,7 @@ static bool is_failed_assertion_step( const decision_proceduret &decision_procedure) { return step->is_assert() && - decision_procedure.get(step->cond_handle).is_false(); + decision_procedure.get(step->cond_handle) == false; } void build_goto_trace( diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index c359168b6a0..0608aa29b40 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -344,9 +344,9 @@ exprt goto_symex_statet::l2_rename_rvalues(exprt lvalue, const namespacet &ns) // The condition is an rvalue: auto &if_lvalue = to_if_expr(lvalue); if_lvalue.cond() = rename(if_lvalue.cond(), ns); - if(!if_lvalue.cond().is_false()) + if(if_lvalue.cond() != false) if_lvalue.true_case() = l2_rename_rvalues(if_lvalue.true_case(), ns); - if(!if_lvalue.cond().is_true()) + if(if_lvalue.cond() != true) if_lvalue.false_case() = l2_rename_rvalues(if_lvalue.false_case(), ns); } else if(lvalue.id() == ID_complex_real) @@ -441,7 +441,7 @@ bool goto_symex_statet::l2_thread_read_encoding( } guardt cond = read_guard; - if(!no_write.op().is_false()) + if(no_write.op() != false) cond |= guardt{no_write.op(), guard_manager}; // It is safe to perform constant propagation in case we have read or @@ -485,7 +485,7 @@ bool goto_symex_statet::l2_thread_read_encoding( expr = std::move(ssa_l2); a_s_read.second.push_back(guard); - if(!no_write.op().is_false()) + if(no_write.op() != false) a_s_read.second.back().add(no_write); return true; diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp index bbf2cab2692..8c7d5fa964f 100644 --- a/src/goto-symex/memory_model_sc.cpp +++ b/src/goto-symex/memory_model_sc.cpp @@ -302,7 +302,7 @@ void memory_model_sct::from_read(symex_target_equationt &equation) exprt cond; cond.make_nil(); - if(c_it->first.second==*w_prime && !ws1.is_false()) + if(c_it->first.second == *w_prime && ws1 != false) { exprt fr=before(r, *w); @@ -314,7 +314,7 @@ void memory_model_sct::from_read(symex_target_equationt &equation) and_exprt(r->guard, (*w)->guard, ws1, rf), fr); } - else if(c_it->first.second==*w && !ws2.is_false()) + else if(c_it->first.second == *w && ws2 != false) { exprt fr=before(r, *w_prime); diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index 54d6b58b677..b7fe76345c5 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -148,7 +148,7 @@ void memory_model_tsot::program_order( simplify(cond, ns); } - if(!cond.is_false()) + if(cond != false) { if(ordering.is_nil()) ordering=partial_order_concurrencyt::before( diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index 9ff92da9824..60bf293ef2f 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -51,9 +51,7 @@ void partial_order_concurrencyt::add_init_writes( if(init_done.find(a)!=init_done.end()) continue; - if(spawn_seen || - e_it->is_shared_read() || - !e_it->guard.is_true()) + if(spawn_seen || e_it->is_shared_read() || e_it->guard != true) { init_steps.emplace_back( e_it->source, goto_trace_stept::typet::SHARED_WRITE); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 8b71f111674..cd3185aff42 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -62,7 +62,7 @@ void postcondition( { postconditiont postcondition(ns, value_set, *it, s); postcondition.compute(dest); - if(dest.is_false()) + if(dest == false) return; } } @@ -137,7 +137,7 @@ void postconditiont::strengthen(exprt &dest) exprt equality = get_original_name(equal_exprt{SSA_step.ssa_lhs, SSA_step.ssa_rhs}); - if(dest.is_true()) + if(dest == true) dest.swap(equality); else dest=and_exprt(dest, equality); diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index 76fc7f48a83..93b85b5fbf8 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -70,7 +70,7 @@ void precondition( { preconditiont precondition(ns, value_sets, target, *it, s, message_handler); precondition.compute(dest); - if(dest.is_false()) + if(dest == false) return; } } diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index 5a3bf883037..b0459f20a06 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -929,19 +929,19 @@ std::vector> get_shadow_dereference_candidates( const exprt base_cond = get_matched_base_cond( shadowed_address.address, matched_base_address, ns, log); shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond); - if(base_cond.is_false()) + if(base_cond == false) { continue; } const exprt expr_cond = get_matched_expr_cond(dereference.pointer, expr, ns, log); - if(expr_cond.is_false()) + if(expr_cond == false) { continue; } - if(base_cond.is_true() && expr_cond.is_true()) + if(base_cond == true && expr_cond == true) { #ifdef DEBUG_SHADOW_MEMORY log.debug() << "exact match" << messaget::eom; @@ -952,7 +952,7 @@ std::vector> get_shadow_dereference_candidates( break; } - if(base_cond.is_true()) + if(base_cond == true) { // No point looking at further shadow addresses // as only one of them can match. @@ -1096,19 +1096,19 @@ get_shadow_memory_for_matched_object( const exprt base_cond = get_matched_base_cond( shadowed_address.address, matched_base_address, ns, log); shadow_memory_log_text_and_expr(ns, log, "base_cond", base_cond); - if(base_cond.is_false()) + if(base_cond == false) { continue; } const exprt expr_cond = get_matched_expr_cond(dereference.pointer, expr, ns, log); - if(expr_cond.is_false()) + if(expr_cond == false) { continue; } - if(base_cond.is_true() && expr_cond.is_true()) + if(base_cond == true && expr_cond == true) { log_shadow_memory_message(log, "exact match"); @@ -1118,7 +1118,7 @@ get_shadow_memory_for_matched_object( break; } - if(base_cond.is_true()) + if(base_cond == true) { // No point looking at further shadow addresses // as only one of them can match. diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp index 13c409ea197..379d60284a8 100644 --- a/src/goto-symex/show_program.cpp +++ b/src/goto-symex/show_program.cpp @@ -47,7 +47,7 @@ static void show_step( std::cout << annotation << '(' << string_value << ')'; std::cout << '\n'; - if(!step.guard.is_true()) + if(step.guard != true) { const std::string guard_string = from_expr(ns, function_id, step.guard); std::cout << std::string(std::to_string(count).size() + 3, ' '); @@ -76,7 +76,7 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation) show_step(ns, step, "ASSUME", count); else if(step.is_constraint()) { - PRECONDITION(step.guard.is_true()); + PRECONDITION(step.guard == true); show_step(ns, step, "CONSTRAINT", count); } else if(step.is_shared_read()) diff --git a/src/goto-symex/simplify_expr_with_value_set.cpp b/src/goto-symex/simplify_expr_with_value_set.cpp index c28ab650150..24a519f6364 100644 --- a/src/goto-symex/simplify_expr_with_value_set.cpp +++ b/src/goto-symex/simplify_expr_with_value_set.cpp @@ -91,13 +91,13 @@ static std::optional try_evaluate_pointer_comparison( typecast_exprt::conditional_cast(value.pointer, other_operand.type()), other_operand}, ns); - if(test_equal.is_true()) + if(test_equal == true) { constant_found = true; // We can't break because we have to make sure we find any instances of // ID_unknown or ID_invalid } - else if(!test_equal.is_false()) + else if(test_equal != false) { // We can't conclude anything about the value-set return {}; diff --git a/src/goto-symex/solver_hardness.cpp b/src/goto-symex/solver_hardness.cpp index 95c8ea70033..384928505e6 100644 --- a/src/goto-symex/solver_hardness.cpp +++ b/src/goto-symex/solver_hardness.cpp @@ -246,7 +246,7 @@ solver_hardnesst::goto_instruction2string(goto_programt::const_targett pc) case GOTO: case INCOMPLETE_GOTO: - if(!instruction.condition().is_true()) + if(instruction.condition() != true) { out << "IF " << format(instruction.condition()) << " THEN "; } diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 8207fd4ea82..987cad6b90e 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -173,7 +173,7 @@ void goto_symext::symex_allocate( INVARIANT( zero_init.is_constant(), "allocate expects constant as second argument"); - if(!zero_init.is_zero() && !zero_init.is_false()) + if(!zero_init.is_zero() && zero_init != false) { const auto zero_value = zero_initializer(*object_type, code.source_location(), ns); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 1745a8e445e..3bde290706b 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -80,7 +80,7 @@ void goto_symext::symex_goto(statet &state) } new_guard = renamed_guard.get(); - if(new_guard.is_false()) + if(new_guard == false) { target.location(state.guard.as_expr(), state.source); @@ -113,7 +113,7 @@ void goto_symext::symex_goto(statet &state) // while(cond); (instruction.incoming_edges.size() == 1 && *instruction.incoming_edges.begin() == goto_target && - goto_target->is_goto() && new_guard.is_true()))) + goto_target->is_goto() && new_guard == true))) { // generate assume(false) or a suitable negation if this // instruction is a conditional goto @@ -152,7 +152,7 @@ void goto_symext::symex_goto(statet &state) return; } - if(new_guard.is_true()) + if(new_guard == true) { // we continue executing the loop if(check_break(loop_id, unwind)) @@ -166,7 +166,7 @@ void goto_symext::symex_goto(statet &state) // No point executing both branches of an unconditional goto. if( - new_guard.is_true() && // We have an unconditional goto, AND + new_guard == true && // We have an unconditional goto, AND // either there are no reachable blocks between us and the target in the // surrounding scope (because state.guard == true implies there is no path // around this GOTO instruction) @@ -193,7 +193,7 @@ void goto_symext::symex_goto(statet &state) state_pc++; // skip dead instructions - if(new_guard.is_true()) + if(new_guard == true) while(state_pc!=goto_target && !state_pc->is_target()) ++state_pc; @@ -280,7 +280,7 @@ void goto_symext::symex_goto(statet &state) // On an unconditional GOTO we don't need our state, as it will be overwritten // by merge_goto. Therefore we move it onto goto_state_list instead of copying // as usual. - if(new_guard.is_true()) + if(new_guard == true) { // The move here only moves goto_statet, the base class of goto_symex_statet // and not the entire thing. @@ -410,7 +410,7 @@ void goto_symext::symex_unreachable_goto(statet &state) goto_state_list.emplace_back(state.source, std::move(new_state)); }; - if(instruction.condition().is_true()) + if(instruction.condition() == true) { if(instruction.is_backwards_goto()) { diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 77e8884158c..4fe53bc7c61 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -186,7 +186,7 @@ void goto_symext::vcc( state.total_vccs++; path_segment_vccs++; - if(condition.is_true()) + if(condition == true) return; const exprt guarded_condition = state.guard.guard_expr(condition); @@ -218,10 +218,10 @@ void goto_symext::symex_assume(statet &state, const exprt &cond) void goto_symext::symex_assume_l2(statet &state, const exprt &cond) { - if(cond.is_true()) + if(cond == true) return; - if(cond.is_false()) + if(cond == false) state.reachable = false; // we are willing to re-write some quantified expressions @@ -856,11 +856,11 @@ void goto_symext::try_filter_value_sets( do_simplify(modified_condition, state.value_set); - if(jump_taken_value_set && modified_condition.is_false()) + if(jump_taken_value_set && modified_condition == false) { erase_from_jump_taken_value_set.insert(value_set_element); } - else if(jump_not_taken_value_set && modified_condition.is_true()) + else if(jump_not_taken_value_set && modified_condition == true) { erase_from_jump_not_taken_value_set.insert(value_set_element); } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 65fc1a8f4d4..8bb99bb42c9 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -551,7 +551,7 @@ bool linkingt::adjust_object_type_rec( equal_exprt eq(old_size, new_size); - if(!simplify_expr(eq, ns).is_true()) + if(simplify_expr(eq, ns) != true) { linking_diagnosticst diag{message_handler, ns}; diag.error( diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 80226ed3cba..e7c94c8c80d 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -176,7 +176,7 @@ static std::optional eager_quantifier_instantiation( const exprt where_simplified = simplify_expr(expr.where(), ns); if( - (where_simplified.is_true() || where_simplified.is_false()) && + (where_simplified == true || where_simplified == false) && (var_expr.type().id() == ID_integer || var_expr.type().id() == ID_rational || var_expr.type().id() == ID_real || var_expr.type().id() == ID_bool || diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index cbb5ee60cc6..2af116bb14f 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -21,7 +21,7 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr) PRECONDITION(expr.is_boolean()); if(expr.is_constant()) - return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true(); + return expr == false ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true(); else if(expr.id()==ID_not) return from_expr_rec(to_not_expr(expr).op()).bdd_not(); else if(expr.id()==ID_and || diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp index b2782f7c5fe..9897b26aab2 100644 --- a/src/solvers/prop/cover_goals.cpp +++ b/src/solvers/prop/cover_goals.cpp @@ -28,7 +28,7 @@ void cover_goalst::mark() for(auto &g : goals) if( g.status == goalt::statust::UNKNOWN && - decision_procedure.get(g.condition).is_true()) + decision_procedure.get(g.condition) == true) { g.status=goalt::statust::COVERED; _number_covered++; @@ -47,7 +47,7 @@ void cover_goalst::constraint() // cover at least one unknown goal for(const auto &g : goals) - if(g.status == goalt::statust::UNKNOWN && !g.condition.is_false()) + if(g.status == goalt::statust::UNKNOWN && g.condition != false) disjuncts.push_back(g.condition); // this is 'false' if there are no disjuncts diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index b288d9320cf..a8385c08272 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -78,11 +78,11 @@ std::optional prop_conv_solvert::get_bool(const exprt &expr) const { // trivial cases - if(expr.is_true()) + if(expr == true) { return true; } - else if(expr.is_false()) + else if(expr == false) { return false; } @@ -195,12 +195,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) if(expr.is_constant()) { - if(expr.is_true()) + if(expr == true) return const_literal(true); else { INVARIANT( - expr.is_false(), + expr == false, "constant expression of type bool should be either true or false"); return const_literal(false); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 14291ee5447..e8948f19b09 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -364,9 +364,9 @@ exprt smt2_convt::get(const exprt &expr) const else if(expr.id() == ID_not) { auto op = get(to_not_expr(expr).op()); - if(op.is_true()) + if(op == true) return false_exprt(); - else if(op.is_false()) + else if(op == false) return true_exprt(); } else if( @@ -904,9 +904,9 @@ literalt smt2_convt::convert(const exprt &expr) // Three cases where no new handle is needed. - if(expr.is_true()) + if(expr == true) return const_literal(true); - else if(expr.is_false()) + else if(expr == false) return const_literal(false); else if(expr.id()==ID_literal) return to_literal_expr(expr).get_literal(); @@ -3543,9 +3543,9 @@ void smt2_convt::convert_constant(const constant_exprt &expr) } else if(expr_type.id()==ID_bool) { - if(expr.is_true()) + if(expr == true) out << "true"; - else if(expr.is_false()) + else if(expr == false) out << "false"; else UNEXPECTEDCASE("unknown Boolean constant"); diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp index a4771c632fe..0bdca09dfc4 100644 --- a/src/solvers/smt2/smt2_format.cpp +++ b/src/solvers/smt2/smt2_format.cpp @@ -60,9 +60,9 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) } else if(expr_type.id() == ID_bool) { - if(expr.is_true()) + if(expr == true) out << "true"; - else if(expr.is_false()) + else if(expr == false) out << "false"; else DATA_INVARIANT(false, "unknown Boolean constant"); diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 4622c32eb9e..330e34a26fd 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -307,7 +307,7 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort void visit(const smt_bool_sortt &) override { - result = smt_bool_literal_termt{member_input.is_true()}; + result = smt_bool_literal_termt{member_input == true}; } void visit(const smt_bit_vector_sortt &bit_vector_sort) override diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp index 689818c4aaf..474ef69f6b5 100644 --- a/src/solvers/strings/string_builtin_function.cpp +++ b/src/solvers/strings/string_builtin_function.cpp @@ -31,7 +31,7 @@ std::optional> eval_string( const exprt cond = get_value(ite.cond()); if(!cond.is_constant()) return {}; - return cond.is_true() + return cond == true ? eval_string(to_array_string_expr(ite.true_case()), get_value) : eval_string(to_array_string_expr(ite.false_case()), get_value); } diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index e1980bed5f4..0b7bd009e4b 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -920,7 +920,7 @@ void string_refinementt::add_lemma( simplify(simple_lemma, ns); } - if(simple_lemma.is_true()) + if(simple_lemma == true) { #if 0 log.debug() << "string_refinementt::add_lemma : tautology" << messaget::eom; @@ -1843,9 +1843,9 @@ exprt string_refinementt::get(const exprt &expr) const { const auto &if_expr = expr_dynamic_cast(current.get()); const exprt cond = get(if_expr.cond()); - if(cond.is_true()) + if(cond == true) current = std::cref(if_expr.true_case()); - else if(cond.is_false()) + else if(cond == false) current = std::cref(if_expr.false_case()); else UNREACHABLE; @@ -2021,7 +2021,7 @@ static bool is_valid_string_constraint( const exprt i = pair.second[j]; const equal_exprt equals(rep, i); const exprt result = simplify_expr(equals, ns); - if(result.is_false()) + if(result == false) { stream << "Indices not equal: " << to_string(constraint) << ", str: " << format(pair.first) << messaget::eom; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index fe496a8c657..6e20238e988 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -99,9 +99,9 @@ exprt boolean_negate(const exprt &src) { if(src.id() == ID_not) return to_not_expr(src).op(); - else if(src.is_true()) + else if(src == true) return false_exprt(); - else if(src.is_false()) + else if(src == false) return true_exprt(); else return not_exprt(src); diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 55118640c91..4fb6c62e388 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -175,9 +175,9 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src) if(type == ID_bool) { - if(src.is_true()) + if(src == true) return os << "true"; - else if(src.is_false()) + else if(src == false) return os << "false"; else return os << src.pretty(); diff --git a/src/util/interval.cpp b/src/util/interval.cpp index 48c6d49c609..1316954e92a 100644 --- a/src/util/interval.cpp +++ b/src/util/interval.cpp @@ -998,7 +998,7 @@ constant_exprt constant_interval_exprt::zero(const typet &type) { constant_exprt zero = from_integer(mp_integer(0), type); INVARIANT( - zero.is_zero() || (type.id() == ID_bool && zero.is_false()), + zero.is_zero() || (type.id() == ID_bool && zero == false), "The value created from 0 should be zero or false"); return zero; } @@ -1351,7 +1351,7 @@ bool constant_interval_exprt::equal(const exprt &a, const exprt &b) INVARIANT(!is_extreme(l, r), "We've excluded this before"); - return simplified_expr(equal_exprt(l, r)).is_true(); + return simplified_expr(equal_exprt(l, r)) == true; } // TODO: Signed/unsigned comparisons. @@ -1399,7 +1399,7 @@ bool constant_interval_exprt::less_than(const exprt &a, const exprt &b) !is_extreme(l) && !is_extreme(r), "We have excluded all of these cases in the code above"); - return simplified_expr(binary_relation_exprt(l, ID_lt, r)).is_true(); + return simplified_expr(binary_relation_exprt(l, ID_lt, r)) == true; } bool constant_interval_exprt::greater_than(const exprt &a, const exprt &b) @@ -1628,8 +1628,8 @@ constant_interval_exprt::typecast(const typet &type) const { if(is_boolean() && is_int(type)) { - bool lower = !has_no_lower_bound() && get_lower().is_true(); - bool upper = has_no_upper_bound() || get_upper().is_true(); + bool lower = !has_no_lower_bound() && get_lower() == true; + bool upper = has_no_upper_bound() || get_upper() == true; INVARIANT(!lower || upper, ""); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index b6f19abda7b..9e3912e9f62 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1072,11 +1072,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) expr_type_id==ID_c_enum || expr_type_id==ID_c_bit_field) { - if(operand.is_true()) + if(operand == true) { return from_integer(1, expr_type); } - else if(operand.is_false()) + else if(operand == false) { return from_integer(0, expr_type); } @@ -1086,15 +1086,15 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(expr_type)); if(!c_enum_type.is_incomplete()) // possibly incomplete { - unsigned int_value = operand.is_true() ? 1u : 0u; + unsigned int_value = operand == true ? 1u : 0u; exprt tmp=from_integer(int_value, c_enum_type); tmp.type()=expr_type; // we maintain the tag type return std::move(tmp); } } - else if(expr_type_id==ID_pointer && - operand.is_false() && - config.ansi_c.NULL_is_zero) + else if( + expr_type_id == ID_pointer && operand == false && + config.ansi_c.NULL_is_zero) { return null_pointer_exprt(to_pointer_type(expr_type)); } diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 1a520182176..226ac0b6e86 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -93,11 +93,11 @@ simplify_exprt::simplify_index(const index_exprt &expr) exprt new_index_expr = simplify_index( index_exprt(with_expr.old(), index, new_expr.type())); // recursive call - if(equality_expr.is_true()) + if(equality_expr == true) { return with_expr.new_value(); } - else if(equality_expr.is_false()) + else if(equality_expr == false) { return new_index_expr; } diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index d7a92eb5a9d..bf19e8e06ef 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -56,13 +56,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) bool erase; - if(it->is_true()) + if(*it == true) { erase=true; negate=!negate; } else - erase=it->is_false(); + erase = *it == false; if(erase) { @@ -110,8 +110,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) if(!it->is_boolean()) return unchanged(expr); - bool is_true=it->is_true(); - bool is_false=it->is_false(); + bool is_true = *it == true; + bool is_false = *it == false; if(expr.id()==ID_and && is_false) { @@ -334,11 +334,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr) { return to_not_expr(op).op(); } - else if(op.is_false()) + else if(op == false) { return true_exprt(); } - else if(op.is_true()) + else if(op == true) { return false_exprt(); } @@ -390,7 +390,7 @@ simplify_exprt::simplify_quantifier_expr(const quantifier_exprt &expr) // the following simplification only holds when the domain is non-empty if( - (where.is_false() || where.is_true()) && + (where == false || where == true) && std::all_of( expr.variables().begin(), expr.variables().end(), diff --git a/src/util/simplify_expr_if.cpp b/src/util/simplify_expr_if.cpp index c951603af48..b4e09aa9b18 100644 --- a/src/util/simplify_expr_if.cpp +++ b/src/util/simplify_expr_if.cpp @@ -250,8 +250,7 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr) // 1 ? a : b -> a and 0 ? a : b -> b if(r_cond.expr.is_constant()) { - return changed( - simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue)); + return changed(simplify_rec(r_cond.expr == true ? truevalue : falsevalue)); } if(do_simplify_if) @@ -350,33 +349,33 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr) { // a?b:c <-> (a && b) || (!a && c) - if(truevalue.is_true() && falsevalue.is_false()) + if(truevalue == true && falsevalue == false) { // a?1:0 <-> a return cond; } - else if(truevalue.is_false() && falsevalue.is_true()) + else if(truevalue == false && falsevalue == true) { // a?0:1 <-> !a return changed(simplify_not(not_exprt(cond))); } - else if(falsevalue.is_false()) + else if(falsevalue == false) { // a?b:0 <-> a AND b return changed(simplify_boolean(and_exprt(cond, truevalue))); } - else if(falsevalue.is_true()) + else if(falsevalue == true) { // a?b:1 <-> !a OR b return changed( simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue))); } - else if(truevalue.is_true()) + else if(truevalue == true) { // a?1:b <-> a||(!a && b) <-> a OR b return changed(simplify_boolean(or_exprt(cond, falsevalue))); } - else if(truevalue.is_false()) + else if(truevalue == false) { // a?0:b <-> !a && b return changed(simplify_boolean( diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index aad92696471..17d4fe4a745 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -882,9 +882,9 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) Forall_operands(it, new_expr) { exprt &op=*it; - if(op.is_true() || op.is_false()) + if(op == true || op == false) { - const bool value = op.is_true(); + const bool value = op == true; op = from_integer(value, unsignedbv_typet(1)); no_change = false; } @@ -1650,7 +1650,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant( std::move(offset), ID_lt, std::move(*object_size)}) .expr; if(in_object_bounds.is_constant()) - return tvt{in_object_bounds.is_true()}; + return tvt{in_object_bounds == true}; } return tvt::unknown(); diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 0b83e117456..2d2f27e4167 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -218,11 +218,11 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr) } // condition is a constant? - if(new_if_expr.cond().is_true()) + if(new_if_expr.cond() == true) { return new_if_expr.true_case(); } - else if(new_if_expr.cond().is_false()) + else if(new_if_expr.cond() == false) { return new_if_expr.false_case(); } diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index a7cc221fd3e..a7da245132e 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -228,13 +228,13 @@ exprt conjunction(exprt a, exprt b) PRECONDITION(a.is_boolean() && b.is_boolean()); if(b.is_constant()) { - if(to_constant_expr(b).is_false()) + if(to_constant_expr(b) == false) return false_exprt{}; return a; } if(a.is_constant()) { - if(to_constant_expr(a).is_false()) + if(to_constant_expr(a) == false) return false_exprt{}; return b; } diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp index dc21adae69e..c8e6e7dedea 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp @@ -803,7 +803,7 @@ void ASSUME_TRUE( auto assumption = env.do_assume(expr, ns); REQUIRE(assumption.id() != ID_nil); REQUIRE(assumption.is_boolean()); - REQUIRE(assumption.is_true()); + REQUIRE(assumption == true); } } @@ -817,7 +817,7 @@ void ASSUME_FALSE( auto assumption = env.do_assume(expr, ns); REQUIRE(assumption.id() != ID_nil); REQUIRE(assumption.is_boolean()); - REQUIRE(assumption.is_false()); + REQUIRE(assumption == false); } } diff --git a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp index afd79a0e43c..21794b4522f 100644 --- a/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp +++ b/unit/analyses/variable-sensitivity/value_expression_evaluation/assume_prune.cpp @@ -34,7 +34,7 @@ static void ASSUME_TRUE( REQUIRE(assumption.id() != ID_nil); REQUIRE(assumption.is_boolean()); - REQUIRE(assumption.is_true()); + REQUIRE(assumption == true); } static void EXPECT_RESULT( diff --git a/unit/goto-symex/shadow_memory_util.cpp b/unit/goto-symex/shadow_memory_util.cpp index 8e9a8208967..1d315aa5d5b 100644 --- a/unit/goto-symex/shadow_memory_util.cpp +++ b/unit/goto-symex/shadow_memory_util.cpp @@ -264,7 +264,7 @@ exprt simplify_bit_or_exprt(const exprt &expr) for(const auto &operand : or_expr->operands()) { const exprt reduced = simplify_bit_or_exprt(operand); - res |= reduced.is_true(); + res |= reduced == true; } return from_integer(res, bool_typet{}); } diff --git a/unit/util/interval/get_extreme.cpp b/unit/util/interval/get_extreme.cpp index 63c15d3f5d0..58d6249859d 100644 --- a/unit/util/interval/get_extreme.cpp +++ b/unit/util/interval/get_extreme.cpp @@ -41,7 +41,7 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") THEN("Require it is TRUE") { - REQUIRE(op1.is_true()); + REQUIRE(op1 == true); REQUIRE(interval_eval); } } @@ -55,7 +55,7 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") THEN("Require it is FALSE") { - REQUIRE(op1.is_false()); + REQUIRE(op1 == false); REQUIRE_FALSE(interval_eval); } } @@ -70,7 +70,7 @@ SCENARIO("get extreme exprt value", "[core][analyses][interval][get_extreme]") THEN("Require it is TRUE") { - REQUIRE(op1.is_true()); + REQUIRE(op1 == true); REQUIRE(interval_eval); REQUIRE(constant_interval_exprt::equal(CEV(1), CEV(1))); } diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 4ba152fa694..40f2bb25675 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -247,7 +247,7 @@ TEST_CASE("Simplify pointer_object equality", "[core][util]") exprt simp = simplify_expr(equal_exprt{p_o_void, p_o_int}, ns); - REQUIRE(simp.is_true()); + REQUIRE(simp == true); } TEST_CASE("Simplify cast from bool", "[core][util]") From 33f157206faa6e25a9062a6a473e5fd7ac596398 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 Jul 2025 20:18:47 +0000 Subject: [PATCH 4/5] Use operator==(exprt, int) instead of is_one Avoids use the newly deprecated exprt method. --- .../variable-sensitivity/interval_abstract_value.cpp | 5 +++-- .../variable-sensitivity/value_set_abstract_object.cpp | 2 +- src/ansi-c/goto-conversion/builtin_functions.cpp | 2 +- src/ansi-c/parser.y | 4 +++- src/util/interval.cpp | 4 ++-- src/util/simplify_expr.cpp | 6 +++--- src/util/simplify_expr_floatbv.cpp | 5 +++-- src/util/simplify_expr_int.cpp | 9 ++++----- 8 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 94e4218442b..8561a51928d 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -242,9 +242,10 @@ bool new_interval_is_top(const constant_interval_exprt &e) if(e.get_lower() == false && e.get_upper() == true) return true; if( - e.type().id() == ID_c_bool && e.get_lower().is_zero() && - e.get_upper().is_one()) + e.type().id() == ID_c_bool && e.get_lower().is_zero() && e.get_upper() == 1) + { return true; + } return false; } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 51009dbb849..6118e81b1ab 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -459,7 +459,7 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set) }, [](const abstract_value_objectt &value) { auto c = value.to_constant(); - return c.is_one() || (c.id() == ID_max_value); + return c == 1 || (c.id() == ID_max_value); }); } diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index c6aadc337bd..951a9dbb453 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -618,7 +618,7 @@ static exprt make_va_list(const exprt &expr, const namespacet &ns) } while(result.type().id() == ID_array && - to_array_type(result.type()).size().is_one()) + to_array_type(result.type()).size() == 1) { result = index_exprt{result, from_integer(0, c_index_type())}; } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index ac07f8cf029..e0a4ed1198e 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -1606,8 +1606,10 @@ pragma_packed: { init($$); if(!PARSER.pragma_pack.empty() && - PARSER.pragma_pack.back().is_one()) + PARSER.pragma_pack.back() == 1) + { set($$, ID_packed); + } } ; diff --git a/src/util/interval.cpp b/src/util/interval.cpp index 1316954e92a..874db6e2d55 100644 --- a/src/util/interval.cpp +++ b/src/util/interval.cpp @@ -689,7 +689,7 @@ exprt constant_interval_exprt::generate_division_expression( PRECONDITION(!is_zero(rhs)); - if(rhs.is_one()) + if(rhs == 1) { return lhs; } @@ -744,7 +744,7 @@ exprt constant_interval_exprt::generate_modulo_expression( PRECONDITION(!is_zero(rhs)); - if(rhs.is_one()) + if(rhs == 1) { return lhs; } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 9e3912e9f62..3d97676548d 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2556,7 +2556,7 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr) // One is neutral element for multiplication if( can_cast_expr(expr) && - (expr.op0().is_one() || expr.op1().is_one())) + (expr.op0() == 1 || expr.op1() == 1)) { return false_exprt{}; } @@ -2751,10 +2751,10 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) // One is neutral element for multiplication if( expr.id() == ID_overflow_result_mult && - (expr.op0().is_one() || expr.op1().is_one())) + (expr.op0() == 1 || expr.op1() == 1)) { return struct_exprt{ - {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}}, + {expr.op0() == 1 ? expr.op1() : expr.op0(), false_exprt{}}, expr.type()}; } diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index 61ba1246560..2b35d2eb088 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -347,8 +347,9 @@ simplify_exprt::simplify_floatbv_op(const ieee_float_op_exprt &expr) } // division by one? Exact for all rounding modes. - if(expr.id()==ID_floatbv_div && - op1.is_constant() && op1.is_one()) + if( + expr.id() == ID_floatbv_div && op1.is_constant() && + ieee_float_valuet{to_constant_expr(op1)} == 1) { return op0; } diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 17d4fe4a745..5a0d211379a 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -253,7 +253,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr) else { // if the constant is a one and there are other factors - if(constant_found && constant->is_one()) + if(constant_found && *constant == 1) { // just delete it new_operands.erase(constant); @@ -346,8 +346,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_div(const div_exprt &expr) else if(expr_type.id()==ID_fixedbv) { // division by one? - if(expr.op1().is_constant() && - expr.op1().is_one()) + if(expr.op1().is_constant() && expr.op1() == 1) { return expr.op0(); } @@ -678,7 +677,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) if(op.id() == ID_typecast && to_typecast_expr(op).op().is_boolean()) { } - else if(op.is_zero() || op.is_one()) + else if(op.is_zero() || op == 1) { } else @@ -707,7 +706,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) *it = to_typecast_expr(*it).op(); else if(it->is_zero()) *it=false_exprt(); - else if(it->is_one()) + else if(*it == 1) *it=true_exprt(); } From 98ed937d29c90270edc161389a9f783c1fcef1d0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 6 Jul 2025 20:38:57 +0000 Subject: [PATCH 5/5] Use operator==(exprt, int) instead of is_zero Avoids use the newly deprecated exprt method. --- jbmc/src/java_bytecode/expr2java.cpp | 4 +-- src/analyses/local_bitvector_analysis.cpp | 2 +- src/analyses/local_may_alias.cpp | 2 +- .../interval_abstract_value.cpp | 3 +- .../value_set_abstract_object.cpp | 2 +- src/ansi-c/c_typecast.cpp | 9 +++--- src/ansi-c/c_typecheck_base.cpp | 2 +- src/ansi-c/c_typecheck_expr.cpp | 6 ++-- src/ansi-c/c_typecheck_initializer.cpp | 10 +++---- src/ansi-c/expr2c.cpp | 4 +-- src/ansi-c/goto-conversion/goto_check_c.cpp | 2 +- src/ansi-c/parser.y | 2 +- src/ansi-c/printf_formatter.cpp | 2 +- src/cpp/cpp_typecheck_conversions.cpp | 5 ++-- src/cpp/cpp_typecheck_method_bodies.cpp | 2 +- src/cprover/c_safety_checks.cpp | 4 +-- src/cprover/simplify_state_expr.cpp | 2 +- src/goto-instrument/dump_c.cpp | 4 +-- src/goto-programs/pointer_arithmetic.cpp | 2 +- .../remove_const_function_pointers.cpp | 2 +- src/goto-programs/rewrite_union.cpp | 2 +- src/goto-programs/string_abstraction.cpp | 4 +-- src/goto-symex/shadow_memory.cpp | 2 +- src/goto-symex/shadow_memory_util.cpp | 2 +- src/goto-symex/symex_assign.cpp | 2 +- src/goto-symex/symex_builtin_functions.cpp | 6 ++-- src/goto-symex/symex_clean_expr.cpp | 2 +- src/goto-symex/symex_dereference.cpp | 2 +- src/linking/linking.cpp | 10 +++---- src/pointer-analysis/value_set.cpp | 4 +-- .../value_set_dereference.cpp | 6 ++-- src/pointer-analysis/value_set_fi.cpp | 2 +- src/solvers/flattening/pointer_logic.cpp | 2 +- src/solvers/smt2/smt2_conv.cpp | 2 +- .../string_format_builtin_function.cpp | 2 +- src/util/expr_initializer.cpp | 10 +++---- src/util/interval.cpp | 6 ++-- src/util/pointer_offset_size.cpp | 4 +-- src/util/pointer_offset_sum.cpp | 4 +-- src/util/simplify_expr.cpp | 20 ++++++------- src/util/simplify_expr_int.cpp | 30 +++++++++---------- src/util/simplify_expr_pointer.cpp | 10 +++---- src/util/simplify_expr_struct.cpp | 2 +- unit/util/expr.cpp | 4 +-- 44 files changed, 101 insertions(+), 110 deletions(-) diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index 41e40925f4e..84be33e1cfd 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -172,7 +172,7 @@ std::string expr2javat::convert_constant( { if(src.type().id()==ID_c_bool) { - if(!src.is_zero()) + if(src != 0) return "true"; else return "false"; @@ -187,7 +187,7 @@ std::string expr2javat::convert_constant( else if(src.type().id()==ID_pointer) { // Java writes 'null' for the null reference - if(src.is_zero()) + if(src == 0) return "null"; } else if(src.type()==java_char_type()) diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp index 59d0e110f23..74f4137cbf0 100644 --- a/src/analyses/local_bitvector_analysis.cpp +++ b/src/analyses/local_bitvector_analysis.cpp @@ -115,7 +115,7 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec( { if(rhs.is_constant()) { - if(rhs.is_zero()) + if(rhs == 0) return flagst::mk_null(); else return flagst::mk_integer_address(); diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index d55b5d57293..fe45d512c0c 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -171,7 +171,7 @@ void local_may_aliast::get_rec( { if(rhs.is_constant()) { - if(rhs.is_zero()) + if(rhs == 0) dest.insert(objects.number(exprt(ID_null_object))); else dest.insert(objects.number(exprt(ID_integer_address_object))); diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 8561a51928d..f939bbfea3e 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -241,8 +241,7 @@ bool new_interval_is_top(const constant_interval_exprt &e) if(e.get_lower() == false && e.get_upper() == true) return true; - if( - e.type().id() == ID_c_bool && e.get_lower().is_zero() && e.get_upper() == 1) + if(e.type().id() == ID_c_bool && e.get_lower() == 0 && e.get_upper() == 1) { return true; } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 6118e81b1ab..070865fccea 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -455,7 +455,7 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set) set, [](const abstract_value_objectt &value) { auto c = value.to_constant(); - return c.is_zero() || (c.id() == ID_min_value); + return c == 0 || (c.id() == ID_min_value); }, [](const abstract_value_objectt &value) { auto c = value.to_constant(); diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 873e857af8f..93f7fe66ee2 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -565,11 +565,10 @@ void c_typecastt::implicit_typecast_followed( { // special case: 0 == NULL - if(simplify_expr(expr, ns).is_zero() && ( - src_type.id()==ID_unsignedbv || - src_type.id()==ID_signedbv || - src_type.id()==ID_natural || - src_type.id()==ID_integer)) + if( + simplify_expr(expr, ns) == 0 && + (src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv || + src_type.id() == ID_natural || src_type.id() == ID_integer)) { expr = null_pointer_exprt{to_pointer_type(orig_dest_type)}; return; // ok diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index f11e08f7e14..62ea56d162b 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -312,7 +312,7 @@ static bool is_instantiation_of_flexible_array( return old_array_type.element_type() == new_array_type.element_type() && old_array_type.get_bool(ID_C_flexible_array_member) && new_array_type.get_bool(ID_C_flexible_array_member) && - (old_array_type.size().is_nil() || old_array_type.size().is_zero()); + (old_array_type.size().is_nil() || old_array_type.size() == 0); } void c_typecheck_baset::typecheck_redefinition_non_type( diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index f381a2ccc12..50f72427c88 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1457,15 +1457,13 @@ void c_typecheck_baset::typecheck_expr_rel( else { // pointer and zero - if(type0.id()==ID_pointer && - simplify_expr(op1, *this).is_zero()) + if(type0.id() == ID_pointer && simplify_expr(op1, *this) == 0) { op1 = null_pointer_exprt{to_pointer_type(type0)}; return; } - if(type1.id()==ID_pointer && - simplify_expr(op0, *this).is_zero()) + if(type1.id() == ID_pointer && simplify_expr(op0, *this) == 0) { op0 = null_pointer_exprt{to_pointer_type(type1)}; return; diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index e17d59966c7..a0091286f36 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -405,7 +405,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( if(index>=dest->operands().size()) { if( - type.id() == ID_array && (to_array_type(type).size().is_zero() || + type.id() == ID_array && (to_array_type(type).size() == 0 || to_array_type(type).size().is_nil())) { const typet &element_type = to_array_type(type).element_type(); @@ -673,10 +673,10 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer( // in case of a variable-length array consume all remaining // initializer elements - if(vla_permitted && - dest_type.id()==ID_array && - (to_array_type(dest_type).size().is_zero() || - to_array_type(dest_type).size().is_nil())) + if( + vla_permitted && dest_type.id() == ID_array && + (to_array_type(dest_type).size() == 0 || + to_array_type(dest_type).size().is_nil())) { value.id(ID_initializer_list); value.operands().clear(); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 58260d26282..36cbe37352d 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1280,7 +1280,7 @@ std::string expr2ct::convert_complex( unsigned precedence) { if( - src.operands().size() == 2 && to_binary_expr(src).op0().is_zero() && + src.operands().size() == 2 && to_binary_expr(src).op0() == 0 && to_binary_expr(src).op1().is_constant()) { // This is believed to be gcc only; check if this is sensible @@ -3779,7 +3779,7 @@ std::string expr2ct::convert_with_precedence( if(object.id() == ID_label) return "&&" + object.get_string(ID_identifier); - else if(object.id() == ID_index && to_index_expr(object).index().is_zero()) + else if(object.id() == ID_index && to_index_expr(object).index() == 0) return convert(to_index_expr(object).array()); else if(to_pointer_type(src.type()).base_type().id() == ID_code) return convert_unary(to_unary_expr(src), "", precedence = 15); diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 8db7d255030..68c04604a94 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/src/ansi-c/goto-conversion/goto_check_c.cpp @@ -1695,7 +1695,7 @@ void goto_check_ct::bounds_check_index( } else if( expr.array().id() == ID_member && - (size.is_zero() || array_type.get_bool(ID_C_flexible_array_member))) + (size == 0 || array_type.get_bool(ID_C_flexible_array_member))) { // a variable sized struct member // diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index e0a4ed1198e..eaa29014451 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -1812,7 +1812,7 @@ member_declaring_list: if(parser_stack($2).id() != ID_struct && parser_stack($2).id() != ID_union && !PARSER.pragma_pack.empty() && - !PARSER.pragma_pack.back().is_zero()) + PARSER.pragma_pack.back() != 0) { // communicate #pragma pack(n) alignment constraints by // by both setting packing AND alignment for individual struct/union diff --git a/src/ansi-c/printf_formatter.cpp b/src/ansi-c/printf_formatter.cpp index 7ad8c06667c..35071951c3b 100644 --- a/src/ansi-c/printf_formatter.cpp +++ b/src/ansi-c/printf_formatter.cpp @@ -215,7 +215,7 @@ void printf_formattert::process_format(std::ostream &out) expr_try_dynamic_cast(address_of->object())) { if( - index_expr->index().is_zero() && + index_expr->index() == 0 && index_expr->array().id() == ID_string_constant) { out << format_constant(index_expr->array()); diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp index b7df8895878..440f501f847 100644 --- a/src/cpp/cpp_typecheck_conversions.cpp +++ b/src/cpp/cpp_typecheck_conversions.cpp @@ -465,8 +465,7 @@ bool cpp_typecheckt::standard_conversion_pointer( return false; // integer 0 to NULL pointer conversion? - if(simplify_expr(expr, *this).is_zero() && - expr.type().id()!=ID_pointer) + if(simplify_expr(expr, *this) == 0 && expr.type().id() != ID_pointer) { new_expr=expr; new_expr.set(ID_value, ID_NULL); @@ -1857,7 +1856,7 @@ bool cpp_typecheckt::reinterpret_typecast( type.id() == ID_pointer && !is_reference(type)) { // integer to pointer - if(simplify_expr(e, *this).is_zero()) + if(simplify_expr(e, *this) == 0) { // NULL new_expr=e; diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp index e8389d721be..60fd063850f 100644 --- a/src/cpp/cpp_typecheck_method_bodies.cpp +++ b/src/cpp/cpp_typecheck_method_bodies.cpp @@ -41,7 +41,7 @@ void cpp_typecheckt::typecheck_method_bodies() std::cout << " is_not_nil: " << body.is_not_nil() << '\n'; std::cout << " !is_zero: " << (!body.is_zero()) << '\n'; #endif - if(body.is_not_nil() && !body.is_zero()) + if(body.is_not_nil() && body != 0) convert_function(method_symbol); } diff --git a/src/cprover/c_safety_checks.cpp b/src/cprover/c_safety_checks.cpp index 7288d7fa594..98a4f67611a 100644 --- a/src/cprover/c_safety_checks.cpp +++ b/src/cprover/c_safety_checks.cpp @@ -165,7 +165,7 @@ void c_safety_checks_rec( const auto &div_expr = to_div_expr(expr); if( div_expr.divisor().is_constant() && - !to_constant_expr(div_expr.divisor()).is_zero()) + to_constant_expr(div_expr.divisor()) != 0) { } else @@ -186,7 +186,7 @@ void c_safety_checks_rec( const auto &mod_expr = to_mod_expr(expr); if( mod_expr.divisor().is_constant() && - !to_constant_expr(mod_expr.divisor()).is_zero()) + to_constant_expr(mod_expr.divisor()) != 0) { } else diff --git a/src/cprover/simplify_state_expr.cpp b/src/cprover/simplify_state_expr.cpp index 1d3770ba68c..0074677edfb 100644 --- a/src/cprover/simplify_state_expr.cpp +++ b/src/cprover/simplify_state_expr.cpp @@ -690,7 +690,7 @@ exprt simplify_is_cstring_expr( // maybe the same // Are we writing zero? - if(update_state_expr.new_value().is_zero()) + if(update_state_expr.new_value() == 0) { // cstring(s[p:=0], q) --> if p alias q then true else cstring(s, q) auto same_object = ::same_object(pointer, update_state_expr.address()); diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 6b2ee20f07d..f74233caea8 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -1499,7 +1499,7 @@ void dump_ct::cleanup_expr(exprt &expr) { const byte_update_exprt &bu = to_byte_update_expr(expr); - if(bu.op().id() == ID_union && bu.offset().is_zero()) + if(bu.op().id() == ID_union && bu.offset() == 0) { const union_exprt &union_expr = to_union_expr(bu.op()); const union_typet &union_type = @@ -1537,7 +1537,7 @@ void dump_ct::cleanup_expr(exprt &expr) to_side_effect_expr(bu.op()).get_statement() == ID_nondet && (bu.op().type().id() == ID_union || bu.op().type().id() == ID_union_tag) && - bu.offset().is_zero()) + bu.offset() == 0) { const union_typet &union_type = bu.op().type().id() == ID_union_tag diff --git a/src/goto-programs/pointer_arithmetic.cpp b/src/goto-programs/pointer_arithmetic.cpp index 7c52e30fd85..28c7b77c187 100644 --- a/src/goto-programs/pointer_arithmetic.cpp +++ b/src/goto-programs/pointer_arithmetic.cpp @@ -46,7 +46,7 @@ void pointer_arithmetict::read(const exprt &src) { const index_exprt &index_expr = to_index_expr(address_of_src.op()); - if(index_expr.index().is_zero()) + if(index_expr.index() == 0) make_pointer(address_of_src); else { diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp index 043a3107184..349855e122c 100644 --- a/src/goto-programs/remove_const_function_pointers.cpp +++ b/src/goto-programs/remove_const_function_pointers.cpp @@ -170,7 +170,7 @@ bool remove_const_function_pointerst::try_resolve_function_call( } else if(simplified_expr.is_constant()) { - if(simplified_expr.is_zero()) + if(simplified_expr == 0) { // We have the null pointer - no need to throw everything away // but we don't add any functions either diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp index 71b37ed0c54..b9bb447bd9d 100644 --- a/src/goto-programs/rewrite_union.cpp +++ b/src/goto-programs/rewrite_union.cpp @@ -146,7 +146,7 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns) for(const auto &comp : union_type.components()) { - if(be.offset().is_zero() && be.type() == comp.type()) + if(be.offset() == 0 && be.type() == comp.type()) { expr = member_exprt{be.op(), comp.get_name(), be.type()}; return false; diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5a00c5a7efb..1c943021c11 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -910,7 +910,7 @@ bool string_abstractiont::build_array(const array_exprt &object, exprt::operandst::const_iterator it=object.operands().begin(); for(mp_integer i = 0; i < *size; ++i, ++it) - if(it->is_zero()) + if(*it == 0) return build_symbol_constant(i, *size, dest); return true; @@ -1194,7 +1194,7 @@ goto_programt::targett string_abstractiont::abstract_char_assign( rhsp = &(to_typecast_expr(*rhsp).op()); // we only care if the constant zero is assigned - if(!rhsp->is_zero()) + if(*rhsp != 0) return target; // index into a character array diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index fe7b2005d53..5df8b64aee4 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -39,7 +39,7 @@ void shadow_memoryt::initialize_shadow_memory( if( field_pair.second.id() == ID_typecast && - to_typecast_expr(field_pair.second).op().is_zero()) + to_typecast_expr(field_pair.second).op() == 0) { const auto zero_value = zero_initializer(type, expr.source_location(), ns); diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index b0459f20a06..4bd18bf3046 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -691,7 +691,7 @@ static void clean_string_constant(exprt &expr) { const auto *index_expr = expr_try_dynamic_cast(expr); if( - index_expr && index_expr->index().is_zero() && + index_expr && index_expr->index() == 0 && can_cast_expr(index_expr->array())) { expr = index_expr->array(); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index c42d871fd2d..15fd2358236 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -46,7 +46,7 @@ static bool is_string_constant_initialization(const exprt &rhs) const auto &index = expr_try_dynamic_cast(address_of->object())) { - if(index->array().id() == ID_string_constant && index->index().is_zero()) + if(index->array().id() == ID_string_constant && index->index() == 0) { return true; } diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 987cad6b90e..0ffc7b606f6 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -173,7 +173,7 @@ void goto_symext::symex_allocate( INVARIANT( zero_init.is_constant(), "allocate expects constant as second argument"); - if(!zero_init.is_zero() && zero_init != false) + if(zero_init != 0 && zero_init != false) { const auto zero_value = zero_initializer(*object_type, code.source_location(), ns); @@ -318,7 +318,7 @@ static irep_idt get_string_argument_rec(const exprt &src) if( index_expr.array().id() == ID_string_constant && - index_expr.index().is_zero()) + index_expr.index() == 0) { const exprt &fmt_str = index_expr.array(); return to_string_constant(fmt_str).value(); @@ -373,7 +373,7 @@ static std::optional get_va_args(const exprt::operandst &operands) return {}; const index_exprt &index_expr = to_index_expr(object); - if(!index_expr.index().is_zero()) + if(index_expr.index() != 0) return {}; else return index_expr.array(); diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 7926a8a86be..f065dbda360 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -79,7 +79,7 @@ static void process_array_expr(exprt &expr, const namespacet &ns) if(expr.type().id() == ID_empty) return; - if(!ode.offset().is_zero()) + if(ode.offset() != 0) { if(expr.type().id() != ID_array) { diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp index 835cb2e763e..6948502b67e 100644 --- a/src/goto-symex/symex_dereference.cpp +++ b/src/goto-symex/symex_dereference.cpp @@ -363,7 +363,7 @@ void goto_symext::dereference_rec( } else if( expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member && - to_array_type(to_index_expr(expr).array().type()).size().is_zero()) + to_array_type(to_index_expr(expr).array().type()).size() == 0) { // This is an expression of the form x.a[i], // where a is a zero-sized array. This gets diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 8bb99bb42c9..58629491f1e 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -523,15 +523,13 @@ bool linkingt::adjust_object_type_rec( const exprt &old_size=to_array_type(t1).size(); const exprt &new_size=to_array_type(t2).size(); - if((old_size.is_nil() && new_size.is_not_nil()) || - (old_size.is_zero() && new_size.is_not_nil()) || - info.old_symbol.is_weak) + if( + (old_size.is_nil() && new_size.is_not_nil()) || + (old_size == 0 && new_size.is_not_nil()) || info.old_symbol.is_weak) { info.set_to_new=true; // store new type } - else if(new_size.is_nil() || - new_size.is_zero() || - info.new_symbol.is_weak) + else if(new_size.is_nil() || new_size == 0 || info.new_symbol.is_weak) { // ok, we will use the old type } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 626777ec8bf..d35a6416269 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -658,7 +658,7 @@ void value_sett::get_value_set_rec( { // integer-to-something - if(op.is_zero()) + if(op == 0) { insert( dest, @@ -1414,7 +1414,7 @@ void value_sett::get_reference_set_rec( offsett o = a_it->second; - if(!index.is_zero() && o.has_value()) + if(index != 0 && o.has_value()) { auto size = pointer_offset_size(array_type.element_type(), ns); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index dd17eced5e6..f9a99530a6c 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -487,7 +487,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( if(root_object.id() == ID_null_object) { - if(!o.offset().is_zero()) + if(o.offset() != 0) return {}; valuet result; @@ -573,7 +573,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // something generic -- really has to be a symbol address_of_exprt object_pointer(object); - if(o.offset().is_zero()) + if(o.offset() == 0) { result.pointer_guard = equal_exprt( typecast_exprt::conditional_cast(pointer_expr, object_pointer.type()), @@ -589,7 +589,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( if( dereference_type_compare(object_type, dereference_type, ns) && - o.offset().is_zero()) + o.offset() == 0) { // The simplest case: types match, and offset is zero! // This is great, we are almost done. diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index bf634d07264..f9704a4f36b 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -923,7 +923,7 @@ void value_set_fit::get_reference_set_sharing_rec( offsett o = object_entry.second; const auto i = numeric_cast(offset); - if(offset.is_zero()) + if(offset == 0) { } else if(i.has_value() && offset_is_zero(o)) diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index c5b866d6104..dcd3ae01b40 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -129,7 +129,7 @@ exprt pointer_logict::pointer_expr( const byte_extract_exprt &be = to_byte_extract_expr(deep_object); const address_of_exprt base(be.op()); - if(be.offset().is_zero()) + if(be.offset() == 0) return typecast_exprt::conditional_cast(base, type); const auto object_size = pointer_offset_size(be.op().type(), ns); diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e8948f19b09..49e2197d9e7 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -816,7 +816,7 @@ void smt2_convt::convert_address_of_rec( const exprt &array = index_expr.array(); const exprt &index = index_expr.index(); - if(index.is_zero()) + if(index == 0) { if(array.type().id()==ID_pointer) convert_expr(array); diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index 20ce1f8ab2a..14e32a86e8c 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -597,7 +597,7 @@ string_constraintst string_format_builtin_functiont::constraints( auto result_constraint_pair = add_axioms_for_format( generator, result, format_string.value(), inputs, message_handler); INVARIANT( - simplify_expr(result_constraint_pair.first, generator.ns).is_zero(), + simplify_expr(result_constraint_pair.first, generator.ns) == 0, "add_axioms_for_format should return 0, meaning that formatting was" "successful"); result_constraint_pair.second.existential.push_back( diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 3525b2804e1..4b99415f535 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -66,7 +66,7 @@ std::optional expr_initializert::expr_initializer_rec( exprt result; if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else if(init_expr.is_zero()) + else if(init_expr == 0) result = from_integer(0, type); else result = duplicate_per_byte(init_expr, type, ns); @@ -80,7 +80,7 @@ std::optional expr_initializert::expr_initializer_rec( exprt result; if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else if(init_expr.is_zero()) + else if(init_expr == 0) result = constant_exprt(ID_0, type); else result = duplicate_per_byte(init_expr, type, ns); @@ -94,7 +94,7 @@ std::optional expr_initializert::expr_initializer_rec( exprt result; if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else if(init_expr.is_zero()) + else if(init_expr == 0) { const std::size_t width = to_bitvector_type(type).get_width(); std::string value(width, '0'); @@ -112,7 +112,7 @@ std::optional expr_initializert::expr_initializer_rec( exprt result; if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else if(init_expr.is_zero()) + else if(init_expr == 0) { auto sub_zero = expr_initializer_rec( to_complex_type(type).subtype(), source_location, init_expr); @@ -287,7 +287,7 @@ std::optional expr_initializert::expr_initializer_rec( exprt result; if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else if(init_expr.is_zero()) + else if(init_expr == 0) result = constant_exprt(irep_idt(), type); else result = duplicate_per_byte(init_expr, type, ns); diff --git a/src/util/interval.cpp b/src/util/interval.cpp index 874db6e2d55..8236240a1cf 100644 --- a/src/util/interval.cpp +++ b/src/util/interval.cpp @@ -998,7 +998,7 @@ constant_exprt constant_interval_exprt::zero(const typet &type) { constant_exprt zero = from_integer(mp_integer(0), type); INVARIANT( - zero.is_zero() || (type.id() == ID_bool && zero == false), + zero == 0 || (type.id() == ID_bool && zero == false), "The value created from 0 should be zero or false"); return zero; } @@ -1269,7 +1269,7 @@ bool constant_interval_exprt::is_zero(const exprt &expr) INVARIANT(!is_max(expr) && !is_min(expr), "We excluded those cases"); - if(expr.is_zero()) + if(expr == 0) { return true; } @@ -1875,7 +1875,7 @@ bool constant_interval_exprt::contains_zero() const return false; } - if(get_lower().is_zero() || get_upper().is_zero()) + if(get_lower() == 0 || get_upper() == 0) { return true; } diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 9e60faf8047..1a355611c7a 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -737,7 +737,7 @@ std::optional get_subexpression_at_offset( if( expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index && - to_index_expr(*expr_at_offset_C).index().is_zero()) + to_index_expr(*expr_at_offset_C).index() == 0) { return get_subexpression_at_offset( to_index_expr(*expr_at_offset_C).array(), @@ -842,7 +842,7 @@ std::optional get_subexpression_at_offset( if( expr_at_offset_C.has_value() && expr_at_offset_C->id() == ID_index && - to_index_expr(*expr_at_offset_C).index().is_zero()) + to_index_expr(*expr_at_offset_C).index() == 0) { return get_subexpression_at_offset( to_index_expr(*expr_at_offset_C).array(), diff --git a/src/util/pointer_offset_sum.cpp b/src/util/pointer_offset_sum.cpp index dc34d0eb0ce..1dce5f958cc 100644 --- a/src/util/pointer_offset_sum.cpp +++ b/src/util/pointer_offset_sum.cpp @@ -19,9 +19,9 @@ exprt pointer_offset_sum(const exprt &a, const exprt &b) return a; else if(b.id() == ID_unknown) return b; - else if(a.is_zero()) + else if(a == 0) return b; - else if(b.is_zero()) + else if(b == 0) return a; return plus_exprt(a, typecast_exprt::conditional_cast(b, a.type())); diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 3d97676548d..28adf3e27a1 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -858,7 +858,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) if( expr_type.id() == ID_pointer && expr.op().is_constant() && (to_constant_expr(expr.op()).get_value() == ID_NULL || - (expr.op().is_zero() && config.ansi_c.NULL_is_zero))) + (expr.op() == 0 && config.ansi_c.NULL_is_zero))) { exprt tmp = expr.op(); tmp.type()=expr.type(); @@ -904,7 +904,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) if( (op_plus_expr.op0().id() == ID_typecast && - to_typecast_expr(op_plus_expr.op0()).op().is_zero()) || + to_typecast_expr(op_plus_expr.op0()).op() == 0) || (op_plus_expr.op0().is_constant() && to_constant_expr(op_plus_expr.op0()).is_null_pointer())) { @@ -2102,7 +2102,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) // byte update of full object is byte_extract(new value) if( - offset.is_zero() && val_size.has_value() && *val_size > 0 && + offset == 0 && val_size.has_value() && *val_size > 0 && root_size.has_value() && *root_size > 0 && *val_size >= *root_size) { byte_extract_exprt be( @@ -2297,7 +2297,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr) if( expr_at_offset_C.id() == ID_with && - to_with_expr(expr_at_offset_C).where().is_zero()) + to_with_expr(expr_at_offset_C).where() == 0) { tmp.set_op(to_with_expr(expr_at_offset_C).old()); tmp.set_offset(other_factor); @@ -2547,8 +2547,8 @@ simplify_exprt::simplify_overflow_binary(const binary_overflow_exprt &expr) // When one operand is zero, an overflow can only occur for a subtraction from // zero. if( - expr.op1().is_zero() || - (expr.op0().is_zero() && !can_cast_expr(expr))) + expr.op1() == 0 || + (expr.op0() == 0 && !can_cast_expr(expr))) { return false_exprt{}; } @@ -2617,7 +2617,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr) { // zero is a neutral element for all operations supported here - if(expr.op().is_zero()) + if(expr.op() == 0) return false_exprt{}; // catch some cases over mathematical types @@ -2667,7 +2667,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) if(expr.id() == ID_overflow_result_unary_minus) { // zero is a neutral element - if(expr.op0().is_zero()) + if(expr.op0() == 0) return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()}; // catch some cases over mathematical types @@ -2718,7 +2718,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) { // When one operand is zero, an overflow can only occur for a subtraction // from zero. - if(expr.op0().is_zero()) + if(expr.op0() == 0) { if( expr.id() == ID_overflow_result_plus || @@ -2732,7 +2732,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()}; } } - else if(expr.op1().is_zero()) + else if(expr.op1() == 0) { if( expr.id() == ID_overflow_result_plus || diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 5a0d211379a..2484178db30 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -192,8 +192,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr) // if one of the operands is zero the result is zero // note: not true on IEEE floating point arithmetic - if(it->is_zero() && - it->type().id()!=ID_floatbv) + if(*it == 0 && it->type().id() != ID_floatbv) { return from_integer(0, expr.type()); } @@ -540,7 +539,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr) it != new_operands.end(); /* no it++ */) { - if(is_number(it->type()) && it->is_zero()) + if(is_number(it->type()) && *it == 0) { it = new_operands.erase(it); no_change = false; @@ -621,7 +620,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr) if( offset_op0.is_constant() && offset_op1.is_constant() && object_size.has_value() && element_size.has_value() && - element_size->is_constant() && !element_size->is_zero() && + element_size->is_constant() && *element_size != 0 && numeric_cast_v(to_constant_expr(offset_op0)) <= *object_size && numeric_cast_v(to_constant_expr(offset_op1)) <= @@ -649,7 +648,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr) if( element_size.has_value() && element_size->is_constant() && - !element_size->is_zero()) + *element_size != 0) { return changed(simplify_rec(div_exprt{ minus_exprt{offset_op0, offset_op1}, @@ -677,7 +676,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) if(op.id() == ID_typecast && to_typecast_expr(op).op().is_boolean()) { } - else if(op.is_zero() || op == 1) + else if(op == 0 || op == 1) { } else @@ -704,7 +703,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) { if(it->id()==ID_typecast) *it = to_typecast_expr(*it).op(); - else if(it->is_zero()) + else if(*it == 0) *it=false_exprt(); else if(*it == 1) *it=true_exprt(); @@ -776,7 +775,7 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr) for(exprt::operandst::iterator it = new_expr.operands().begin(); it != new_expr.operands().end();) // no it++ { - if(it->is_zero() && new_expr.operands().size() > 1) + if(*it == 0 && new_expr.operands().size() > 1) { it = new_expr.operands().erase(it); no_change = false; @@ -1474,7 +1473,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant( // is and therefore cannot simplify return unchanged(expr); } - equal = tmp0_const.is_zero() && tmp1_const.is_zero(); + equal = tmp0_const == 0 && tmp1_const == 0; } return make_boolean_expr(expr.id() == ID_equal ? equal : !equal); } @@ -1561,7 +1560,7 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1) { // we can't eliminate zeros if( - op0.is_zero() || op1.is_zero() || + op0 == 0 || op1 == 0 || (op0.is_constant() && to_constant_expr(op0).is_null_pointer()) || (op1.is_constant() && to_constant_expr(op1).is_null_pointer())) { @@ -1590,8 +1589,7 @@ static bool eliminate_common_addends(exprt &op0, exprt &op1) } else if(op0==op1) { - if(!op0.is_zero() && - op0.type().id()!=ID_complex) + if(op0 != 0 && op0.type().id() != ID_complex) { // elimination! op0=from_integer(0, op0.type()); @@ -1824,7 +1822,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant( exprt ptr = simplify_object(expr.op0()).expr; // NULL + N == NULL is N == 0 if(ptr.is_constant() && to_constant_expr(ptr).is_null_pointer()) - return make_boolean_expr(offset.is_zero()); + return make_boolean_expr(offset == 0); // &x + N == NULL is false when the offset is in bounds else if(auto address_of = expr_try_dynamic_cast(ptr)) { @@ -1912,7 +1910,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant( // is the constant zero? - if(expr.op1().is_zero()) + if(expr.op1() == 0) { if(expr.id()==ID_ge && expr.op0().type().id()==ID_unsignedbv) @@ -2001,13 +1999,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant( const auto &lhs_typecast_op = to_typecast_expr(expr.op0()).op(); // we re-write (TYPE)boolean == 0 -> !boolean - if(expr.op1().is_zero() && expr.id()==ID_equal) + if(expr.op1() == 0 && expr.id() == ID_equal) { return changed(simplify_not(not_exprt(lhs_typecast_op))); } // we re-write (TYPE)boolean != 0 -> boolean - if(expr.op1().is_zero() && expr.id()==ID_notequal) + if(expr.op1() == 0 && expr.id() == ID_notequal) { return lhs_typecast_op; } diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 2d2f27e4167..d1afed4af5a 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -246,7 +246,7 @@ simplify_exprt::simplify_address_of(const address_of_exprt &expr) { auto index_expr = to_index_expr(new_object.expr); - if(!index_expr.index().is_zero()) + if(index_expr.index() != 0) { // we normalize &a[i] to (&a[0])+i exprt offset = index_expr.op1(); @@ -353,7 +353,7 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr) { if(op.type().id()==ID_pointer) ptr_expr.push_back(op); - else if(!op.is_zero()) + else if(op != 0) { exprt tmp=op; if(tmp.type()!=expr.type()) @@ -424,7 +424,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of( if( tmp0_address_of.object().id() == ID_index && - to_index_expr(tmp0_address_of.object()).index().is_zero()) + to_index_expr(tmp0_address_of.object()).index() == 0) { tmp0_address_of = address_of_exprt(to_index_expr(tmp0_address_of.object()).array()); @@ -438,7 +438,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of( if( tmp1_address_of.object().id() == ID_index && - to_index_expr(tmp1_address_of.object()).index().is_zero()) + to_index_expr(tmp1_address_of.object()).index() == 0) { tmp1 = address_of_exprt(to_index_expr(tmp1_address_of.object()).array()); } @@ -500,7 +500,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object( return unchanged(expr); } } - else if(!op.is_constant() || !op.is_zero()) + else if(!op.is_constant() || op != 0) { return unchanged(expr); } diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 80b1961508c..3993484ad48 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -172,7 +172,7 @@ simplify_exprt::simplify_member(const member_exprt &expr) { // rewrite byte_extract(X, 0).member to X // if the type of X is that of the member - if(byte_extract_expr.offset().is_zero()) + if(byte_extract_expr.offset() == 0) { const union_typet &union_type = op.type().id() == ID_union_tag diff --git a/unit/util/expr.cpp b/unit/util/expr.cpp index 462708fb3b0..0965932dc2e 100644 --- a/unit/util/expr.cpp +++ b/unit/util/expr.cpp @@ -20,7 +20,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]") THEN("is_zero() should be false") { - REQUIRE_FALSE(bitfield3.is_zero()); + REQUIRE_FALSE(bitfield3 == 0); } } GIVEN("An exprt representing a bitfield constant of 0") @@ -30,7 +30,7 @@ SCENARIO("bitfield-expr-is-zero", "[core][util][expr]") THEN("is_zero() should be true") { - REQUIRE(bitfield0.is_zero()); + REQUIRE(bitfield0 == 0); } } }