@@ -244,11 +244,14 @@ static assignmentt rewrite_with_to_field_symbols(
244
244
// / expression by assignments to just those fields. May generate "with" (or
245
245
// / "update") expressions, which \ref rewrite_with_to_field_symbols will then
246
246
// / take care of.
247
+ // / \tparam use_update: use update_exprt instead of with_exprt when building
248
+ // / expressions that modify components of an array or a struct
247
249
// / \param [in, out] state: symbolic execution state to perform renaming
248
250
// / \param assignment: assignment to transform
249
251
// / \param ns: namespace
250
252
// / \param do_simplify: set to true if, and only if, simplification is enabled
251
253
// / \return updated assignment
254
+ template <bool use_update>
252
255
static assignmentt shift_indexed_access_to_lhs (
253
256
goto_symext::statet &state,
254
257
assignmentt assignment,
@@ -285,31 +288,38 @@ static assignmentt shift_indexed_access_to_lhs(
285
288
if (byte_extract.id () == ID_index)
286
289
{
287
290
index_exprt &idx = to_index_expr (byte_extract);
288
-
289
- #ifdef USE_UPDATE
290
- update_exprt new_rhs{idx.array (), exprt{}, ssa_rhs};
291
- new_rhs.designator ().push_back (index_designatort{idx.index ()});
292
- #else
293
- with_exprt new_rhs{idx.array (), idx.index (), ssa_rhs};
294
- #endif
295
-
296
- ssa_rhs = new_rhs;
291
+ ssa_rhs = [&]() -> exprt {
292
+ if (use_update)
293
+ {
294
+ update_exprt new_rhs{idx.array (), exprt{}, ssa_rhs};
295
+ new_rhs.designator ().push_back (index_designatort{idx.index ()});
296
+ return std::move (new_rhs);
297
+ }
298
+ else
299
+ return with_exprt{idx.array (), idx.index (), ssa_rhs};
300
+ }();
297
301
byte_extract = idx.array ();
298
302
}
299
303
else
300
304
{
301
305
member_exprt &member = to_member_expr (byte_extract);
302
306
const irep_idt &component_name = member.get_component_name ();
303
-
304
- #ifdef USE_UPDATE
305
- update_exprt new_rhs{member.compound (), exprt{}, ssa_rhs};
306
- new_rhs.designator ().push_back (member_designatort{component_name});
307
- #else
308
- with_exprt new_rhs (member.compound (), exprt (ID_member_name), ssa_rhs);
309
- new_rhs.where ().set (ID_component_name, component_name);
310
- #endif
311
-
312
- ssa_rhs = new_rhs;
307
+ ssa_rhs = [&]() -> exprt {
308
+ if (use_update)
309
+ {
310
+ update_exprt new_rhs{member.compound (), exprt{}, ssa_rhs};
311
+ new_rhs.designator ().push_back (
312
+ member_designatort{component_name});
313
+ return std::move (new_rhs);
314
+ }
315
+ else
316
+ {
317
+ with_exprt new_rhs (
318
+ member.compound (), exprt (ID_member_name), ssa_rhs);
319
+ new_rhs.where ().set (ID_component_name, component_name);
320
+ return std::move (new_rhs);
321
+ }
322
+ }();
313
323
byte_extract = member.compound ();
314
324
}
315
325
}
@@ -377,7 +387,7 @@ void symex_assignt::assign_non_struct_symbol(
377
387
// introduced by assign_struct_member, are transformed into member
378
388
// expressions on the LHS. If we add an option to disable field-sensitivity
379
389
// in the future these should be omitted.
380
- auto assignment = shift_indexed_access_to_lhs (
390
+ auto assignment = shift_indexed_access_to_lhs< use_update ()> (
381
391
state, assignmentt{lhs, std::move (l2_rhs)}, ns, symex_config.simplify_opt );
382
392
assignment = rewrite_with_to_field_symbols<use_update ()>(
383
393
state, std::move (assignment), ns);
0 commit comments