avoid direct access to exprt::opX

src/goto-symex/build_goto_trace.cpp

@@ -92,12 +92,9 @@ exprt build_full_lhs_rec(
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
-    exprt tmp=src_original;
-    tmp.op0() = build_full_lhs_rec(
-      prop_conv,
-      ns,
-      to_byte_extract_expr(tmp).op(),
-      to_byte_extract_expr(src_ssa).op());
+    byte_extract_exprt tmp = to_byte_extract_expr(src_original);
+    tmp.op() = build_full_lhs_rec(
+      prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
 
     // re-write into big case-split
   }

src/goto-symex/goto_symex_state.cpp

@@ -132,13 +132,20 @@ static bool check_renaming(const exprt &expr)
   if(check_renaming(expr.type()))
     return true;
 
-  if(expr.id()==ID_address_of &&
-     expr.op0().id()==ID_symbol)
-    return check_renaming_l1(expr.op0());
-  else if(expr.id()==ID_address_of &&
-          expr.op0().id()==ID_index)
-    return check_renaming_l1(expr.op0().op0()) ||
-           check_renaming(expr.op0().op1());
+  if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_symbol)
+  {
+    return check_renaming_l1(to_address_of_expr(expr).object());
+  }
+  else if(
+    expr.id() == ID_address_of &&
+    to_address_of_expr(expr).object().id() == ID_index)
+  {
+    const auto index_expr = to_index_expr(to_address_of_expr(expr).object());
+    return check_renaming_l1(index_expr.array()) ||
+           check_renaming(index_expr.index());
+  }
   else if(expr.id()==ID_symbol)
   {
     if(!expr.get_bool(ID_C_SSA_symbol))

src/goto-symex/symex_dead.cpp

@@ -30,7 +30,7 @@ void goto_symext::symex_dead(statet &state)
   state.rename(ssa, ns, goto_symex_statet::L1);
 
   // in case of pointers, put something into the value set
-  if(ns.follow(code.op0().type()).id()==ID_pointer)
+  if(ns.follow(code.symbol().type()).id() == ID_pointer)
   {
     exprt failed = get_failed_symbol(to_symbol_expr(code.symbol()), ns);
 

src/goto-symex/symex_decl.cpp

@@ -28,9 +28,8 @@ void goto_symext::symex_decl(statet &state)
   // two-operand decl not supported here
   // we handle the decl with only one operand
   PRECONDITION(code.operands().size() == 1);
-  PRECONDITION(code.op0().id() == ID_symbol);
 
-  symex_decl(state, to_symbol_expr(code.op0()));
+  symex_decl(state, to_symbol_expr(to_code_decl(code).symbol()));
 }
 
 void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)

src/goto-symex/symex_dereference.cpp

@@ -270,7 +270,7 @@ void goto_symext::dereference_rec(
     }
 
     exprt tmp1;
-    tmp1.swap(expr.op0());
+    tmp1.swap(to_dereference_expr(expr).pointer());
 
     // first make sure there are no dereferences in there
     dereference_rec(tmp1, state, guard, false);

src/goto-symex/symex_function_call.cpp

@@ -435,7 +435,7 @@ void goto_symext::return_assignment(statet &state)
 
   PRECONDITION(code.operands().size() == 1 || frame.return_value.is_nil());
 
