From 1f94bceb739eaa8d8bda419d74a961f6a5d7d8dc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Feb 2019 15:24:51 +0000 Subject: [PATCH] byte_extract lowering: lower newly introduced byte_extract expressions byte_extract lowering must not return any further byte_extract expressions. --- src/solvers/lowering/byte_operators.cpp | 2 +- unit/solvers/lowering/byte_operators.cpp | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 44a130302b3..458611533aa 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -289,7 +289,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) tmp.type()=comp.type(); tmp.offset()=new_offset; - s.add_to_operands(std::move(tmp)); + s.add_to_operands(lower_byte_extract(tmp, ns)); } if(!failed) diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index e7b00a91c69..a79d0c4012f 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -162,9 +162,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") const exprt lower_be = lower_byte_extract(be, ns); const exprt lower_be_s = simplify_expr(lower_be, ns); - // TODO: does not currently hold - // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian)); - // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian)); + REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian)); + REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian)); REQUIRE(lower_be.type() == be.type()); // TODO: does not currently hold // REQUIRE(lower_be == r);