Merge pull request #5030 from diffblue/unit-opX

Daniel Kroening · web-flow · commit 31ce65bd506e · 2019-08-22T10:14:40.000+01:00
fix accesses to exprt::opX() in unit/
diff --git a/unit/solvers/strings/string_refinement/substitute_array_list.cpp b/unit/solvers/strings/string_refinement/substitute_array_list.cpp
@@ -37,19 +37,19 @@ SCENARIO("substitute_array_list", "[core][solvers][strings][string_refinement]")
   // Check that `subst = e1 WITH [1:='y']`
   REQUIRE(subst.id() == ID_with);
   REQUIRE(subst.operands().size() == 3);
-  const exprt &e1 = subst.op0();
-  REQUIRE(subst.op1() == index1);
-  REQUIRE(subst.op2() == chary);
+  const exprt &e1 = to_with_expr(subst).old();
+  REQUIRE(to_with_expr(subst).where() == index1);
+  REQUIRE(to_with_expr(subst).new_value() == chary);
 
   // Check that `e1 = e2 WITH [0:='x']`
   REQUIRE(e1.id() == ID_with);
   REQUIRE(e1.operands().size() == 3);
-  const exprt &e2 = e1.op0();
-  REQUIRE(e1.op1() == index0);
-  REQUIRE(e1.op2() == charx);
+  const exprt &e2 = to_with_expr(e1).old();
+  REQUIRE(to_with_expr(e1).where() == index0);
+  REQUIRE(to_with_expr(e1).new_value() == charx);
 
   // Check that `e1 = ARRAY_OF 0`
   REQUIRE(e2.id() == ID_array_of);
   REQUIRE(e2.operands().size() == 1);
-  REQUIRE(e2.op0() == from_integer(0, char_type));
+  REQUIRE(to_array_of_expr(e2).op() == from_integer(0, char_type));
 }
diff --git a/unit/util/interval_constraint.cpp b/unit/util/interval_constraint.cpp
@@ -31,16 +31,20 @@ SCENARIO(
         "expressions representing a <= expr && expr <= z")
       {
         REQUIRE(can_cast_expr<and_exprt>(result));
+        REQUIRE(result.operands().size() == 2);
+        const auto &result_binary = to_binary_expr(result);
 
-        REQUIRE(result.op0().id() == ID_ge);
-        REQUIRE(result.op0().op0().type() == unsignedbv_typet(16));
-        REQUIRE(can_cast_expr<constant_exprt>(result.op0().op1()));
-        REQUIRE(to_constant_expr(result.op0().op1()).get_value() == "61"); // a
+        REQUIRE(result_binary.op0().id() == ID_ge);
+        const auto &op0_binary = to_binary_expr(result_binary.op0());
+        REQUIRE(op0_binary.op0().type() == unsignedbv_typet(16));
+        REQUIRE(can_cast_expr<constant_exprt>(op0_binary.op1()));
+        REQUIRE(to_constant_expr(op0_binary.op1()).get_value() == "61"); // a
 
-        REQUIRE(result.op1().id() == ID_le);
-        REQUIRE(result.op1().op0().type() == unsignedbv_typet(16));
-        REQUIRE(can_cast_expr<constant_exprt>(result.op1().op1()));
-        REQUIRE(to_constant_expr(result.op1().op1()).get_value() == "7A"); // b
+        REQUIRE(result_binary.op1().id() == ID_le);
+        const auto &op1_binary = to_binary_expr(result_binary.op1());
+        REQUIRE(op1_binary.op0().type() == unsignedbv_typet(16));
+        REQUIRE(can_cast_expr<constant_exprt>(op1_binary.op1()));
+        REQUIRE(to_constant_expr(op1_binary.op1()).get_value() == "7A"); // b
       }
     }
   }
@@ -64,16 +68,20 @@ SCENARIO(
         "expressions representing 6 <= expr && expr <= 9")
       {
         REQUIRE(can_cast_expr<and_exprt>(result));
+        REQUIRE(result.operands().size() == 2);
+        const auto &result_binary = to_binary_expr(result);
 
-        REQUIRE(result.op0().id() == ID_ge);
-        REQUIRE(result.op0().op0().type() == unsignedbv_typet(32));
-        REQUIRE(can_cast_expr<constant_exprt>(result.op0().op1()));
-        REQUIRE(to_constant_expr(result.op0().op1()).get_value() == "6");
+        REQUIRE(result_binary.op0().id() == ID_ge);
+        const auto &op0_binary = to_binary_expr(result_binary.op0());
+        REQUIRE(op0_binary.op0().type() == unsignedbv_typet(32));
+        REQUIRE(can_cast_expr<constant_exprt>(op0_binary.op1()));
+        REQUIRE(to_constant_expr(op0_binary.op1()).get_value() == "6");
 
-        REQUIRE(result.op1().id() == ID_le);
-        REQUIRE(result.op1().op0().type() == unsignedbv_typet(32));
-        REQUIRE(can_cast_expr<constant_exprt>(result.op1().op1()));
-        REQUIRE(to_constant_expr(result.op1().op1()).get_value() == "9");
+        REQUIRE(result_binary.op1().id() == ID_le);
+        const auto &op1_binary = to_binary_expr(result_binary.op1());
+        REQUIRE(op1_binary.op0().type() == unsignedbv_typet(32));
+        REQUIRE(can_cast_expr<constant_exprt>(op1_binary.op1()));
+        REQUIRE(to_constant_expr(op1_binary.op1()).get_value() == "9");
       }
     }
   }
diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp
@@ -3,7 +3,9 @@
 /// \file Tests that irep sharing works correctly
 
 #include <testing-utils/use_catch.h>
+
 #include <util/irep.h>
+#include <util/std_expr.h>
 
 #ifdef SHARING
 
@@ -118,7 +120,7 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
 {
   GIVEN("An expression created with add_to_operands(std::move(...))")
   {
-    exprt test_expr(ID_1);
+    multi_ary_exprt test_expr(ID_1);
     exprt test_subexpr(ID_1);
     exprt test_subsubexpr(ID_1);
     test_subexpr.add_to_operands(std::move(test_subsubexpr));
@@ -132,15 +134,15 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
       "copying should not change them in the copy")
     {
       exprt &operand = test_expr.op0();
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       operand.id(ID_0);
       REQUIRE(test_expr.op0().id() == ID_0);
       REQUIRE(expr.op0().id() == ID_1);
     }
     THEN("Holding a reference to an operand should not prevent sharing")
     {
       exprt &operand = test_expr.op0();
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       REQUIRE(&expr.read() == &test_expr.read());
       operand = exprt(ID_0);
       REQUIRE(expr.op0().id() == test_expr.op0().id());
@@ -152,7 +154,7 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
 {
   GIVEN("An expression created with add_to_operands(std::move(...))")
   {
-    exprt test_expr(ID_1);
+    multi_ary_exprt test_expr(ID_1);
     exprt test_subexpr(ID_1);
     exprt test_subsubexpr(ID_1);
     test_subexpr.add_to_operands(std::move(test_subsubexpr));
@@ -165,20 +167,20 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
     }
     THEN("Changing operands in the original should not change them in a copy")
     {
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       test_expr.op0().id(ID_0);
       REQUIRE(expr.op0().id() == ID_1);
     }
     THEN("Changing operands in a copy should not change them in the original")
     {
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       expr.op0().id(ID_0);
       REQUIRE(test_expr.op0().id() == ID_1);
       REQUIRE(expr.op0().id() == ID_0);
     }
     THEN("Getting a reference to an operand in a copy should break sharing")
     {
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       exprt &operand = expr.op0();
       REQUIRE(&expr.read() != &test_expr.read());
       operand = exprt(ID_0);
@@ -187,7 +189,7 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
     THEN(
       "Getting a reference to an operand in the original should break sharing")
     {
-      exprt expr = test_expr;
+      multi_ary_exprt expr = test_expr;
       exprt &operand = test_expr.op0();
       REQUIRE(&expr.read() != &test_expr.read());
       operand = exprt(ID_0);
diff --git a/unit/util/replace_symbol.cpp b/unit/util/replace_symbol.cpp
@@ -16,9 +16,7 @@ TEST_CASE("Replace all symbols in expression", "[core][util][replace_symbol]")
   symbol_exprt s1("a", typet("some_type"));
   symbol_exprt s2("b", typet("some_type"));
 
-  exprt binary("binary", typet("some_type"));
-  binary.copy_to_operands(s1);
-  binary.copy_to_operands(s2);
+  binary_exprt binary(s1, "binary", s2, typet("some_type"));
 
   array_typet array_type(typet("sub-type"), s1);
   REQUIRE(array_type.size() == s1);
@@ -55,9 +53,11 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
   symbol_exprt array("b", array_type);
   index_exprt index(array, s1);
 
-  exprt binary("binary", typet("some_type"));
-  binary.copy_to_operands(address_of_exprt(s1));
-  binary.copy_to_operands(address_of_exprt(index));
+  binary_exprt binary(
+    address_of_exprt(s1),
+    "binary",
+    address_of_exprt(index),
+    typet("some_type"));
 
   constant_exprt c("some_value", typet("some_type"));
 
@@ -86,9 +86,11 @@ TEST_CASE("Replace always", "[core][util][replace_symbol]")
   symbol_exprt array("b", array_type);
   index_exprt index(array, s1);
 
-  exprt binary("binary", typet("some_type"));
-  binary.copy_to_operands(address_of_exprt(s1));
-  binary.copy_to_operands(address_of_exprt(index));
+  binary_exprt binary(
+    address_of_exprt(s1),
+    "binary",
+    address_of_exprt(index),
+    typet("some_type"));
 
   constant_exprt c("some_value", typet("some_type"));
 

Original file line number	Diff line number	Diff line change
`@@ -3,7 +3,9 @@`
`3`	`3`	`/// \file Tests that irep sharing works correctly`
`4`	`4`
`5`	`5`	`#include <testing-utils/use_catch.h>`
	`6`	`+`
`6`	`7`	`#include <util/irep.h>`
	`8`	`+#include <util/std_expr.h>`
`7`	`9`
`8`	`10`	`#ifdef SHARING`
`9`	`11`
`@@ -118,7 +120,7 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")`
`118`	`120`	`{`
`119`	`121`	`GIVEN("An expression created with add_to_operands(std::move(...))")`
`120`	`122`	`{`
`121`		`- exprt test_expr(ID_1);`
	`123`	`+ multi_ary_exprt test_expr(ID_1);`
`122`	`124`	`exprt test_subexpr(ID_1);`
`123`	`125`	`exprt test_subsubexpr(ID_1);`
`124`	`126`	`test_subexpr.add_to_operands(std::move(test_subsubexpr));`
`@@ -132,15 +134,15 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")`
`132`	`134`	`"copying should not change them in the copy")`
`133`	`135`	`{`
`134`	`136`	`exprt &operand = test_expr.op0();`
`135`		`- exprt expr = test_expr;`
	`137`	`+ multi_ary_exprt expr = test_expr;`
`136`	`138`	`operand.id(ID_0);`
`137`	`139`	`REQUIRE(test_expr.op0().id() == ID_0);`
`138`	`140`	`REQUIRE(expr.op0().id() == ID_1);`
`139`	`141`	`}`
`140`	`142`	`THEN("Holding a reference to an operand should not prevent sharing")`
`141`	`143`	`{`
`142`	`144`	`exprt &operand = test_expr.op0();`
`143`		`- exprt expr = test_expr;`
	`145`	`+ multi_ary_exprt expr = test_expr;`
`144`	`146`	`REQUIRE(&expr.read() == &test_expr.read());`
`145`	`147`	`operand = exprt(ID_0);`
`146`	`148`	`REQUIRE(expr.op0().id() == test_expr.op0().id());`
`@@ -152,7 +154,7 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")`
`152`	`154`	`{`
`153`	`155`	`GIVEN("An expression created with add_to_operands(std::move(...))")`
`154`	`156`	`{`
`155`		`- exprt test_expr(ID_1);`
	`157`	`+ multi_ary_exprt test_expr(ID_1);`
`156`	`158`	`exprt test_subexpr(ID_1);`
`157`	`159`	`exprt test_subsubexpr(ID_1);`
`158`	`160`	`test_subexpr.add_to_operands(std::move(test_subsubexpr));`
`@@ -165,20 +167,20 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")`
`165`	`167`	`}`
`166`	`168`	`THEN("Changing operands in the original should not change them in a copy")`
`167`	`169`	`{`
`168`		`- exprt expr = test_expr;`
	`170`	`+ multi_ary_exprt expr = test_expr;`
`169`	`171`	`test_expr.op0().id(ID_0);`
`170`	`172`	`REQUIRE(expr.op0().id() == ID_1);`
`171`	`173`	`}`
`172`	`174`	`THEN("Changing operands in a copy should not change them in the original")`
`173`	`175`	`{`
`174`		`- exprt expr = test_expr;`
	`176`	`+ multi_ary_exprt expr = test_expr;`
`175`	`177`	`expr.op0().id(ID_0);`
`176`	`178`	`REQUIRE(test_expr.op0().id() == ID_1);`
`177`	`179`	`REQUIRE(expr.op0().id() == ID_0);`
`178`	`180`	`}`
`179`	`181`	`THEN("Getting a reference to an operand in a copy should break sharing")`
`180`	`182`	`{`
`181`		`- exprt expr = test_expr;`
	`183`	`+ multi_ary_exprt expr = test_expr;`
`182`	`184`	`exprt &operand = expr.op0();`
`183`	`185`	`REQUIRE(&expr.read() != &test_expr.read());`
`184`	`186`	`operand = exprt(ID_0);`
`@@ -187,7 +189,7 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")`
`187`	`189`	`THEN(`
`188`	`190`	`"Getting a reference to an operand in the original should break sharing")`
`189`	`191`	`{`
`190`		`- exprt expr = test_expr;`
	`192`	`+ multi_ary_exprt expr = test_expr;`
`191`	`193`	`exprt &operand = test_expr.op0();`
`192`	`194`	`REQUIRE(&expr.read() != &test_expr.read());`
`193`	`195`	`operand = exprt(ID_0);`