Skip to content

Commit abdb044

Browse files
NathanJPhillipstautschnig
authored andcommitted
Unit test to check that irept implements sharing
Separately test irept and exprt, where the latter are expected to have the very same behaviour.
1 parent d58fd18 commit abdb044

File tree

1 file changed

+20
-0
lines changed

1 file changed

+20
-0
lines changed

unit/util/irep_sharing.cpp

+20
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,16 @@ SCENARIO("irept_sharing", "[core][utils][irept]")
9393
REQUIRE(&irep.read() != &test_irep.read());
9494
REQUIRE(irep.id() != test_irep.id());
9595
}
96+
// the following would be desirable for irept to be safe, but we know it
97+
// presently does not hold; see #1855 for a proposed solution
98+
// THEN("Holding a reference to an operand should prevent sharing")
99+
// {
100+
// irept &operand = test_irep.get_sub()[0];
101+
// irept irep = test_irep;
102+
// REQUIRE(&irep.read() != &test_irep.read());
103+
// operand = irept(ID_0);
104+
// REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
105+
// }
96106
THEN("Changing an id should not prevent sharing")
97107
{
98108
test_irep.id(ID_0);
@@ -190,6 +200,16 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
190200
REQUIRE(&expr.read() != &test_expr.read());
191201
REQUIRE(expr.id() != test_expr.id());
192202
}
203+
// the following would be desirable for irept to be safe, but we know it
204+
// presently does not hold; see #1855 for a proposed solution
205+
// THEN("Holding a reference to an operand should prevent sharing")
206+
// {
207+
// exprt &operand = test_expr.op0();
208+
// exprt expr = test_expr;
209+
// REQUIRE(&expr.read() != &test_expr.read());
210+
// operand = exprt(ID_0);
211+
// REQUIRE(expr.op0().id() != test_expr.op0().id());
212+
// }
193213
THEN("Changing an id should not prevent sharing")
194214
{
195215
test_expr.id(ID_0);

0 commit comments

Comments
 (0)