Skip to content

Commit 7777ccd

Browse files
committed
Move check for bv size to flattening/ instead of ansi-c/
1 parent 8c5eae2 commit 7777ccd

File tree

3 files changed

+7
-12
lines changed

3 files changed

+7
-12
lines changed

regression/ansi-c/Issue_7104_Bv_Size/deref.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ deref.c
33

44
^EXIT=1$
55
^SIGNAL=0$
6-
only bitvectors of size multiple of 8 can be dereferenced
6+
only bitvectors of size multiple of 8 bits can be dereferenced
77
^CONVERSION ERROR$
88
--
99
--

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1805,17 +1805,6 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
18051805
error() << "dereferencing void pointer" << eom;
18061806
throw 0;
18071807
}
1808-
1809-
if(is_signed_or_unsigned_bitvector(expr.type()))
1810-
{
1811-
auto bv_type_width = to_bitvector_type(expr.type()).get_width();
1812-
if(bv_type_width % 8 != 0)
1813-
{
1814-
throw invalid_source_file_exceptiont{
1815-
"only bitvectors of size multiple of 8 can be dereferenced",
1816-
expr.source_location()};
1817-
}
1818-
}
18191808
}
18201809
else
18211810
{

src/solvers/flattening/boolbv_byte_extract.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
4040
}
4141

4242
const std::size_t width = boolbv_width(expr.type());
43+
if(width % 8 != 0)
44+
{
45+
throw invalid_source_file_exceptiont{
46+
"only bitvectors of size multiple of 8 bits can be dereferenced",
47+
expr.source_location()};
48+
}
4349

4450
// special treatment for bit-fields and big-endian:
4551
// we need byte granularity

0 commit comments

Comments
 (0)