avoid usage of partial constructor for constant_exprt

Author: Daniel Kroening

src/goto-cc/linker_script_merge.cpp

@@ -565,10 +565,11 @@ int linker_script_merget::ls_data2instructions(
 
     symbol_exprt lhs(d["sym"].value, pointer_type(char_type()));
 
-    constant_exprt rhs;
-    rhs.set_value(integer2binary(string2integer(id2string(symbol_value)),
-          unsigned_int_type().get_width()));
-    rhs.type()=unsigned_int_type();
+    constant_exprt rhs(
+      integer2binary(
+        string2integer(id2string(symbol_value)),
+        unsigned_int_type().get_width()),
+      unsigned_int_type());
 
     exprt rhs_tc(rhs);
     rhs_tc.make_typecast(pointer_type(char_type()));

src/solvers/flattening/boolbv_get.cpp

@@ -255,17 +255,13 @@ exprt boolbvt::bv_get_rec(
       mp_integer int_value=binary2integer(value, false);
       mp_integer from=string2integer(type.get_string(ID_from));
 
-      constant_exprt value_expr(type);
-      value_expr.set_value(integer2string(int_value+from));
-      return value_expr;
+      return constant_exprt(integer2string(int_value + from), type);
     }
     break;
 
   default:
   case bvtypet::IS_C_ENUM:
-    constant_exprt value_expr(type);
-    value_expr.set_value(value);
-    return value_expr;
+    return constant_exprt(value, type);
   }
 
   return nil_exprt();

src/solvers/flattening/bv_pointers.cpp

