remove unused member_exprt::symbol()

[kroening]

Reverts d47d503; the method isn't used.

[tautschnig]

I'd suggest that the information included in the PR also makes it into the commit message.

[peterschrammel]

@thk123, this requires a TG bump.

[thk123]

Done: diffblue/test-gen#2217 - awaiting CI

[thk123]

Yeah turns out TG is using this - will fix up.

[thk123]

What's the motivation here? Not only is it not unused (this PR removes two uses) but it is non-trivial - it loops back up the expression tree to find the root symbol. It seems your replacements won't work for: a.b.c, previously would get a, now will crash.

Edit: In these cases it doesn't do seem to do anything useful - will see if the same is true in TG. If not, will make a static function in where it is used.

[tautschnig]

What's the motivation here?

It's just wrong. The root operand of a member_exprt need not be a symbol_exprt. (It could be a struct_exprt, a dereference_exprt, and possibly something else.)

Any current user of this method should use object_descriptor_exprt, use its .build(...), and then .root_object(). When I got to review this PR there hadn't been any edits to users, so I trusted the "it's unused." Otherwise I would have added the above guidance.

[thk123]

Thanks @tautschnig for the explanation. TG updated to use object_descriptor_exprt - and passed tests locally - will post when CI passes.

[kroening]

Does anyone know why cmake builds are unhappy?

[tautschnig]

Does anyone know why cmake builds are unhappy?

There are invariant failures in the unit tests. I suppose they should be rewritten in the way I described (using object_descriptor_exprt) rather than as currently done. I'm actually more concerned that it's only in cmake that unit tests fail...

[tautschnig]

See #2877 for the JBMC unit tests.

TG bump passing

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: 0099f74).
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

• the cbmc commit has disappeared in the mean time (e.g. in a force-push)
• the author is not in the list of contributors (e.g. first-time contributors).

[thk123]

This was updated after the bump passed and now causes TG to fail. Please hold off merging if you make substantial (e.g. interface) changes until the TG bump has been updated.

[tautschnig]

Hmm, sorry, I had understood #2860 (comment) as TG having been cleaned up.

[thk123]

@tautschnig Fair - it was, but CI was still failing on this PR. Then the changes to the unit test were applied (adding a symbol_tablet parameter to some test utilities) and this broke TG.

Annoyingly in GH there is no way to really see the diff between incremental revisions of a rebased PR (which would have shown the diff to be substantial enough to retest on TG).