operator== for exprt and bool, int, nullptr_t

jbmc/src/java_bytecode/expr2java.cpp

@@ -172,22 +172,22 @@ std::string expr2javat::convert_constant(
 {
   if(src.type().id()==ID_c_bool)
   {
-    if(!src.is_zero())
+    if(src != 0)
       return "true";
     else
       return "false";
   }
   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)
   {
     // Java writes 'null' for the null reference
-    if(src.is_zero())
+    if(src == 0)
       return "null";
   }
   else if(src.type()==java_char_type())

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)));
       }
 

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
       {

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

src/analyses/custom_bitvector_analysis.cpp

@@ -530,7 +530,7 @@
 
       const exprt result2 = simplify_expr(eval(guard, cba), ns);
 
-      if(result2.is_false())
+      if(result2 == false)
         make_bottom();
     }
     break;
@@ -814,9 +814,9 @@
       if(use_xml)
       {
         out << "<result status=\"";
-        if(result.is_true())
+        if(result == true)
           out << "SUCCESS";
-        else if(result.is_false())
+        else if(result == false)
           out << "FAILURE";
         else
           out << "UNKNOWN";
@@ -838,9 +838,9 @@
         out << '\n';
       }
 
-      if(result.is_true())
+      if(result == true)
         pass++;
-      else if(result.is_false())
+      else if(result == false)
         fail++;
       else
         unknown++;

src/analyses/goto_rw.cpp

@@ -116,9 +116,9 @@
   const range_spect &range_start,
   const range_spect &size)
 {
-  if(if_expr.cond().is_false())
+  if(if_expr.cond() == false)
     get_objects_rec(mode, if_expr.false_case(), range_start, size);
-  else if(if_expr.cond().is_true())
+  else if(if_expr.cond() == true)
     get_objects_rec(mode, if_expr.true_case(), range_start, size);
   else
   {
@@ -735,9 +735,9 @@
   const range_spect &range_start,
   const range_spect &size)
 {
-  if(if_expr.cond().is_false())
+  if(if_expr.cond() == false)
     get_objects_rec(mode, if_expr.false_case(), range_start, size);
-  else if(if_expr.cond().is_true())
+  else if(if_expr.cond() == true)
     get_objects_rec(mode, if_expr.true_case(), range_start, size);
   else
   {

src/analyses/guard_bdd.cpp

@@ -44,7 +44,7 @@
   }
   else
   {
-    if(expr.is_false())
+    if(expr == false)
     {
       return boolean_negate(as_expr());
     }

src/analyses/guard_expr.cpp

@@ -24,7 +24,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
   }
   else
   {
-    if(expr.is_false())
+    if(expr == false)
     {
       return boolean_negate(as_expr());
     }
@@ -39,9 +39,9 @@ void guard_exprt::add(const exprt &expr)
 {
   PRECONDITION(expr.is_boolean());
 
-  if(is_false() || expr.is_true())
+  if(is_false() || expr == true)
     return;
-  else if(is_true() || expr.is_false())
+  else if(is_true() || expr == false)
   {
     this->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

src/analyses/guard_expr.h

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANALYSES_GUARD_EXPR_H
 #define CPROVER_ANALYSES_GUARD_EXPR_H
 
-#include <util/expr.h>
+#include <util/std_expr.h>
 
 /// 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);

src/analyses/interval_analysis.cpp

@@ -46,7 +46,7 @@
     {
       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 @@
     for(const auto &symbol_expr : symbols)
     {
       exprt tmp=d.make_expression(symbol_expr);
-      if(!tmp.is_true())
+      if(tmp != true)
         assertion.push_back(tmp);
     }
 

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();
     }
   }

src/analyses/invariant_set.cpp

@@ -394,11 +394,11 @@
     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 @@
   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 @@
   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();

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

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)

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)));

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))
     {

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;
 

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);
   }
 

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);
   }
 

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,12 +239,12 @@ 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() &&
-    e.get_upper().is_one())
+  if(e.type().id() == ID_c_bool && e.get_lower() == 0 && e.get_upper() == 1)
+  {
     return true;
+  }
 
   return false;
 }