Merge pull request #5044 from diffblue/binary_infix_exprt

offer .lhs() and .rhs() for all binary expressions

Author: Daniel Kroening

src/analyses/goto_check.cpp

@@ -1065,11 +1065,11 @@ void goto_checkt::nan_check(
 
     isnan = or_exprt(
       and_exprt(
-        equal_exprt(minus_expr.op0(), plus_inf),
-        equal_exprt(minus_expr.op1(), plus_inf)),
+        equal_exprt(minus_expr.lhs(), plus_inf),
+        equal_exprt(minus_expr.rhs(), plus_inf)),
       and_exprt(
-        equal_exprt(minus_expr.op0(), minus_inf),
-        equal_exprt(minus_expr.op1(), minus_inf)));
+        equal_exprt(minus_expr.lhs(), minus_inf),
+        equal_exprt(minus_expr.rhs(), minus_inf)));
   }
   else
     UNREACHABLE;

src/solvers/flattening/bv_pointers.cpp

@@ -393,23 +393,23 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     const minus_exprt &minus_expr = to_minus_expr(expr);
 
     INVARIANT(
-      minus_expr.op0().type().id() == ID_pointer,
+      minus_expr.lhs().type().id() == ID_pointer,
       "first operand should be of pointer type");
 
     if(
-      minus_expr.op1().type().id() != ID_unsignedbv &&
-      minus_expr.op1().type().id() != ID_signedbv)
+      minus_expr.rhs().type().id() != ID_unsignedbv &&
+      minus_expr.rhs().type().id() != ID_signedbv)
     {
       bvt bv;
       conversion_failed(minus_expr, bv);
       return bv;
     }
 
-    const unary_minus_exprt neg_op1(minus_expr.op1());
+    const unary_minus_exprt neg_op1(minus_expr.rhs());
 
-    bvt bv = convert_bv(minus_expr.op0());
+    bvt bv = convert_bv(minus_expr.lhs());
 
-    typet pointer_sub_type = minus_expr.op0().type().subtype();
+    typet pointer_sub_type = minus_expr.rhs().type().subtype();
     mp_integer element_size;
 
     if(pointer_sub_type.id()==ID_empty)

src/util/std_expr.h

@@ -691,6 +691,26 @@ class binary_exprt : public expr_protectedt
     check(expr, vm);
   }
 
+  exprt &lhs()
+  {
+    return exprt::op0();
+  }
+
+  const exprt &lhs() const
+  {
+    return exprt::op0();
+  }
+
+  exprt &rhs()
+  {
+    return exprt::op1();
+  }
+
+  const exprt &rhs() const
+  {
+    return exprt::op1();
+  }
+
   // make op0 and op1 public
   using exprt::op0;
   using exprt::op1;
@@ -821,26 +841,6 @@ class binary_relation_exprt:public binary_predicate_exprt
       expr_binary.op0().type() == expr_binary.op1().type(),
       "lhs and rhs of binary relation expression should have same type");
   }
-
-  exprt &lhs()
-  {
-    return op0();
-  }
-
-  const exprt &lhs() const
-  {
-    return op0();
-  }
-
-  exprt &rhs()
-  {
-    return op1();
-  }
-
-  const exprt &rhs() const
-  {
-    return op1();
-  }
 };
 
 template <>