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

byte_extract lowering: ensure type consistency 

Make sure we construct concatenations that are type consistent.
This commit is contained in:
Michael Tautschnig 2019-02-03 15:46:22 +00:00
parent f4ed82aa8e
commit a3d77e6ac0
2 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -343,8 +343,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
return simplify_expr(typecast_exprt(op.front(), src.type()), ns);
else // width_bytes>=2
{
concatenation_exprt concatenation(std::move(op), src.type());
return simplify_expr(concatenation, ns);
concatenation_exprt concatenation(
std::move(op), bitvector_typet(subtype.id(), width_bytes * 8));
return simplify_expr(
typecast_exprt(std::move(concatenation), src.type()), ns);
}
}

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

@ -104,8 +104,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
constant_exprt size = from_integer(8, size_type());
std::vector<typet> types = {
// struct_typet({{"comp1", u16}, {"comp2", u16}}),
// struct_typet({{"comp1", u32}, {"comp2", u64}}),
struct_typet({{"comp1", u16}, {"comp2", u16}}),
struct_typet({{"comp1", u32}, {"comp2", u64}}),
#if 0
// not currently handled: components not byte aligned
struct_typet({{"comp1", u32},
@ -114,8 +114,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
{"comp2", u8}}),
#endif
// union_typet({{"compA", u32}, {"compB", u64}}),
// c_enum_typet(u16),
// c_enum_typet(unsignedbv_typet(128)),
c_enum_typet(u16),
c_enum_typet(unsignedbv_typet(128)),
// array_typet(u8, size),
// array_typet(s32, size),
// array_typet(u64, size),
@ -193,10 +193,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
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);
// TODO: does not currently hold
// REQUIRE(lower_be_s == r);
REQUIRE(lower_be == r);
REQUIRE(lower_be_s == r);
}
}
}