Change "violated assumption" to "assumption" in trace

[polgreen]

Assumptions aren't violated, they are adhered to

[allredj]

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

[smowton]

Does this apply to assert as well?

[polgreen]

No, that's the point. Assertions are violated, assumptions are not. Currently CBMC says that assumptions and assertions are violated

(if we actually are violating assumptions there are bigger problems, but that's not what's actually happening, it's just the output text that's misleading)

[smowton]

I mean, can you get an assert step in the trace that passes? The assumption seems like it would depend on where it occurs in the trace just like the assertion -- if it's in the middle, we passed the assertion/assumption, and if it's at the end we failed it?

[polgreen]

Asserts are handled by a different case in this switch statement. The case I have changed only handles goto_trace_stept::typet::ASSUME, and asserts are goto_trace_stept::typet::ASSERT.

The output for assertions is "violated property".

Non-failing assertions, that are located on a path to a failing assertion, simply don't appear in the trace

[polgreen]

I can't find any place where a __CPROVER_assert can end up being a goto_trace_stept::typet::ASSUME ? But if that does happen, and we have a trace where that __CPROVER_assert is somewhere in the middle and is not violated, it would still not be accurate to output "Violated assumption".

[polgreen]

actually the condition on this output needs to be fixed as well, this code should be outputted when an assumption is passed. If an assumption is violated, something really wrong has happened, and CBMC should show some kind of error messages, as that would be against the documented behaviour of __CPROVER_assume

[smowton]

Agreed, I think at present this code is unreachable.

[smowton]

Nb. a failing assumption won't generate an error, we'll just call it a successful verification, since assumptions holding ==> assertions passing (even if "assumptions holding" is trivially false)

[polgreen]

Yes, what I meant is you should never have a trace to a violated assertion in which there is a violated assumption. This code would only be reachable in the case where we were generating a trace, in which case that would mean a violated assertion and a violated assumption, which should definitely not ever happen.

[polgreen]

I have now made this code reachable. I think outputting assumptions in the traces is useful, although I guess that can be argued either way

[smowton]

Agreed re: assumptions. @kroening's call re: displaying passing assumptions in the trace I suppose. I suspect if we want to go for passing assumptions we'd also want to show passing / failing GOTOs in the same spirit (personally I think that would be quite useful,but matter of trace)

[allredj]

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

[polgreen]

@kroening ?

[polgreen]

Either this PR should be merged, or this unreachable code in CBMC should be removed:
https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/goto_trace.cpp#L323-L337

[martin-cs]

@polgreen I agree that one or the other should happen (I lean slightly towards your PR and having it print the correct thing) but I lack the code ownership to make it happen.

[tautschnig]

@polgreen This needs a rebase.

[polgreen]

rebased

[tautschnig]

Thanks @polgreen! Now clang-format is still unhappy and one regression test fails as it encodes a specific number of lines in the pattern being matched. I think that number now needs to be increased by 8, because the assumptions are printed. While at it, I am wondering whether there really should be two blank lines after each assumption? But that's just a visual detail.

[allredj]

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