Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adding extra information about invariant messages #2142

Merged
merged 2 commits into from
Sep 27, 2018
Merged

Adding extra information about invariant messages #2142

merged 2 commits into from
Sep 27, 2018

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented May 1, 2018

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!

tautschnig
tautschnig approved these changes May 1, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Comments on some further refinement below, but guidance of this sorts is very useful!

CODING_STANDARD.md Outdated
@@ -188,6 +188,10 @@ Formatting is enforced using clang-format. For more information about this, see
- 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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While at it: should those messages start with a lowercase or an uppercase character?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

72 upper case vs. 100+ lower case so going with lower case.

CODING_STANDARD.md Outdated
@@ -188,6 +188,10 @@ Formatting is enforced using clang-format. For more information about this, see
- 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
should have a non-zero size") to make it clear both the violation and the
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it should be "to make clear both the violation ..." (drop "it")

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Opted for:

to make both the violation and the expected behavior clear

@danpoe
Copy link
Contributor

danpoe commented May 1, 2018

This seems to slightly clash with the documentation in invariant.cpp which says that the message should state the reason for why it holds. For example something like "array has non-zero size as it was checked by the caller". Whatever style we choose, we should probably update the documentation in invariant.cpp as well.

@danpoe danpoe mentioned this pull request May 4, 2018
Merged
@thk123
Copy link
Contributor Author

thk123 commented May 15, 2018

Sorry lost the will on this one! Is the verdict invariant.cpp should be updated to match the wording proposed in this PR? I believe the wording I proposed more closely matches how we use them: to document coders assumptions rather than the invariant.cpp wording which hopes for precisely known invariants.

@tautschnig
Copy link
Collaborator

I think the wording in invariant.cpp should be updated, because aspects like "was checked by the caller" are expressed by using a PRECONDITION (while a DATA_INVARIANT should hold by construction).

@thk123 thk123 force-pushed the docs/invariant-message branch from f7a9150 to 3bf7d6c Compare May 30, 2018 09:00
@thk123
Copy link
Contributor Author

thk123 commented May 30, 2018

@danpoe @tautschnig I've had a go at updating the invariant.h file, let me know what you think.

tautschnig
tautschnig approved these changes May 30, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
@@ -22,10 +22,18 @@ Author: Martin Brain, [email protected]
** evaluate to a boolean.
**
** 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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit pick: s/literals/literal/

@danpoe danpoe mentioned this pull request Sep 20, 2018
Merged
@tautschnig
Copy link
Collaborator

@thk123 @danpoe as this has come up in #2963: could this PR please be revisited and merged ASAP?

danpoe
danpoe approved these changes Sep 20, 2018 •
edited
Loading
View reviewed changes
@danpoe danpoe force-pushed the docs/invariant-message branch from 3bf7d6c to 43bfc73 Compare September 27, 2018 12:26
@thk123 thk123 requested a review from pkesseli as a code owner September 27, 2018 12:26
allredj
allredj reviewed Sep 27, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@danpoe danpoe merged commit 974a0e3 into diffblue:develop Sep 27, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@danpoe danpoe danpoe approved these changes

@chrisr-diffblue chrisr-diffblue chrisr-diffblue approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@smowton smowton Awaiting requested review from smowton

@pkesseli pkesseli Awaiting requested review from pkesseli

Assignees

@thk123 thk123

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@thk123 @danpoe @tautschnig @allredj @chrisr-diffblue