replace exprt::opX by named methods

This will eventually enable us to protect the opX methods.

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -1673,8 +1673,8 @@ void c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(
   typecheck_expr_trinary(if_expr);
 
   // copy the result
-  expr.op0()=if_expr.op1();
-  expr.op1()=if_expr.op2();
+  expr.op0() = if_expr.true_case();
+  expr.op1() = if_expr.false_case();
   expr.type()=if_expr.type();
 }
 

src/goto-programs/builtin_functions.cpp

@@ -1402,9 +1402,11 @@ void goto_convertt::do_function_call_symbol(
     }
 
     // build (*ptr==oldval)?newval:*ptr
-    if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
-    if(if_expr.op1().type()!=if_expr.type())
-      if_expr.op1().make_typecast(if_expr.type());
+    if_exprt if_expr(
+      equal,
+      typecast_exprt::conditional_cast(arguments[2], deref_ptr.type()),
+      deref_ptr,
+      deref_ptr.type());
 
     goto_programt::targett t3=dest.add_instruction(ASSIGN);
     t3->source_location=function.source_location();
@@ -1461,9 +1463,11 @@ void goto_convertt::do_function_call_symbol(
       equal.op1().make_typecast(equal.op0().type());
 
     // build (*ptr==oldval)?newval:*ptr
-    if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
-    if(if_expr.op1().type()!=if_expr.type())
-      if_expr.op1().make_typecast(if_expr.type());
+    if_exprt if_expr(
+      equal,
+      typecast_exprt::conditional_cast(arguments[2], deref_ptr.type()),
+      deref_ptr,
+      deref_ptr.type());
 
     goto_programt::targett t3=dest.add_instruction(ASSIGN);
     t3->source_location=function.source_location();

src/solvers/lowering/byte_operators.cpp

@@ -362,9 +362,9 @@ static exprt lower_byte_update(
 
   const mp_integer &element_size = *element_size_opt;
 
-  if(src.op0().type().id()==ID_array)
+  if(src.op().type().id()==ID_array)
   {
-    const array_typet &array_type=to_array_type(src.op0().type());
+    const array_typet &array_type=to_array_type(src.op().type());
     const typet &subtype=array_type.subtype();
 
     // array of bitvectors?
@@ -531,14 +531,14 @@ static exprt lower_byte_update(
         subtype.id_string());
     }
   }
-  else if(src.op0().type().id()==ID_signedbv ||
-          src.op0().type().id()==ID_unsignedbv ||
-          src.op0().type().id()==ID_floatbv ||
-          src.op0().type().id()==ID_c_bool ||
-          src.op0().type().id()==ID_pointer)
+  else if(src.op().type().id()==ID_signedbv ||
+          src.op().type().id()==ID_unsignedbv ||
+          src.op().type().id()==ID_floatbv ||
+          src.op().type().id()==ID_c_bool ||
+          src.op().type().id()==ID_pointer)
   {
     // do a shift, mask and OR
-    const auto type_width = pointer_offset_bits(src.op0().type(), ns);
+    const auto type_width = pointer_offset_bits(src.op().type(), ns);
     CHECK_RETURN(type_width.has_value() && *type_width > 0);
     const std::size_t width = numeric_cast_v<std::size_t>(*type_width);
 
@@ -560,7 +560,7 @@ static exprt lower_byte_update(
           unsignedbv_typet(
             width - numeric_cast_v<std::size_t>(element_size) * 8)),
         src.value(),
-        src.op0().type());
+        src.op().type());
     else
       value_extended = src.value();
 
@@ -602,7 +602,7 @@ static exprt lower_byte_update(
     PRECONDITION_WITH_DIAGNOSTICS(
       false,
       "flatten_byte_update can only do arrays and scalars right now",
-      src.op0().type().id_string());
+      src.op().type().id_string());
   }
 }
 

src/util/simplify_expr.cpp

@@ -2061,8 +2061,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
             plus_exprt new_offset(offset, compo_offset);
             simplify_node(new_offset);
             exprt new_value(with.new_value());
-            expr.op1().swap(new_offset);
-            expr.op2().swap(new_value);
+            expr.offset().swap(new_offset);
+            expr.value().swap(new_value);
             simplify_byte_update(expr); // do this recursively
             return false;
           }
@@ -2088,8 +2088,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
           plus_exprt new_offset(offset, index_offset);
           simplify_node(new_offset);
           exprt new_value(with.new_value());
-          expr.op1().swap(new_offset);
-          expr.op2().swap(new_value);
+          expr.offset().swap(new_offset);
+          expr.value().swap(new_value);
           simplify_byte_update(expr); // do this recursively
           return false;
         }