Make make_(free_)bv_expr return exprt

Author: romainbrenguier

src/cbmc/bv_cbmc.cpp

@@ -20,13 +20,11 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
     throw 0;
   }
 
-  exprt new_cycle;
   const exprt &old_cycle=expr.op0();
   const exprt &cycle_var=expr.op1();
   const exprt &bound=expr.op2();
   const exprt &predicate=expr.op3();
-
-  make_free_bv_expr(expr.type(), new_cycle);
+  const exprt new_cycle = make_free_bv_expr(expr.type());
 
   mp_integer bound_value;
   if(to_integer(bound, bound_value))
@@ -98,18 +96,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr)
 
 bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr)
 {
-  if(expr.operands().size()!=1)
-  {
-    error().source_location=expr.find_source_location();
-    error() << "waitfor_symbol expected to have one operand" << eom;
-    throw 0;
-  }
-
-  exprt result;
+  PRECONDITION(expr.operands().size() == 1);
   const exprt &bound=expr.op0();
-
-  make_free_bv_expr(expr.type(), result);
-
+  const exprt result = make_free_bv_expr(expr.type());
   // constraint: result<=bound
 
   set_to_true(binary_relation_exprt(result, ID_le, bound));

src/solvers/flattening/boolbv.cpp

@@ -650,35 +650,25 @@ void boolbvt::set_to(const exprt &expr, bool value)
   return SUB::set_to(expr, value);
 }
 
-void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
+exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
 {
-  dest=exprt(ID_bv_literals, type);
+  exprt dest(ID_bv_literals, type);
   irept::subt &bv_sub=dest.add(ID_bv).get_sub();
-
   bv_sub.resize(bv.size());
 
   for(std::size_t i=0; i<bv.size(); i++)
     bv_sub[i].id(std::to_string(bv[i].get()));
+  return dest;
 }
 
-void boolbvt::make_free_bv_expr(const typet &type, exprt &dest)
+exprt boolbvt::make_free_bv_expr(const typet &type)
 {
-  std::size_t width=boolbv_width(type);
-
-  if(width==0)
-  {
-    error() << "failed to get width of " << type.pretty() << eom;
-    throw 0;
-  }
-
-  bvt bv;
-  bv.resize(width);
-
-  // make result free variables
-  Forall_literals(it, bv)
-    *it=prop.new_variable();
-
-  make_bv_expr(type, bv, dest);
+  const std::size_t width = boolbv_width(type);
+  PRECONDITION(width != 0);
+  bvt bv(width);
+  for(auto &lit : bv)
+    lit = prop.new_variable();
+  return make_bv_expr(type, bv);
 }
 
 bool boolbvt::is_unbounded_array(const typet &type) const

src/solvers/flattening/boolbv.h

@@ -176,8 +176,8 @@ class boolbvt:public arrayst
   virtual bvt convert_function_application(
     const function_application_exprt &expr);
 
-  virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest);
-  virtual void make_free_bv_expr(const typet &type, exprt &dest);
+  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
+  virtual exprt make_free_bv_expr(const typet &type);
 
   void convert_with(
     const typet &type,