field_sensitivityt::get_fields: recurse on operands even when input is already L2

smowton · tautschnig · commit 8cd443cf14ee · 2019-04-16T11:55:44.000Z
For an L1 or lower expression, get_fields already recursed, e.g. to turn
`x` -&gt; `{ { x..a..g, x..a..h }, x..b }` rather than `{ x..a, a..b }`
when its `a` member is itself struct-typed. However this recursion was
omitted in the case where the input expression is already L2 renamed.
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
@@ -133,7 +133,10 @@ exprt field_sensitivityt::get_fields(
       tmp.remove_level_2();
       tmp.set_expression(member);
       if(was_l2)
-        result.add_to_operands(state.rename(tmp, ns).get());
+      {
+        result.add_to_operands(
+          state.rename(get_fields(ns, state, tmp), ns).get());
+      }
       else
         result.add_to_operands(get_fields(ns, state, tmp));
     }
@@ -162,7 +165,10 @@ exprt field_sensitivityt::get_fields(
       tmp.remove_level_2();
       tmp.set_expression(index);
       if(was_l2)
-        result.add_to_operands(state.rename(tmp, ns).get());
+      {
+        result.add_to_operands(
+          state.rename(get_fields(ns, state, tmp), ns).get());
+      }
       else
         result.add_to_operands(get_fields(ns, state, tmp));
     }
