@@ -115,12 +115,12 @@ assigns_clauset::conditional_address_ranget::conditional_address_ranget(
115
115
generate_new_symbol (" __car_valid" , bool_typet(), location).symbol_expr()),
116
116
lower_bound_address_var(generate_new_symbol(
117
117
" __car_lb" ,
118
- guarded_slice.start_adress .type(),
118
+ guarded_slice.start_address .type(),
119
119
location)
120
120
.symbol_expr()),
121
121
upper_bound_address_var(generate_new_symbol(
122
122
" __car_ub" ,
123
- guarded_slice.start_adress .type(),
123
+ guarded_slice.start_address .type(),
124
124
location)
125
125
.symbol_expr())
126
126
{
@@ -158,10 +158,10 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions(
158
158
auto validity_check_expr =
159
159
check_target_validity == check_target_validityt::YES_ALLOW_NULL
160
160
? or_exprt{not_exprt{clean_guard},
161
- null_pointer (guarded_slice.start_adress ),
162
- w_ok_exprt{guarded_slice.start_adress , guarded_slice.size }}
161
+ null_pointer (guarded_slice.start_address ),
162
+ w_ok_exprt{guarded_slice.start_address , guarded_slice.size }}
163
163
: or_exprt{not_exprt{clean_guard},
164
- w_ok_exprt{guarded_slice.start_adress , guarded_slice.size }};
164
+ w_ok_exprt{guarded_slice.start_address , guarded_slice.size }};
165
165
166
166
if (check_target_validity != check_target_validityt::NO)
167
167
{
@@ -185,23 +185,23 @@ assigns_clauset::conditional_address_ranget::generate_snapshot_instructions(
185
185
validity_condition_var,
186
186
simplify_expr (
187
187
and_exprt{clean_guard,
188
- not_exprt{null_pointer (guarded_slice.start_adress )}},
188
+ not_exprt{null_pointer (guarded_slice.start_address )}},
189
189
parent.ns ),
190
190
location_no_checks));
191
191
192
192
instructions.add (
193
193
goto_programt::make_decl (lower_bound_address_var, location_no_checks));
194
194
195
195
instructions.add (goto_programt::make_assignment (
196
- lower_bound_address_var, guarded_slice.start_adress , location_no_checks));
196
+ lower_bound_address_var, guarded_slice.start_address , location_no_checks));
197
197
198
198
instructions.add (
199
199
goto_programt::make_decl (upper_bound_address_var, location_no_checks));
200
200
201
201
instructions.add (goto_programt::make_assignment (
202
202
upper_bound_address_var,
203
203
simplify_expr (
204
- plus_exprt{guarded_slice.start_adress , guarded_slice.size }, parent.ns ),
204
+ plus_exprt{guarded_slice.start_address , guarded_slice.size }, parent.ns ),
205
205
location_no_checks));
206
206
207
207
// The snapshot assignments involve only instrumentation variables
@@ -277,7 +277,7 @@ exprt assigns_clauset::generate_inclusion_check(
277
277
if (allow_null_target == check_target_validityt::YES_ALLOW_NULL)
278
278
return false_exprt{};
279
279
else
280
- return null_pointer (lhs.guarded_slice .start_adress );
280
+ return null_pointer (lhs.guarded_slice .start_address );
281
281
}
282
282
283
283
exprt::operandst conditions;
@@ -297,7 +297,7 @@ exprt assigns_clauset::generate_inclusion_check(
297
297
298
298
if (allow_null_target == check_target_validityt::YES_ALLOW_NULL)
299
299
return or_exprt{
300
- null_pointer (lhs.guarded_slice .start_adress ),
300
+ null_pointer (lhs.guarded_slice .start_address ),
301
301
and_exprt{lhs.validity_condition_var , disjunction (conditions)}};
302
302
else
303
303
return and_exprt{lhs.validity_condition_var , disjunction (conditions)};
0 commit comments