replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

byte_extract lowering: lower newly introduced byte_extract expressions 

byte_extract lowering must not return any further byte_extract expressions.
This commit is contained in:
Michael Tautschnig 2019-02-03 15:24:51 +00:00
parent ccd97d4f2c
commit 1f94bceb73
2 changed files with 3 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/solvers/lowering/byte_operators.cpp
View File

@ -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)

5
unit/solvers/lowering/byte_operators.cpp
View File

@ -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);