@@ -291,7 +291,6 @@ static void rewrite_with_to_field_symbols(
291
291
// / \param ns: namespace
292
292
// / \param do_simplify: set to true if, and only if, simplification is enabled
293
293
static void shift_indexed_access_to_lhs (
294
- goto_symext::statet &state,
295
294
exprt &ssa_rhs,
296
295
ssa_exprt &lhs_mod,
297
296
const namespacet &ns,
@@ -358,8 +357,6 @@ static void shift_indexed_access_to_lhs(
358
357
lhs_mod = to_ssa_expr (byte_extract);
359
358
}
360
359
}
361
-
362
- rewrite_with_to_field_symbols (state, ssa_rhs, lhs_mod, ns);
363
360
}
364
361
365
362
void goto_symext::symex_assign_symbol (
@@ -383,8 +380,13 @@ void goto_symext::symex_assign_symbol(
383
380
384
381
ssa_exprt lhs_mod = lhs;
385
382
386
- shift_indexed_access_to_lhs (
387
- state, l2_rhs, lhs_mod, ns, symex_config.simplify_opt );
383
+ // Note the following two calls are specifically required for
384
+ // field-sensitivity. For example, with-expressions, which may have just been
385
+ // introduced by symex_assign_struct_member, are transformed into member
386
+ // expressions on the LHS. If we add an option to disable field-sensitivity
387
+ // in the future these should be omitted.
388
+ shift_indexed_access_to_lhs (l2_rhs, lhs_mod, ns, symex_config.simplify_opt );
389
+ rewrite_with_to_field_symbols (state, l2_rhs, lhs_mod, ns);
388
390
389
391
do_simplify (l2_rhs);
390
392
0 commit comments