Do not artificially separate message handler and uit

[tautschnig]

They were passed around independently, even though they originated from the very
same object.

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: 31e6b52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77146181
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).

[tautschnig]

FWIW: this is an API change, and will thus a need for adjusting TG is expected. Or at least that's what I hope the reported TG failure is about.

[peterschrammel]

@thk123, can you create a TG bump for this, please?

[thk123]

Started - though could use some guidance on exactly how to apply this. For example, we have:

cbmc_solverst cbmc_solvers(bmc_options, symbol_table, sub_solver_out);

sub_solver_out is either a message_handlert or a null_message_handlert (decided by a define) and not entirely trivial for me to change either to be a ui_message_handlert. What is the purpose of this, why does cbmc_solverst have a tight dependency on what output to use?

[tautschnig]

What is the purpose of this, why does cbmc_solverst have a tight dependency on what output to use?

That's a fair question, and I've got another commit in #2310 (f578d33) that removes the unused ui information from string refinement.(done in #2542) What isn't done yet is completely removing it from refinement, but that would be a functional change, not only cleanup.

With regard to guidance: In your current set-up, somehow you must be picking a ui despite just having a message_handlert or null_message_handlert. So whatever selects this ui should be investigated, because it problably has a ui_message_handlert. If it doesn't, then you've genuinely decoupled the message handler from the ui configuration, which seems broken to me.

[peterschrammel]

Rebased and TG bump created.

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: eefad58).
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).

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: 8eb05f7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84891985
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).

TG bump passes

[peterschrammel]

@kroening, that's ready to merge.

[kroening]

I would need a bit more background on this one. What makes me nervous is that there's now ui_message_handler inside goto-cc, which doesn't intend to do any xml or json output, or interact with any UI.

[tautschnig]

What makes me nervous is that there's now ui_message_handler inside goto-cc, which doesn't intend to do any xml or json output, or interact with any UI.

The console equally is a user interface, isn't it?

[peterschrammel]

ui_message_handlert was already inside goto-cc through gcc_message_handlert and console_message_handlert.

[kroening]

Ah, we are anyway trying to get rid of language_uit.

[peterschrammel]

Ah, we are anyway trying to get rid of language_uit.

Is this an 'approve'?

Edit: #2980 needs to be merged first, then rebase.

[kroening]

The new include seems to be spurious?

[tautschnig]

I'm afraid it isn't, this file uses std::unique_ptr, which previously worked as it was transitively included via message handler includes.

[kroening]

After rebasing to #2980, the changes in goto-cc should no longer be necessary. The rest is fine!

[allredj]

This PR failed Diffblue compatibility checks (cbmc commit: 0c8b108).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85486179
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).