Skip to content

Commit 5eb6fee

Browse files
committed
Dump-C: do not produce c_bit_field declarations
goto-program conversion may introduce temporaries of c_bit_field type. These, however, are not permitted outside structs in C. Instead, change their types to plain bitvector types to use `__CPROVER_bitvector[n]` syntax.
1 parent 2e0fcc8 commit 5eb6fee

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/goto-instrument/goto_program2code.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1435,6 +1435,15 @@ void goto_program2codet::cleanup_code(
14351435

14361436
if(code.op0().type().id()==ID_array)
14371437
cleanup_expr(to_array_type(code.op0().type()).size(), true);
1438+
else if(code.op0().type().id() == ID_c_bit_field)
1439+
{
1440+
c_bit_field_typet original_type = to_c_bit_field_type(code.op0().type());
1441+
bitvector_typet bv_type =
1442+
to_bitvector_type(original_type.underlying_type());
1443+
bv_type.set_width(original_type.get_width());
1444+
bv_type.remove(ID_C_c_type);
1445+
code.op0().type() = std::move(bv_type);
1446+
}
14381447

14391448
add_local_types(code.op0().type());
14401449

0 commit comments

Comments
 (0)