-  exprt value = code.op0();
+  exprt value = code.return_value();
 
   if(frame.return_value.is_not_nil())
   {

src/goto-symex/symex_goto.cpp

@@ -233,11 +233,13 @@ void goto_symext::symex_goto(statet &state)
     // produce new guard symbol
     exprt guard_expr;
 
-    if(new_guard.id()==ID_symbol ||
-       (new_guard.id()==ID_not &&
-        new_guard.operands().size()==1 &&
-        new_guard.op0().id()==ID_symbol))
+    if(
+      new_guard.id() == ID_symbol ||
+      (new_guard.id() == ID_not &&
+       to_not_expr(new_guard).op().id() == ID_symbol))
+    {
       guard_expr=new_guard;
+    }
     else
     {
       symbol_exprt guard_symbol_expr=

src/util/config.cpp

@@ -1101,13 +1101,14 @@ static irep_idt string_from_ns(
   const exprt &tmp=symbol->value;
 
   INVARIANT(
-    tmp.id() == ID_address_of && tmp.operands().size() == 1 &&
-      tmp.op0().id() == ID_index && tmp.op0().operands().size() == 2 &&
-      tmp.op0().op0().id() == ID_string_constant,
+    tmp.id() == ID_address_of &&
+      to_address_of_expr(tmp).object().id() == ID_index &&
+      to_index_expr(to_address_of_expr(tmp).object()).array().id() ==
+        ID_string_constant,
     "symbol table configuration entry `" + id2string(id) +
       "' must be a string constant");
 
-  return tmp.op0().op0().get(ID_value);
+  return to_index_expr(to_address_of_expr(tmp).object()).array().get(ID_value);
 }
 
 static unsigned unsigned_from_ns(

src/util/expr_util.cpp

@@ -56,8 +56,8 @@ exprt make_binary(const exprt &expr)
     exprt tmp=expr;
     tmp.operands().clear();
     tmp.operands().resize(2);
-    tmp.op0().swap(previous);
-    tmp.op1()=*it;
+    to_binary_expr(tmp).op0().swap(previous);
+    to_binary_expr(tmp).op1() = *it;
     previous.swap(tmp);
   }
 
@@ -126,8 +126,8 @@ exprt is_not_zero(
 
 exprt boolean_negate(const exprt &src)
 {
-  if(src.id()==ID_not && src.operands().size()==1)
-    return src.op0();
+  if(src.id() == ID_not)
+    return to_not_expr(src).op();
   else if(src.is_true())
     return false_exprt();
   else if(src.is_false())

src/util/json_expr.cpp

@@ -39,42 +39,47 @@ static exprt simplify_json_expr(
     {
       const irep_idt &value=to_constant_expr(src).get_value();
 
-      if(value!=ID_NULL &&
-         (value!=std::string(value.size(), '0') ||
-          !config.ansi_c.NULL_is_zero) &&
-         src.operands().size()==1 &&
-         src.op0().id()!=ID_constant)
-        // try to simplify the constant pointer
-        return simplify_json_expr(src.op0(), ns);
+      if(
+        value != ID_NULL &&
+        (value != std::string(value.size(), '0') ||
+         !config.ansi_c.NULL_is_zero) &&
+        src.operands().size() == 1 &&
+        to_unary_expr(src).op().id() != ID_constant)
+      // try to simplify the constant pointer
+      {
+        return simplify_json_expr(to_unary_expr(src).op(), ns);
+      }
     }
   }
-  else if(src.id()==ID_address_of &&
-          src.operands().size()==1 &&
-          src.op0().id()==ID_member &&
-          id2string(to_member_expr(
-            src.op0()).get_component_name()).find("@")!=std::string::npos)
+  else if(
+    src.id() == ID_address_of &&
+    to_address_of_expr(src).object().id() == ID_member &&
+    id2string(
+      to_member_expr(to_address_of_expr(src).object()).get_component_name())
+        .find("@") != std::string::npos)
   {
     // simplify expressions of the form &member_expr(object, @class_identifier)
-    return simplify_json_expr(src.op0(), ns);
+    return simplify_json_expr(to_address_of_expr(src).object(), ns);
   }
-  else if(src.id()==ID_address_of &&
-          src.operands().size()==1 &&
-          src.op0().id()==ID_index &&
-          to_index_expr(src.op0()).index().id()==ID_constant &&
-          to_constant_expr(
-            to_index_expr(src.op0()).index()).value_is_zero_string())
+  else if(
+    src.id() == ID_address_of &&
+    to_address_of_expr(src).object().id() == ID_index &&
+    to_index_expr(to_address_of_expr(src).object()).index().id() ==
+      ID_constant &&
+    to_constant_expr(to_index_expr(to_address_of_expr(src).object()).index())
+      .value_is_zero_string())
   {
     // simplify expressions of the form  &array[0]
-    return simplify_json_expr(to_index_expr(src.op0()).array(), ns);
+    return simplify_json_expr(
+      to_index_expr(to_address_of_expr(src).object()).array(), ns);
   }
   else if(src.id()==ID_member &&
-          src.operands().size()==1 &&
           id2string(
             to_member_expr(src).get_component_name())
               .find("@")!=std::string::npos)
   {
     // simplify expressions of the form  member_expr(object, @class_identifier)
-    return simplify_json_expr(src.op0(), ns);
+    return simplify_json_expr(to_member_expr(src).struct_op(), ns);
   }
 
   return src;
@@ -317,11 +322,15 @@ json_objectt json(
       result["name"]=json_stringt("pointer");
       result["type"]=json_stringt(type_string);
       exprt simpl_expr=simplify_json_expr(expr, ns);
-      if(simpl_expr.get(ID_value)==ID_NULL ||
-         // remove typecast on NULL
-         (simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer &&
-          simpl_expr.op0().get(ID_value)==ID_NULL))
+      if(
+        simpl_expr.get(ID_value) == ID_NULL ||
+        // remove typecast on NULL
+        (simpl_expr.id() == ID_constant &&
+         simpl_expr.type().id() == ID_pointer &&
+         to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
+      {
         result["data"]=json_stringt(value_string);
+      }
       else if(simpl_expr.id()==ID_symbol)
       {
         const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();

src/util/ssa_expr.cpp

@@ -77,9 +77,10 @@ bool ssa_exprt::can_build_identifier(const exprt &expr)
 {
   if(expr.id()==ID_symbol)
     return true;
-  else if(expr.id()==ID_member ||
-          expr.id()==ID_index)
-    return can_build_identifier(expr.op0());
+  else if(expr.id() == ID_member)
+    return can_build_identifier(to_member_expr(expr).compound());
+  else if(expr.id() == ID_index)
+    return can_build_identifier(to_index_expr(expr).array());
   else
     return false;
 }

src/util/std_code.cpp

@@ -134,9 +134,7 @@ codet &code_blockt::find_last_statement()
     }
     else if(statement==ID_label)
     {
-      DATA_INVARIANT(
-        last->operands().size() == 1, "label must have one operand");
-      last=&(to_code(last->op0()));
+      last = &(to_code_label(*last).code());
     }
     else
       break;