A decision_proceduret isn't a messaget [blocks: #3800] #4042

tautschnig · 2019-02-03T01:09:38Z

Some derived classes may want to generate output, but then it's safe for them to
be messaget's.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
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).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

tautschnig · 2019-02-03T02:13:49Z

I guess this needs a genuine update to TG as there are some API changes required. The message handler that may now be needed should be available wherever those functions are invoked.

peterschrammel · 2019-02-04T00:10:08Z

src/goto-symex/symex_target_equation.cpp

 {
  try
  {
-    convert_guards(prop_conv);
-    convert_assignments(prop_conv);
+    convert_guards(prop_conv, message_handler);


Can you add a messaget log member to reduce the churn?

I could do, but then the constructor would need to take a message_handlert (as constructing a messaget without a message_handlert is deprecated). Does that seem reasonable?

@peterschrammel I have done as you suggested - I think it's thanks to your goto-checker refactoring that this was a fairly smooth sailing.

romainbrenguier

Needs a rebase. Otherwise looks good, but I'm waiting for tests result to give approval.

romainbrenguier · 2019-02-06T12:59:54Z

src/solvers/prop/prop_conv.h

@@ -67,7 +68,7 @@ class prop_convt:public decision_proceduret

 /*! \brief TO_BE_DOCUMENTED
 */
-class prop_conv_solvert:public prop_convt
+class prop_conv_solvert : public prop_convt, public messaget


ideally the inheritance should be removed here as well (could be done in a separate PR)

Yes, I am going to do so in a separate PR. I just wanted to keep the churn as small as possible.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

romainbrenguier · 2019-03-05T15:52:38Z

Half of the CI checks on TG were passing when I made the pull request (the other half didn't start for some reason), I can't check it now because the build is not working for other reasons, but I wouldn't block this PR for that

tautschnig · 2019-03-05T15:57:07Z

Thanks @romainbrenguier! This is still in need of review anyway, but I'll remove the TG-approval label for now.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 46a8930).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103243408
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.

allredj · 2019-03-06T15:24:15Z

src/util/decision_procedure.h

@@ -12,11 +12,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_DECISION_PROCEDURE_H
 #define CPROVER_UTIL_DECISION_PROCEDURE_H

-#include "message.h"
+#include <iosfwd>
+#include <string>


Not sure why these are needed.

decision_procedure_text returns a std::string and print_assignment takes a std::ostream as parameter. (Previously both includes were dragged in by message.h.)

allredj

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

Some derived classes may want to generate output, but then it's safe for them to be messaget's.

allredj

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

tautschnig added the cleanup label Feb 3, 2019

tautschnig requested review from allredj, chrisr-diffblue, kroening, martin-cs, peterschrammel, pkesseli, romainbrenguier and smowton as code owners February 3, 2019 01:09

allredj reviewed Feb 3, 2019

View reviewed changes

tautschnig assigned thk123, peterschrammel and romainbrenguier Feb 3, 2019

tautschnig changed the title ~~A decision_proceduret isn't a messaget~~ A decision_proceduret isn't a messaget [blocks: #3800] Feb 3, 2019

tautschnig added the blocker label Feb 3, 2019

peterschrammel reviewed Feb 4, 2019

View reviewed changes

romainbrenguier reviewed Feb 6, 2019

View reviewed changes

romainbrenguier approved these changes Feb 6, 2019

View reviewed changes

romainbrenguier assigned tautschnig and unassigned romainbrenguier Feb 6, 2019

tautschnig force-pushed the decision_proceduret-no-messaget branch 2 times, most recently from 4851c79 to dc3c08c Compare February 7, 2019 08:29

tautschnig assigned kroening and chrisr-diffblue and unassigned tautschnig Feb 7, 2019

allredj reviewed Feb 7, 2019

View reviewed changes

tautschnig force-pushed the decision_proceduret-no-messaget branch 2 times, most recently from c0c8514 to d933332 Compare February 7, 2019 20:42

tautschnig requested a review from danpoe as a code owner February 7, 2019 20:42

tautschnig requested a review from hannes-steffenhagen-diffblue as a code owner February 7, 2019 20:42

tautschnig force-pushed the decision_proceduret-no-messaget branch 3 times, most recently from 22160c3 to 3530bc8 Compare February 14, 2019 17:31

allredj reviewed Feb 14, 2019

View reviewed changes

tautschnig added the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Feb 21, 2019

tautschnig removed the Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers label Mar 5, 2019

tautschnig force-pushed the decision_proceduret-no-messaget branch from 3530bc8 to 46a8930 Compare March 5, 2019 16:02

allredj reviewed Mar 5, 2019

View reviewed changes

allredj approved these changes Mar 6, 2019

View reviewed changes

peterschrammel approved these changes Mar 6, 2019

View reviewed changes

peterschrammel assigned tautschnig and unassigned peterschrammel Mar 6, 2019

tautschnig force-pushed the decision_proceduret-no-messaget branch from 46a8930 to 4d8662f Compare March 6, 2019 23:39

allredj reviewed Mar 7, 2019

View reviewed changes

A decision_proceduret isn't a messaget

ab09a6c

Some derived classes may want to generate output, but then it's safe for them to be messaget's.

tautschnig force-pushed the decision_proceduret-no-messaget branch from 4d8662f to ab09a6c Compare March 7, 2019 07:04

tautschnig unassigned thk123, kroening and chrisr-diffblue Mar 7, 2019

tautschnig merged commit 133c096 into diffblue:develop Mar 7, 2019

tautschnig deleted the decision_proceduret-no-messaget branch March 7, 2019 08:34

allredj reviewed Mar 7, 2019

View reviewed changes

A decision_proceduret isn't a messaget [blocks: #3800] #4042

A decision_proceduret isn't a messaget [blocks: #3800] #4042

Uh oh!

Conversation

tautschnig commented Feb 3, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Feb 3, 2019

Uh oh!

peterschrammel Feb 4, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 4, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 7, 2019

Choose a reason for hiding this comment

Uh oh!

romainbrenguier left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier Feb 6, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Feb 7, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

romainbrenguier commented Mar 5, 2019

Uh oh!

tautschnig commented Mar 5, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj Mar 6, 2019

Choose a reason for hiding this comment

Uh oh!

tautschnig Mar 6, 2019

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!