Skip to content

Initial additional information about the invariant macros and hierarchy. #3388

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
Merged
merged 1 commit into from
Nov 19, 2018
Merged

Initial additional information about the invariant macros and hierarchy. #3388

merged 1 commit into from
Nov 19, 2018

Conversation

sonodtt
Copy link
Contributor

@sonodtt sonodtt commented Nov 13, 2018

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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.

Initial additional information about the invariant macros and hierarchy.

peterschrammel
peterschrammel approved these changes Nov 13, 2018
View reviewed changes
src/util/invariant.h Outdated
@@ -82,6 +82,9 @@ Author: Martin Brain, [email protected]
/// family of macros, allowing constructs like
/// `INVARIANT(x==y, my_invariantt, (T1)actual1, (T2)actual2, ...)`
///
/// \ref invariant_failedt is also the base class of any 'structured
/// exceptions' - as found in file base_exceptions.h
Copy link
Member

Choose a reason for hiding this comment

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

\ref base_exceptions.h

tautschnig
tautschnig reviewed Nov 14, 2018
View reviewed changes
src/util/invariant.h Outdated
@@ -196,6 +199,9 @@ std::string get_backtrace();

void report_exception_to_stderr(const invariant_failedt &);

/// This class is the backbone of all the invariant types. Every instance of an
/// invariant is ultimately generated by this class, which is at times called
/// via a wrapper function.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I am not sure this comment is in the right place? It's now part of the documentation of a method, not a class?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes - whoops! Function.

src/util/invariant.h Outdated
@@ -230,8 +236,9 @@ CBMC_NORETURN
abort();
}

/// Takes a backtrace, constructs an invariant_violatedt from reason and the
/// backtrace, aborts printing the invariant's description.
/// This is a wrapper class used by the macro 'INVARIANT(CONDITION, REASON)'
Copy link
Collaborator

Choose a reason for hiding this comment

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

Again, I am wondering whether this is in the right place - it's documenting a method, but talks about a class?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Argh! Fixed.

src/util/invariant.h Outdated
@@ -342,6 +349,8 @@ std::string assemble_diagnostics(Diagnostics &&... args)
}
} // namespace detail


/// This is a wrapper class, used by the macro 'INVARIANT_WITH_DIAGNOSTICS'
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should it just be "wrapper function"?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes. Function.

@sonodtt sonodtt force-pushed the doc-day-cprover-invariant-extra-comments branch from 6a6b304 to def20b5 Compare November 15, 2018 14:19
@peterschrammel
Copy link
Member

@sonodtt, can you fix the overlong lines please: https://travis-ci.org/diffblue/cbmc/jobs/455518975#L493

@sonodtt sonodtt force-pushed the doc-day-cprover-invariant-extra-comments branch from def20b5 to 250255f Compare November 16, 2018 07:52
@peterschrammel
Copy link
Member

@sonodtt, clang-format is still complaining: https://travis-ci.org/diffblue/cbmc/jobs/455856034#L536

@sonodtt sonodtt force-pushed the doc-day-cprover-invariant-extra-comments branch from 250255f to 6717df3 Compare November 16, 2018 14:27
allredj
allredj reviewed Nov 16, 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: 6717df3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/91681970

@sonodtt sonodtt merged commit df5e3b8 into diffblue:develop Nov 19, 2018
@sonodtt sonodtt deleted the doc-day-cprover-invariant-extra-comments branch November 19, 2018 14:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig left review comments

@allredj allredj allredj left review comments

@peterschrammel peterschrammel peterschrammel approved these changes

@xbauch xbauch xbauch approved these changes

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

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

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@sonodtt sonodtt

Labels
documentation
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@sonodtt @peterschrammel @tautschnig @xbauch @allredj @chrisr-diffblue