Comment on and clarify field-sensitivity-specific expression transformations

smowton · tautschnig · commit 1708b9057597 · 2019-03-29T14:59:45.000Z
The function name was previously incorrect (it did more than it said),
so now I just call both transformations from symex_assign.
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
@@ -291,7 +291,6 @@ static void rewrite_with_to_field_symbols(
 /// \param ns: namespace
 /// \param do_simplify: set to true if, and only if, simplification is enabled
 static void shift_indexed_access_to_lhs(
-  goto_symext::statet &state,
   exprt &ssa_rhs,
   ssa_exprt &lhs_mod,
   const namespacet &ns,
@@ -358,8 +357,6 @@ static void shift_indexed_access_to_lhs(
       lhs_mod = to_ssa_expr(byte_extract);
     }
   }
-
-  rewrite_with_to_field_symbols(state, ssa_rhs, lhs_mod, ns);
 }
 
 void goto_symext::symex_assign_symbol(
@@ -383,8 +380,13 @@ void goto_symext::symex_assign_symbol(
 
   ssa_exprt lhs_mod = lhs;
 
-  shift_indexed_access_to_lhs(
-    state, l2_rhs, lhs_mod, ns, symex_config.simplify_opt);
+  // Note the following two calls are specifically required for
+  // field-sensitivity. For example, with-expressions, which may have just been
+  // introduced by symex_assign_struct_member, are transformed into member
+  // expressions on the LHS. If we add an option to disable field-sensitivity
+  // in the future these should be omitted.
+  shift_indexed_access_to_lhs(l2_rhs, lhs_mod, ns, symex_config.simplify_opt);
+  rewrite_with_to_field_symbols(state, l2_rhs, lhs_mod, ns);
 
   do_simplify(l2_rhs);
 
