Replace uses of exprt::make_not by boolean_negate

exprt::make_not is deprecated, and boolean_negate also performs additional type
checking.

Author: tautschnig

src/analyses/custom_bitvector_analysis.cpp

@@ -11,8 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "custom_bitvector_analysis.h"
 
-#include <util/xml_expr.h>
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
+#include <util/xml_expr.h>
 
 #include <langapi/language_util.h>
 
@@ -527,7 +528,7 @@ void custom_bitvector_domaint::transform(
       // Comparing iterators is safe as the target must be within the same list
       // of instructions because this is a GOTO.
       if(to!=from->get_target())
-        guard.make_not();
+        guard = boolean_negate(guard);
 
       exprt result=eval(guard, cba);
       exprt result2=simplify_expr(result, ns);

src/analyses/flow_insensitive_analysis.cpp

@@ -14,8 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
-#include <util/std_expr.h>
+#include <util/expr_util.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 exprt flow_insensitive_abstract_domain_baset::get_guard(
   locationt from,
@@ -28,11 +29,7 @@ exprt flow_insensitive_abstract_domain_baset::get_guard(
   next++;
 
   if(next==to)
-  {
-    exprt tmp(from->guard);
-    tmp.make_not();
-    return tmp;
-  }
+    return boolean_negate(from->guard);
 
   return from->guard;
 }

src/analyses/goto_check.cpp

@@ -861,11 +861,9 @@ void goto_checkt::nan_check(
   else
     UNREACHABLE;
 
-  isnan.make_not();
-
   add_guarded_claim(
-    isnan,
-    "NaN on "+expr.id_string(),
+    boolean_negate(isnan),
+    "NaN on " + expr.id_string(),
     "NaN",
     expr.find_source_location(),
     expr,

src/analyses/invariant_set.cpp

@@ -13,16 +13,17 @@ Author: Daniel Kroening, [email protected]
 
 #include <iostream>
 
+#include <util/arith_tools.h>
 #include <util/base_exceptions.h>
-#include <util/symbol_table.h>
+#include <util/base_type.h>
+#include <util/c_types.h>
+#include <util/expr_util.h>
 #include <util/namespace.h>
-#include <util/arith_tools.h>
-#include <util/std_expr.h>
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
+#include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
 
-#include <util/c_types.h>
 #include <langapi/language_util.h>
 
 void inv_object_storet::output(std::ostream &out) const
@@ -758,10 +759,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
       nnf(tmp, !negate);
       expr.swap(tmp);
     }
-    else
+    else if(negate)
     {
-      if(negate)
-        expr.make_not();
+      expr = boolean_negate(expr);
     }
   }
   else if(expr.id()==ID_le)
@@ -812,10 +812,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
     if(negate)
       expr.id(ID_equal);
   }
-  else
+  else if(negate)
   {
-    if(negate)
-      expr.make_not();
+    expr = boolean_negate(expr);
   }
 }
 

src/analyses/invariant_set_domain.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "invariant_set_domain.h"
 
