From d24e63f018c04de12a6240e88fa4c91511fadf1c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sun, 3 Feb 2019 15:23:54 +0000 Subject: [PATCH] byte_extract lowering over arrays: fix bits vs bytes error The offset is computed in bits. --- src/solvers/lowering/byte_operators.cpp | 2 +- unit/solvers/lowering/byte_operators.cpp | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 07c47675870..33f680a4dfb 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -246,7 +246,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) { plus_exprt new_offset( unpacked.offset(), - from_integer(i * (*element_width), unpacked.offset().type())); + from_integer(i * (*element_width) / 8, unpacked.offset().type())); byte_extract_exprt tmp(unpacked); tmp.type()=subtype; diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 63ffaa87406..da1a770dea0 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -116,9 +116,9 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") // union_typet({{"compA", u32}, {"compB", u64}}), c_enum_typet(u16), c_enum_typet(unsignedbv_typet(128)), - // array_typet(u8, size), - // array_typet(s32, size), - // array_typet(u64, size), + array_typet(u8, size), + array_typet(s32, size), + array_typet(u64, size), unsignedbv_typet(24), unsignedbv_typet(128), signedbv_typet(24),