@@ -68,58 +68,33 @@ void bv_endianness_mapt::build_big_endian(const typet &src)
68
68
endianness_mapt
69
69
bv_pointerst::endianness_map (const typet &type, bool little_endian) const
70
70
{
71
- return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width };
71
+ return bv_endianness_mapt{type, little_endian, ns, bv_width };
72
72
}
73
73
74
- std::size_t bv_pointerst::bv_pointers_widtht::
75
- operator ()(const typet &type) const
76
- {
77
- if (type.id () != ID_pointer)
78
- return boolbv_widtht::operator ()(type);
79
-
80
- // check or update the cache, just like boolbv_widtht does
81
- std::pair<cachet::iterator, bool > cache_result =
82
- cache.insert (std::pair<typet, entryt>(type, entryt ()));
83
-
84
- if (cache_result.second )
85
- {
86
- std::size_t &total_width = cache_result.first ->second .total_width ;
87
-
88
- total_width = get_address_width (to_pointer_type (type));
89
- DATA_INVARIANT (total_width > 0 , " pointer width shall be greater than zero" );
90
- }
91
-
92
- return cache_result.first ->second .total_width ;
93
- }
94
-
95
- std::size_t bv_pointerst::bv_pointers_widtht::get_object_width (
96
- const pointer_typet &type) const
74
+ std::size_t bv_pointerst::get_object_width (const pointer_typet &) const
97
75
{
98
76
// not actually type-dependent for now
99
- (void )type;
100
77
return config.bv_encoding .object_bits ;
101
78
}
102
79
103
- std::size_t bv_pointerst::bv_pointers_widtht::get_offset_width (
104
- const pointer_typet &type) const
80
+ std::size_t bv_pointerst::get_offset_width (const pointer_typet &type) const
105
81
{
106
82
const std::size_t pointer_width = type.get_width ();
107
83
const std::size_t object_width = get_object_width (type);
108
84
PRECONDITION (pointer_width >= object_width);
109
85
return pointer_width - object_width;
110
86
}
111
87
112
- std::size_t bv_pointerst::bv_pointers_widtht::get_address_width (
113
- const pointer_typet &type) const
88
+ std::size_t bv_pointerst::get_address_width (const pointer_typet &type) const
114
89
{
115
90
return type.get_width ();
116
91
}
117
92
118
93
bvt bv_pointerst::object_literals (const bvt &bv, const pointer_typet &type)
119
94
const
120
95
{
121
- const std::size_t offset_width = bv_pointers_width. get_offset_width (type);
122
- const std::size_t object_width = bv_pointers_width. get_object_width (type);
96
+ const std::size_t offset_width = get_offset_width (type);
97
+ const std::size_t object_width = get_object_width (type);
123
98
PRECONDITION (bv.size () >= offset_width + object_width);
124
99
125
100
return bvt (
@@ -129,7 +104,7 @@ bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
129
104
bvt bv_pointerst::offset_literals (const bvt &bv, const pointer_typet &type)
130
105
const
131
106
{
132
- const std::size_t offset_width = bv_pointers_width. get_offset_width (type);
107
+ const std::size_t offset_width = get_offset_width (type);
133
108
PRECONDITION (bv.size () >= offset_width);
134
109
135
110
return bvt (bv.begin (), bv.begin () + offset_width);
@@ -166,8 +141,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
166
141
bvt invalid_bv = object_literals (
167
142
encode (pointer_logic.get_invalid_object (), type), type);
168
143
169
- const std::size_t object_bits =
170
- bv_pointers_width.get_object_width (type);
144
+ const std::size_t object_bits = get_object_width (type);
171
145
172
146
bvt equal_invalid_bv;
173
147
equal_invalid_bv.reserve (object_bits);
@@ -240,8 +214,7 @@ bv_pointerst::bv_pointerst(
240
214
message_handlert &message_handler,
241
215
bool get_array_constraints)
242
216
: boolbvt(_ns, _prop, message_handler, get_array_constraints),
243
- pointer_logic(_ns),
244
- bv_pointers_width(_ns)
217
+ pointer_logic(_ns)
245
218
{
246
219
}
247
220
@@ -490,7 +463,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
490
463
count == 1 ,
491
464
" there should be exactly one pointer-type operand in a pointer-type sum" );
492
465
493
- const std::size_t offset_bits = bv_pointers_width. get_offset_width (type);
466
+ const std::size_t offset_bits = get_offset_width (type);
494
467
bvt sum = bv_utils.build_constant (0 , offset_bits);
495
468
496
469
forall_operands (it, plus_expr)
@@ -845,8 +818,8 @@ exprt bv_pointerst::bv_get_rec(
845
818
846
819
bvt bv_pointerst::encode (std::size_t addr, const pointer_typet &type) const
847
820
{
848
- const std::size_t offset_bits = bv_pointers_width. get_offset_width (type);
849
- const std::size_t object_bits = bv_pointers_width. get_object_width (type);
821
+ const std::size_t offset_bits = get_offset_width (type);
822
+ const std::size_t object_bits = get_object_width (type);
850
823
851
824
bvt zero_offset (offset_bits, const_literal (false ));
852
825
@@ -864,7 +837,7 @@ bvt bv_pointerst::offset_arithmetic(
864
837
const bvt &bv,
865
838
const mp_integer &x)
866
839
{
867
- const std::size_t offset_bits = bv_pointers_width. get_offset_width (type);
840
+ const std::size_t offset_bits = get_offset_width (type);
868
841
869
842
return offset_arithmetic (
870
843
type, bv, 1 , bv_utils.build_constant (x, offset_bits));
@@ -882,7 +855,7 @@ bvt bv_pointerst::offset_arithmetic(
882
855
index.type ().id ()==ID_signedbv?bv_utilst::representationt::SIGNED:
883
856
bv_utilst::representationt::UNSIGNED;
884
857
885
- const std::size_t offset_bits = bv_pointers_width. get_offset_width (type);
858
+ const std::size_t offset_bits = get_offset_width (type);
886
859
bv_index=bv_utils.extension (bv_index, offset_bits, rep);
887
860
888
861
return offset_arithmetic (type, bv, factor, bv_index);
@@ -904,7 +877,7 @@ bvt bv_pointerst::offset_arithmetic(
904
877
bv_index = bv_utils.signed_multiplier (index, bv_factor);
905
878
}
906
879
907
- const std::size_t offset_bits = bv_pointers_width. get_offset_width (type);
880
+ const std::size_t offset_bits = get_offset_width (type);
908
881
bv_index = bv_utils.sign_extension (bv_index, offset_bits);
909
882
910
883
bvt offset_bv = offset_literals (bv, type);
@@ -919,7 +892,7 @@ bvt bv_pointerst::add_addr(const exprt &expr)
919
892
std::size_t a=pointer_logic.add_object (expr);
920
893
921
894
const pointer_typet type = pointer_type (expr.type ());
922
- const std::size_t object_bits = bv_pointers_width. get_object_width (type);
895
+ const std::size_t object_bits = get_object_width (type);
923
896
const std::size_t max_objects=std::size_t (1 )<<object_bits;
924
897
925
898
if (a==max_objects)
0 commit comments