Skip to content

Commit 3dfa46b

Browse files
committed
remove index_type()
This removes index_type(), and the last remaining user. The function has been deprecated since January 2022.
1 parent eaa2cdd commit 3dfa46b

File tree

3 files changed

+1
-10
lines changed

3 files changed

+1
-10
lines changed

src/goto-symex/shadow_memory_util.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -475,7 +475,7 @@ exprt compute_or_over_bytes(
475475
for(mp_integer index = 0; index < size; ++index)
476476
{
477477
extract_bytes_of_expr(
478-
index_exprt(expr, from_integer(index, index_type())),
478+
index_exprt(expr, from_integer(index, array_type.index_type())),
479479
field_type,
480480
ns,
481481
log,

src/util/c_types.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,6 @@ bitvector_typet c_index_type()
1919
return signed_size_type();
2020
}
2121

22-
bitvector_typet index_type()
23-
{
24-
return c_index_type();
25-
}
26-
2722
signedbv_typet signed_int_type()
2823
{
2924
signedbv_typet result(config.ansi_c.int_width);

src/util/c_types.h

-4
Original file line numberDiff line numberDiff line change
@@ -479,10 +479,6 @@ inline code_with_contract_typet &to_code_with_contract_type(typet &type)
479479
return static_cast<code_with_contract_typet &>(type);
480480
}
481481

482-
DEPRECATED(
483-
SINCE(2022, 1, 13, "use c_index_type() or array_typet::index_type() instead"))
484-
bitvector_typet index_type();
485-
486482
bitvector_typet c_index_type();
487483
signedbv_typet signed_int_type();
488484
unsignedbv_typet unsigned_int_type();

0 commit comments

Comments
 (0)