Adding extra information about invariant messages#2142
Adding extra information about invariant messages#2142danpoe merged 2 commits intodiffblue:developfrom
Conversation
tautschnig
left a comment
There was a problem hiding this comment.
Comments on some further refinement below, but guidance of this sorts is very useful!
CODING_STANDARD.md
Outdated
| - Avoid `assert`. If the condition is an actual invariant, use INVARIANT, | ||
| PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If | ||
| there are possible reasons why it might fail, throw an exception. | ||
| - Use "should" style statements for messages in invariants (e.g. "Array |
There was a problem hiding this comment.
While at it: should those messages start with a lowercase or an uppercase character?
There was a problem hiding this comment.
72 upper case vs. 100+ lower case so going with lower case.
CODING_STANDARD.md
Outdated
| PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If | ||
| there are possible reasons why it might fail, throw an exception. | ||
| - Use "should" style statements for messages in invariants (e.g. "Array | ||
| should have a non-zero size") to make it clear both the violation and the |
There was a problem hiding this comment.
I think it should be "to make clear both the violation ..." (drop "it")
There was a problem hiding this comment.
Opted for:
to make both the violation and the expected behavior clear
|
This seems to slightly clash with the documentation in |
|
Sorry lost the will on this one! Is the verdict |
|
I think the wording in |
f7a9150 to
3bf7d6c
Compare
|
@danpoe @tautschnig I've had a go at updating the |
tautschnig
left a comment
There was a problem hiding this comment.
Re-approving. Two wishlist items:
- As there now is some duplication of information, could you please add cross-referencing by mentioning invariant.h in CODING_STANDARD.md and vice-versa?
- The commit message "Update the invariant.cpp documentation to match" both seems to be incomplete (match what?) and refers to the wrong file (it's invariant.h).
src/util/invariant.h
Outdated
| ** | ||
| ** As well as the condition they have a text argument that should be | ||
| ** used to say why they are true. The reason should be a string literals. | ||
| ** used to say why they are true. The reason should be a string literals |
There was a problem hiding this comment.
Nit pick: s/literals/literal/
3bf7d6c to
43bfc73
Compare
allredj
left a comment
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 43bfc73).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86151309
Saw a couple of PRs getting comments relating to the grammatical style of invariant messages. I've added a clarification to the coding standard which reflects what I do and have seen others do so hopefully this isn't contentious!