remove bitwise_neg(mp_integer)

[kroening]

The semantics of this operation is highly machine-dependent, and thus, it's
difficult to use. The single user is replaced by xor -1.

• Each commit message has a non-empty body, explaining why the change was made.
• My contribution is formatted in line with CODING_STANDARD.md.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• 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).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[tautschnig]

Ok, but I do wonder whether it would be more suitable for the interpreter to turn the mp_integer into a bitvector, then do the operation on a bitvector, and turn the result back into an mp_integer. (But that would apply to all bit operations, not just the one touched here.)

[kroening]

You mean bitvector as in vector<bool>?

[tautschnig]

You mean bitvector as in vector<bool>?

No, I was thinking of result = simplify(bitnot_exprt(from_integer(value, type)), ns);

[kroening]

Ah; well, there's an entirely different interpreter that just uses simplify(). That could directly apply to expressions at the top-level, without the need to even split by expression.

[tautschnig]

Ah; well, there's an entirely different interpreter that just uses simplify(). That could directly apply to expressions at the top-level, without the need to even split by expression.

Maybe that's all that should be done? What's the point of the current implementation?

[kroening]

Another option is to the use parts of path-based symex that aren't symbolic.

[kroening]

(which in turn uses simplify()).

[allredj]

Passed Diffblue compatibility checks (cbmc commit: d22e9b9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/87102220