Merge pull request #3783 from tautschnig/deprecation-binary_predicate_exprt

Construct binary_predicate_exprt in a non-deprecated way

Author: tautschnig

src/ansi-c/c_typecheck_expr.cpp

@@ -2420,7 +2420,8 @@ exprt c_typecheck_baset::do_special_functions(
 
     irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
 
-    predicate_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
+    binary_predicate_exprt ok_expr(
+      expr.arguments()[0], id, expr.arguments()[1]);
     ok_expr.add_source_location() = source_location;
 
     return std::move(ok_expr);

src/goto-analyzer/taint_analysis.cpp

@@ -175,9 +175,10 @@ void taint_analysist::instrument(
               case taint_parse_treet::rulet::SINK:
                 {
                   goto_programt::targett t=insert_before.add_instruction();
-                  binary_predicate_exprt get_may("get_may");
-                  get_may.op0()=where;
-                  get_may.op1()=address_of_exprt(string_constantt(rule.taint));
+                  binary_predicate_exprt get_may(
+                    where,
+                    "get_may",
+                    address_of_exprt(string_constantt(rule.taint)));
                   t->make_assertion(not_exprt(get_may));
                   t->source_location=instruction.source_location;
                   t->source_location.set_property_class(

src/goto-instrument/thread_instrumentation.cpp

@@ -41,11 +41,11 @@ void thread_exit_instrumentation(goto_programt &goto_program)
 
   const string_constantt mutex_locked_string("mutex-locked");
 
-  binary_exprt get_may("get_may");
-
   // NULL is any
-  get_may.op0()=null_pointer_exprt(pointer_type(empty_typet()));
-  get_may.op1()=address_of_exprt(mutex_locked_string);
+  binary_predicate_exprt get_may(
+    null_pointer_exprt(pointer_type(empty_typet())),
+    "get_may",
+    address_of_exprt(mutex_locked_string));
 
   end->make_assertion(not_exprt(get_may));
 

src/solvers/smt2/smt2_parser.cpp

@@ -264,9 +264,7 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   // go backwards, build quantified expression
   for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
   {
-    binary_predicate_exprt quantifier(id);
-    quantifier.op0()=*r_it;
-    quantifier.op1().swap(result);
+    binary_predicate_exprt quantifier(*r_it, id, result);
     result=quantifier;
   }