+#include <util/expr_util.h>
 #include <util/simplify_expr.h>
 
 void invariant_set_domaint::transform(
@@ -32,7 +33,7 @@ void invariant_set_domaint::transform(
       goto_programt::const_targett next=from_l;
       next++;
       if(next==to_l)
-        tmp.make_not();
+        tmp = boolean_negate(from_l->guard);
 
       simplify(tmp, ns);
       invariant_set.strengthen(tmp);

src/analyses/static_analysis.cpp

@@ -15,8 +15,9 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <memory>
 
-#include <util/std_expr.h>
+#include <util/expr_util.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include "is_threaded.h"
 
@@ -31,11 +32,7 @@ exprt static_analysis_baset::get_guard(
   next++;
 
   if(next==to)
-  {
-    exprt tmp(from->guard);
-    tmp.make_not();
-    return tmp;
-  }
+    return boolean_negate(from->guard);
 
   return from->guard;
 }

src/goto-instrument/branch.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "branch.h"
 
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/prefix.h>
 
 #include "function.h"
@@ -48,7 +49,7 @@ void branch(
          !i_it->guard.is_constant())
       {
         // negate condition
-        i_it->guard.make_not();
+        i_it->guard = boolean_negate(i_it->guard);
 
         goto_programt::targett t1=body.insert_after(i_it);
         t1->make_function_call(

src/goto-instrument/code_contracts.cpp

@@ -13,6 +13,7 @@ Date: February 2016
 
 #include "code_contracts.h"
 
+#include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/replace_symbol.h>
 
@@ -158,7 +159,7 @@ static void check_apply_invariants(
   if(loop_head->is_goto())
     loop_end->guard.make_false();
   else
-    loop_end->guard.make_not();
+    loop_end->guard = boolean_negate(loop_end->guard);
 }
 
 void code_contractst::apply_contract(

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening
 
 #include "cover_instrument.h"
 
+#include <util/expr_util.h>
+
 #include <langapi/language_util.h>
 
 #include <algorithm>
@@ -73,7 +75,7 @@ void collect_mcdc_controlling_rec(
           new_conditions.push_back(conjunction(o));
           result.insert(conjunction(new_conditions));
 
-          o[i].make_not();
+          o[i] = boolean_negate(op);
           new_conditions.back() = conjunction(o);
           result.insert(conjunction(new_conditions));
         }

src/goto-instrument/unwind.cpp

@@ -16,8 +16,10 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
+#include <util/expr_util.h>
 #include <util/std_expr.h>
 #include <util/string_utils.h>
+
 #include <goto-programs/goto_functions.h>
 
 #include "loop_utils.h"
@@ -127,8 +129,7 @@ void goto_unwindt::unwind(
 
     if(!t->guard.is_true()) // cond in backedge
     {
-      exit_cond=t->guard;
-      exit_cond.make_not();
+      exit_cond = boolean_negate(t->guard);
     }
     else if(loop_head->is_goto())
     {

src/goto-programs/goto_convert.cpp

@@ -980,8 +980,7 @@ void goto_convertt::convert_for(
 
   // v: if(!c) goto z;
   v->make_goto(z);
-  v->guard=cond;
-  v->guard.make_not();
+  v->guard = boolean_negate(cond);
   v->source_location=cond.source_location();
 
   // do the w label

src/goto-programs/goto_convert_function_call.cpp

@@ -12,10 +12,11 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert_class.h"
 
 
-#include <util/replace_expr.h>
-#include <util/source_location.h>
 #include <util/cprover_prefix.h>
+#include <util/expr_util.h>
 #include <util/prefix.h>
+#include <util/replace_expr.h>
+#include <util/source_location.h>
 #include <util/std_expr.h>
 
 #include <util/c_types.h>
@@ -135,8 +136,7 @@ void goto_convertt::do_function_call_if(
 
   // v: if(!c) goto y;
   v->make_goto(y);
-  v->guard=function.cond();
-  v->guard.make_not();
+  v->guard = boolean_negate(function.cond());
   v->source_location=function.cond().source_location();
 
   // w: f();

src/goto-programs/string_abstraction.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/pointer_predicates.h>
 #include <util/type_eq.h>
 
@@ -1273,8 +1274,7 @@ goto_programt::targett string_abstractiont::value_assignments_if(
 
   goto_else->function=target->function;
   goto_else->source_location=target->source_location;
-  goto_else->make_goto(else_target, rhs.cond());
-  goto_else->guard.make_not();
+  goto_else->make_goto(else_target, boolean_negate(rhs.cond()));
 
   goto_out->function=target->function;
   goto_out->source_location=target->source_location;

src/goto-symex/slice_by_trace.cpp

@@ -88,14 +88,12 @@ void symex_slice_by_tracet::slice_by_trace(
 
     if(g_copy.id()==ID_symbol || g_copy.id() == ID_not)
     {
-      g_copy.make_not();
-      simplify(g_copy, ns);
+      g_copy = simplify_expr(boolean_negate(g_copy), ns);
       implications.insert(g_copy);
     }
     else if(g_copy.id()==ID_and)
     {
-      exprt copy_last(g_copy.operands().back());
-      copy_last.make_not();
+      exprt copy_last = boolean_negate(g_copy.operands().back());
       simplify(copy_last, ns);
       implications.insert(copy_last);
     }
@@ -408,8 +406,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
 
     if((guard.id()==ID_symbol) || (guard.id() == ID_not))
     {
-      guard.make_not();
-      simplify(guard, ns);
+      guard = simplify_expr(boolean_negate(guard), ns);
 
       if(implications.count(guard)!=0)
       {
@@ -426,8 +423,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
     {
       Forall_operands(git, guard)
       {
-        exprt neg_expr=*git;
-        neg_expr.make_not();
+        exprt neg_expr = boolean_negate(*git);
         simplify(neg_expr, ns);
 
         if(implications.count(neg_expr)!=0)
@@ -466,8 +462,7 @@ void symex_slice_by_tracet::slice_SSA_steps(
         }
         else
         {
-          cond_copy.make_not();
-          simplify(cond_copy, ns);
+          cond_copy = simplify_expr(boolean_negate(cond_copy), ns);
           if(implications.count(cond_copy)!=0)
           {
             sliced_conds++;
@@ -622,8 +617,7 @@ bool symex_slice_by_tracet::implies_false(const exprt e)
       i=imps.begin();
       i!=imps.end(); i++)
   {
-    exprt i_copy(*i);
-    i_copy.make_not();
+    exprt i_copy = boolean_negate(*i);
     simplify(i_copy, ns);
     if(imps.count(i_copy)!=0)
       return true;

src/goto-symex/symex_goto.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <algorithm>
 
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/range.h>
@@ -242,8 +243,7 @@ void goto_symext::symex_goto(statet &state)
     {
       symbol_exprt guard_symbol_expr=
         symbol_exprt(guard_identifier, bool_typet());
-      exprt new_rhs=new_guard;
-      new_rhs.make_not();
+      exprt new_rhs = boolean_negate(new_guard);
 
       ssa_exprt new_lhs(guard_symbol_expr);
       state.rename(new_lhs, ns, goto_symex_statet::L1);
@@ -266,8 +266,7 @@ void goto_symext::symex_goto(statet &state)
         original_source,
         symex_targett::assignment_typet::GUARD);
 
-      guard_expr=guard_symbol_expr;
-      guard_expr.make_not();
+      guard_expr = boolean_negate(guard_symbol_expr);
       state.rename(guard_expr, ns);
     }
 
@@ -276,25 +275,20 @@ void goto_symext::symex_goto(statet &state)
       if(!backward)
         state.guard.add(guard_expr);
       else
-      {
-        guard_expr.make_not();
-        state.guard.add(guard_expr);
-      }
+        state.guard.add(boolean_negate(guard_expr));
     }
     else
     {
       statet::goto_statet &new_state = goto_state_list.back();
       if(!backward)
       {
         new_state.guard.add(guard_expr);
-        guard_expr.make_not();
-        state.guard.add(guard_expr);
+        state.guard.add(boolean_negate(guard_expr));
       }
       else
       {
         state.guard.add(guard_expr);
-        guard_expr.make_not();
-        new_state.guard.add(guard_expr);
+        new_state.guard.add(boolean_negate(guard_expr));
       }
     }
   }