Delay printing playback harness until after verification status

[YoshikiTakashima]

Description of changes:

Delay printing of harness until the verification status message is printed.

Resolved issues:

Resolves #2462

Call-outs:

Again, not familiar with testing this feature, so feel free to suggest any improvements on that front.

Testing:

• How is this change tested? tests/ui/concrete-playback/message-order

• Is this a refactor change? No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[jaisnan]

Have you tried running concrete playback with --inplace. Does the behavior of pasting the unit test into the source get impacted by this change? Even if it's not, I think it would be good to have a few regression tests with inplace just so we know the impact.

[YoshikiTakashima]

Good pt. I don't think so, but let me write another test to be sure.

[celinval]

May I suggest a different approach? Can you move the call to gen_and_add_concrete_playback() to harness_runner module instead of call_cbmc. We need to make sure that call is made after the result was rendered.

[YoshikiTakashima]

@celinval I can do that. The inputs to gen_and_add_concrete_playback() will need to move into the VerificationResults to be available but that might be cleaner.?

[YoshikiTakashima]

@celinval thanks for the suggestion. This was way easier, no change to VerificationResult required.

[YoshikiTakashima]

Should be good to go.

@jaisnan The similar tests to what you requested seem to have merged as part of #2464 and #2477

[celinval]

Awesome! Thanks