fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

[kroening]

This fixes a segfault in ebmc -- this may even be worth a position in a whitepaper on test generation!

[peterschrammel]

bool operator<(
  const mini_bdd_mgrt::reverse_keyt &x,
  const mini_bdd_mgrt::reverse_keyt &y)

[peterschrammel]

if(x.var<y.var)
  return true;

etc

[peterschrammel]

Do we have a test case that exhibits the problem?

[mgudemann]

BDD2, BDD3 and BDD5 in `regression/ebmc` fail without this

…

On 27 June 2017 at 11:10, Peter Schrammel ***@***.***> wrote: Do we have a test case that exhibits the problem? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1062 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACeHTDrKwy7Um3k7GY0-SKckK2wOyqqNks5sIMcVgaJpZM4OF71x> .

[tautschnig]

BDD2, BDD3 and BDD5 in regression/ebmc fail without this

Are these now routinely run in some Travis set up?

What about enabling/reviving unit/miniBDD.cpp? I don't think any bug fix without an accompanying regression test should get merged as no-one will understand what has gone wrong.

[tautschnig]

Apart from various minor comments: there needs to be some convincing regression test story. If the regression test is run in some non-public repository then that's better than nothing, but really the regression test should live with the repository holding the source here.

[tautschnig]

Why is this changed to a friend rather than being a member?

[mgudemann]

Apart from various minor comments: there needs to be some convincing regression test story. If the regression test is run in some non-public repository then that's better than nothing, but really the regression test should live with the repository holding the source here. > }; + friend bool operator<(const reverse_keyt &, const reverse_keyt &); + Why is this changed to a `friend` rather than being a member?

This is just the literal revert of the change that caused the problem. It is very well possible to do the fix with a member function.

[mgudemann]

Michael Tautschnig <[email protected]> writes:

> BDD2, BDD3 and BDD5 in `regression/ebmc` fail without this Are these now routinely run in some Travis set up?

not yet, but hopefully will be soon

[tautschnig]

This is just the literal revert of the change that caused the problem. It is very well possible to do the fix with a member function.

I wasn't quite aware that I had broken this in 61f747d. Note to self: do not mix unrelated changes, because they will escape code review...

[kroening]

Now uses a friend.

[tautschnig]

The linter warnings are to be addressed; but adding some sort of test appears to be most important.

[kroening]

An attempt has been made to add a test; the sad result is that this one gets stuck on the fixed variant as well, suggesting that there's still some bug, either in miniBDD, or in the test.

[tautschnig]

Thank you for adding this test! How about reviving the previous unit test to see whether some very basic operations at least succeed?

[kroening]

Success! The test now passes on the fixed version, and fails on the previous one.

[tautschnig]

Thank you for adding this test! Could the linter please be made happy or, where appropriate, be silenced?

[kroening]

Done. Note that this has required a change to util/invariant.h.

[tautschnig]

Looks good to me!