Move goto_statet and framet to their own files [blocks: #4302]

[romainbrenguier]

No functional changes.

• Each commit message has a non-empty body, explaining why the change was made.
• [na] Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• [na] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• [na] Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• [na] My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

It's probably a good idea, but also doesn't seem particularly urgent to me. Several existing PRs conflict with the changes proposed here, and rebasing with code moving between files is really painful. I'll thus refrain from approving until those other PRs have been merged.

[romainbrenguier]

@tautschnig

It's probably a good idea, but also doesn't seem particularly urgent to me. Several existing PRs conflict with the changes proposed here, and rebasing with code moving between files is really painful. I'll thus refrain from approving until those other PRs have been merged.

Can we make a list of these PRs, so that we wait for them, and try to get the new coming ones rebased on this?

I only had this one #3986, but I prefer to delay it and wait for this change.

[tautschnig]

Can we make a list of these PRs, so that we wait for them, and try to get the new coming ones rebased on this?

It's probably incomplete, but https://github.com/diffblue/cbmc/pulls?utf8=%E2%9C%93&q=is%3Apr+is%3Aopen++label%3A%22Symbolic+Execution%22+ is a starting point.

[romainbrenguier]

It's probably incomplete, but https://github.com/diffblue/cbmc/pulls?utf8=%E2%9C%93&q=is%3Apr+is%3Aopen++label%3A%22Symbolic+Execution%22+ is a starting point.

A lot of pull request there do not touch goto_symex_state.h so are not relevant.
A search for "goto_symex_statet" only gave 4 pull requests https://github.com/diffblue/cbmc/pulls?utf8=%E2%9C%93&q=is%3Apr+is%3Aopen+%22goto_symex_statet%22+ but I couldn't find how to make github search for file names.

[allredj]

✔️
Passed Diffblue compatibility checks (cbmc commit: 016ca57).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102655038

[tautschnig]

A lot of pull request there do not touch goto_symex_state.h so are not relevant.

Yes, but your list is definitively incomplete, so we've got an over-approximation and an under-approximation.

All I'm asking for is awareness and some care. Awareness for the impact of changes being proposed.

[tautschnig]

@romainbrenguier This can probably go in as one of the next commits, but it does need a rebase. (Any reference to safe_pointers needs to be removed from the new goto_state.h.)

[allredj]

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 3bce5c2).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103008022
Status will be re-evaluated on next push.
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).

• the compatibility was already broken by an earlier merge.