use codet constructors with operands

This prevents construction followed by another assignment.

Author: Daniel Kroening

src/util/std_code.h

@@ -187,14 +187,14 @@ class code_blockt:public codet
     return result;
   }
 
-  explicit code_blockt(const std::vector<codet> &_statements):codet(ID_block)
+  explicit code_blockt(const std::vector<codet> &_statements)
+    : codet(ID_block, (const std::vector<exprt> &)_statements)
   {
-    operands()=(const std::vector<exprt> &)_statements;
   }
 
-  explicit code_blockt(std::vector<codet> &&_statements):codet(ID_block)
+  explicit code_blockt(std::vector<codet> &&_statements)
+    : codet(ID_block, std::move((std::vector<exprt> &&) _statements))
   {
-    operands()=std::move((std::vector<exprt> &&)_statements);
   }
 
   void add(const codet &code)
@@ -272,9 +272,9 @@ class code_assignt:public codet
     operands().resize(2);
   }
 
-  code_assignt(const exprt &lhs, const exprt &rhs):codet(ID_assign)
+  code_assignt(const exprt &lhs, const exprt &rhs)
+    : codet(ID_assign, {lhs, rhs})
   {
-    add_to_operands(lhs, rhs);
   }
 
   exprt &lhs()
@@ -435,9 +435,8 @@ inline code_declt &to_code_decl(codet &code)
 class code_deadt:public codet
 {
 public:
-  explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead)
+  explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead, {symbol})
   {
-    add_to_operands(symbol);
   }
 
   symbol_exprt &symbol()
@@ -513,9 +512,8 @@ class code_assumet:public codet
     operands().resize(1);
   }
 
-  explicit code_assumet(const exprt &expr):codet(ID_assume)
+  explicit code_assumet(const exprt &expr) : codet(ID_assume, {expr})
   {
-    add_to_operands(expr);
   }
 
   const exprt &assumption() const
@@ -565,9 +563,8 @@ class code_assertt:public codet
     operands().resize(1);
   }
 
-  explicit code_assertt(const exprt &expr):codet(ID_assert)
+  explicit code_assertt(const exprt &expr) : codet(ID_assert, {expr})
   {
-    add_to_operands(expr);
   }
 
   const exprt &assertion() const
@@ -638,16 +635,14 @@ class code_ifthenelset:public codet
     const exprt &condition,
     const codet &then_code,
     const codet &else_code)
-    : codet(ID_ifthenelse)
+    : codet(ID_ifthenelse, {condition, then_code, else_code})
   {
-    add_to_operands(condition, then_code, else_code);
   }
 
   /// An if \p condition then \p then_code statement (no "else" case).
   code_ifthenelset(const exprt &condition, const codet &then_code)
-    : codet(ID_ifthenelse)
+    : codet(ID_ifthenelse, {condition, then_code, nil_exprt()})
   {
-    add_to_operands(condition, then_code, nil_exprt());
   }
 
   const exprt &cond() const
@@ -722,11 +717,9 @@ class code_switcht:public codet
     operands().resize(2);
   }
 
-  code_switcht(const exprt &_value, const codet &_body) : codet(ID_switch)
+  code_switcht(const exprt &_value, const codet &_body)
+    : codet(ID_switch, {_value, _body})
   {
-    operands().resize(2);
-    value() = _value;
-    body() = _body;
   }
 
   const exprt &value() const
@@ -784,11 +777,9 @@ class code_whilet:public codet
     operands().resize(2);
   }
 
-  code_whilet(const exprt &_cond, const codet &_body) : codet(ID_while)
+  code_whilet(const exprt &_cond, const codet &_body)
+    : codet(ID_while, {_cond, _body})
   {
-    operands().resize(2);
-    cond() = _cond;
-    body() = _body;
   }
 
   const exprt &cond() const
@@ -846,11 +837,9 @@ class code_dowhilet:public codet
     operands().resize(2);
   }
 
-  code_dowhilet(const exprt &_cond, const codet &_body) : codet(ID_dowhile)
+  code_dowhilet(const exprt &_cond, const codet &_body)
+    : codet(ID_dowhile, {_cond, _body})
   {
-    operands().resize(2);
-    cond() = _cond;
-    body() = _body;
   }
 
   const exprt &cond() const
@@ -917,11 +906,8 @@ class code_fort:public codet
     const exprt &_cond,
     const exprt &_iter,
     const codet &_body)
-    : codet(ID_for)
+    : codet(ID_for, {_init, _cond, _iter, _body})
   {
-    reserve_operands(4);
-    add_to_operands(_init, _cond, _iter);
-    add_to_operands(_body);
   }
 
   // nil or a statement
@@ -1203,9 +1189,8 @@ class code_returnt:public codet
     op0().make_nil();
   }
 
-  explicit code_returnt(const exprt &_op):codet(ID_return)
+  explicit code_returnt(const exprt &_op) : codet(ID_return, {_op})
   {
-    add_to_operands(_op);
   }
 
   const exprt &return_value() const
@@ -1275,12 +1260,10 @@ class code_labelt:public codet
     set_label(_label);
   }
 
-  code_labelt(
-    const irep_idt &_label, const codet &_code):codet(ID_label)
+  code_labelt(const irep_idt &_label, const codet &_code)
+    : codet(ID_label, {_code})
   {
-    operands().resize(1);
     set_label(_label);
-    code()=_code;
   }
 
   const irep_idt &get_label() const
@@ -1339,10 +1322,9 @@ class code_switch_caset:public codet
     operands().resize(2);
   }
 
-  code_switch_caset(
-    const exprt &_case_op, const codet &_code):codet(ID_switch_case)
+  code_switch_caset(const exprt &_case_op, const codet &_code)
+    : codet(ID_switch_case, {_case_op, _code})
   {
-    add_to_operands(_case_op, _code);
   }
 
   bool is_default() const
@@ -1470,9 +1452,8 @@ class code_asmt:public codet
   {
   }
 
-  explicit code_asmt(const exprt &expr):codet(ID_asm)
+  explicit code_asmt(const exprt &expr) : codet(ID_asm, {expr})
   {
-    add_to_operands(expr);
   }
 
   const irep_idt &get_flavor() const
@@ -1517,9 +1498,8 @@ class code_expressiont:public codet
     operands().resize(1);
   }
 
-  explicit code_expressiont(const exprt &expr):codet(ID_expression)
+  explicit code_expressiont(const exprt &expr) : codet(ID_expression, {expr})
   {
-    add_to_operands(expr);
   }
 
   const exprt &expression() const
@@ -2117,9 +2097,9 @@ class code_try_catcht:public codet
   }
 
   /// A statement representing try \p _try_code catch ...
-  explicit code_try_catcht(const codet &_try_code) : codet(ID_try_catch)
+  explicit code_try_catcht(const codet &_try_code)
+    : codet(ID_try_catch, {_try_code})
   {
-    add_to_operands(_try_code);
   }
 
   codet &try_code()