Merge pull request #8675 from tautschnig/operator-equals

operator== for exprt and bool, int, nullptr_t

Author: tautschnig

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 @@ 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 << "<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 @@ void custom_bitvector_analysist::check(
         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 @@ void rw_range_sett::get_objects_if(
   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 @@ void rw_guarded_range_set_value_sett::get_objects_if(
   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 @@ exprt guard_bddt::guard_expr(exprt expr) const
   }
   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 @@ 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);
     }