@@ -633,8 +633,7 @@ exprt bv_pointerst::bv_get_rec(
   // we treat these like bit-vector constants, but with
   // some additional annotation
 
-  constant_exprt result(type);
-  result.set_value(value);
+  constant_exprt result(value, type);
 
   pointer_logict::pointert pointer;
   pointer.object=integer2size_t(binary2integer(value_addr, false));

src/solvers/flattening/pointer_logic.cpp

@@ -80,30 +80,24 @@ exprt pointer_logict::pointer_expr(
   {
     if(pointer.offset==0)
     {
-      constant_exprt result(type);
-      result.set_value(ID_NULL);
+      null_pointer_exprt result(type);
       return result;
     }
     else
     {
-      constant_exprt null(type);
-      null.set_value(ID_NULL);
+      null_pointer_exprt null(type);
       return plus_exprt(null,
         from_integer(pointer.offset, pointer_diff_type()));
     }
   }
   else if(pointer.object==invalid_object) // INVALID?
   {
-    constant_exprt result(type);
-    result.set_value("INVALID");
-    return result;
+    return constant_exprt("INVALID", type);
   }
 
   if(pointer.object>=objects.size())
   {
-    constant_exprt result(type);
-    result.set_value("INVALID-"+std::to_string(pointer.object));
-    return result;
+    return constant_exprt("INVALID-" + std::to_string(pointer.object), type);
   }
 
   const exprt &object_expr=objects[pointer.object];

src/solvers/smt2/smt2_conv.cpp

@@ -2300,7 +2300,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
 
     if(src_type.id()==ID_bool)
     {
-      constant_exprt val(dest_type);
+      constant_exprt val(irep_idt(), dest_type);
 
       ieee_floatt a(to_floatbv_type(dest_type));
 

src/util/arith_tools.cpp

@@ -113,9 +113,7 @@ constant_exprt from_integer(
 
   if(type_id==ID_integer)
   {
-    constant_exprt result(type);
-    result.set_value(integer2string(int_value));
-    return result;
+    return constant_exprt(integer2string(int_value), type);
   }
   else if(type_id==ID_natural)
   {
@@ -125,45 +123,34 @@ constant_exprt from_integer(
       r.make_nil();
       return r;
     }
-    constant_exprt result(type);
-    result.set_value(integer2string(int_value));
-    return result;
+
+    return constant_exprt(integer2string(int_value), type);
   }
   else if(type_id==ID_unsignedbv)
   {
     std::size_t width=to_unsignedbv_type(type).get_width();
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_bv)
   {
     std::size_t width=to_bv_type(type).get_width();
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_signedbv)
   {
     std::size_t width=to_signedbv_type(type).get_width();
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
       to_c_enum_type(type).subtype().get_size_t(ID_width);
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
   {
     std::size_t width=to_c_bool_type(type).get_width();
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_bool)
   {
@@ -180,9 +167,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_bit_field)
   {
     std::size_t width=to_c_bit_field_type(type).get_width();
-    constant_exprt result(type);
-    result.set_value(integer2binary(int_value, width));
-    return result;
+    return constant_exprt(integer2binary(int_value, width), type);
   }
   else if(type_id==ID_fixedbv)
   {

src/util/bv_arithmetic.cpp

@@ -85,9 +85,7 @@ mp_integer bv_arithmetict::pack() const
 
 exprt bv_arithmetict::to_expr() const
 {
-  constant_exprt result(spec.to_type());
-  result.set_value(integer2binary(value, spec.width));
-  return result;
+  return constant_exprt(integer2binary(value, spec.width), spec.to_type());
 }
 
 bv_arithmetict &bv_arithmetict::operator/=(const bv_arithmetict &other)

src/util/fixedbv.cpp

@@ -45,10 +45,8 @@ constant_exprt fixedbvt::to_expr() const
   fixedbv_typet type;
   type.set_width(spec.width);
   type.set_integer_bits(spec.integer_bits);
-  constant_exprt expr(type);
   assert(spec.width!=0);
-  expr.set_value(integer2binary(v, spec.width));
-  return expr;
+  return constant_exprt(integer2binary(v, spec.width), type);
 }
 
 void fixedbvt::round(const fixedbv_spect &dest_spec)

src/util/ieee_float.cpp

@@ -696,9 +696,7 @@ void ieee_floatt::divide_and_round(
 
 constant_exprt ieee_floatt::to_expr() const
 {
-  constant_exprt result(spec.to_type());
-  result.set_value(integer2binary(pack(), spec.width()));
-  return result;
+  return constant_exprt(integer2binary(pack(), spec.width()), spec.to_type());
 }
 
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)

src/util/json_expr.cpp

@@ -276,9 +276,9 @@ json_objectt json(
     }
     else if(type.id()==ID_c_enum_tag)
     {
-      constant_exprt tmp;
-      tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
-      tmp.set_value(to_constant_expr(expr).get_value());
+      constant_exprt tmp(
+        to_constant_expr(expr).get_value(),
+        ns.follow_tag(to_c_enum_tag_type(type)));
       return json(tmp, ns, mode);
     }
     else if(type.id()==ID_bv)

src/util/rational_tools.cpp

@@ -83,8 +83,5 @@ constant_exprt from_rational(const rationalt &a)
   std::string d=integer2string(a.get_numerator());
   if(a.get_denominator()!=1)
     d+="/"+integer2string(a.get_denominator());
-  constant_exprt result;
-  result.type()=rational_typet();
-  result.set_value(d);
-  return result;
+  return constant_exprt(d, rational_typet());
 }

src/util/simplify_expr_int.cpp

@@ -743,7 +743,6 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
 
     assert(a_str.size()==b_str.size());
 
-    constant_exprt new_op(expr.type());
     std::string new_value;
     new_value.resize(width);
 
@@ -765,7 +764,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     else
       break;
 
-    new_op.set_value(new_value);
+    constant_exprt new_op(new_value, expr.type());
 
     // erase first operand
     expr.operands().erase(expr.operands().begin());
@@ -829,8 +828,7 @@ bool simplify_exprt::simplify_bitwise(exprt &expr)
     }
     else if(expr.id()==ID_bitxor)
     {
-      constant_exprt new_op(expr.type());
-      new_op.set_value(integer2binary(0, width));
+      constant_exprt new_op(integer2binary(0, width), expr.type());
       expr.swap(new_op);
       return false;
     }

src/util/std_expr.h

@@ -4149,19 +4149,17 @@ template<> inline bool can_cast_expr<constant_exprt>(const exprt &base)
 class true_exprt:public constant_exprt
 {
 public:
-  true_exprt():constant_exprt(bool_typet())
+  true_exprt() : constant_exprt(ID_true, bool_typet())
   {
-    set_value(ID_true);
   }
 };
 
 /// \brief The Boolean constant false
 class false_exprt:public constant_exprt
 {
 public:
-  false_exprt():constant_exprt(bool_typet())
+  false_exprt() : constant_exprt(ID_false, bool_typet())
   {
-    set_value(ID_false);
   }
 };
 
@@ -4178,9 +4176,9 @@ class nil_exprt:public exprt
 class null_pointer_exprt:public constant_exprt
 {
 public:
-  explicit null_pointer_exprt(const pointer_typet &type):constant_exprt(type)
+  explicit null_pointer_exprt(const pointer_typet &type)
+    : constant_exprt(ID_NULL, type)
   {
-    set_value(ID_NULL);
   }
 };
 

src/util/xml_expr.cpp

@@ -199,9 +199,9 @@ xmlt xml(
     }
     else if(type.id()==ID_c_enum_tag)
     {
-      constant_exprt tmp;
-      tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
-      tmp.set_value(to_constant_expr(expr).get_value());
+      constant_exprt tmp(
+        to_constant_expr(expr).get_value(),
+        ns.follow_tag(to_c_enum_tag_type(type)));
       return xml(tmp, ns);
     }
     else if(type.id()==ID_bv)