Skip to content

Adds documentation about function contracts #6185

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.

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

Merged
merged 1 commit into from
Jun 18, 2021

Conversation

feliperodri
Copy link
Collaborator

@feliperodri feliperodri commented Jun 17, 2021

Related to #6149.

Signed-off-by: Felipe R. Monteiro [email protected]

Adds a section about "Function Contracts" to the CPROVER manual.

  • 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.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • 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.

@feliperodri feliperodri added aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts labels Jun 17, 2021
@feliperodri feliperodri self-assigned this Jun 17, 2021
@codecov
Copy link

codecov bot commented Jun 17, 2021

Codecov Report

Merging #6185 (4b66d29) into develop (0002950) will increase coverage by 8.22%.
The diff coverage is n/a.

❗ Current head 4b66d29 differs from pull request most recent head 4f80ed1. Consider uploading reports for the commit 4f80ed1 to get more accurate results
Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6185      +/-   ##
===========================================
+ Coverage    67.40%   75.62%   +8.22%     
===========================================
  Files         1157     1454     +297     
  Lines        95236   160922   +65686     
===========================================
+ Hits         64197   121705   +57508     
- Misses       31039    39217    +8178     
Flag Coverage Δ
cproversmt2 ?
regression ?
unit ?

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/util/string_container.cpp 52.94% <0.00%> (-47.06%) ⬇️
src/solvers/prop/prop.cpp 42.85% <0.00%> (-41.76%) ⬇️
src/solvers/flattening/boolbv_member.cpp 53.65% <0.00%> (-38.65%) ⬇️
src/cpp/cpp_storage_spec.cpp 65.00% <0.00%> (-35.00%) ⬇️
src/util/cmdline.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/array_pool.h 66.66% <0.00%> (-33.34%) ⬇️
src/solvers/strings/string_refinement.h 66.66% <0.00%> (-33.34%) ⬇️
...rs/strings/string_concatenation_builtin_function.h 0.00% <0.00%> (-33.34%) ⬇️
src/cbmc/c_test_input_generator.cpp 60.00% <0.00%> (-30.33%) ⬇️
src/ansi-c/anonymous_member.cpp 66.66% <0.00%> (-25.34%) ⬇️
... and 1433 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2e3ba57...4f80ed1. Read the comment docs.

@@ -0,0 +1,502 @@
# Function Contracts
Copy link
Contributor

Choose a reason for hiding this comment

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

Overall comment: this file contains too much "how" and not enough "what". We do not need to explain the implementations of ASSIGNS and is_fresh, but we should explain what they do, perhaps using examples. Also, my thought is that there should be a page for each construct (similar to a reference manual) with examples that demonstrate how the construct works. So, I'd like to see some refactoring, and a few more examples of how the constructs work.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I've re-write and re-sctructured the documentation to highlight "what" instead of "how" and added more examples.

Copy link
Contributor

@SaswatPadhi SaswatPadhi left a comment

Choose a reason for hiding this comment

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

Couple of initial comments

@diffblue diffblue deleted a comment from SaswatPadhi Jun 18, 2021
@feliperodri feliperodri marked this pull request as ready for review June 18, 2021 05:25
@feliperodri feliperodri requested a review from markrtuttle June 18, 2021 05:28
Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

Thank you! Documentation patches are very welcome!

__CPROVER_old(*identifier*)
```

Refers to the value of a given object in the pre-state of a function within the
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can it also be used for loops?

Copy link
Contributor

Choose a reason for hiding this comment

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

Not yet, but we have an intern working on this, so hopefully soon 🙂

@@ -0,0 +1,43 @@
# Quantifiers
Copy link
Collaborator

Choose a reason for hiding this comment

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

Would it be possible to add something about the impact this has on the choice of back-end and that depending on how they are used, it may be necessary to use an SMT solver.

Copy link
Contributor

Choose a reason for hiding this comment

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

+1. Thanks for pointing this out!
We had planned to do this (#6149). Let's make the changes as part of this PR.

@feliperodri feliperodri requested a review from SaswatPadhi June 18, 2021 14:16
@feliperodri feliperodri force-pushed the doc-contracts branch 2 times, most recently from 9f74394 to 811995a Compare June 18, 2021 19:12
@feliperodri feliperodri force-pushed the doc-contracts branch 3 times, most recently from a2047bd to 14555a4 Compare June 18, 2021 20:03
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue left a comment

Choose a reason for hiding this comment

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

Thats a massive, and fantastic, addition to the docs - many thanks!

@feliperodri feliperodri merged commit 523622a into diffblue:develop Jun 18, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
aws Bugs or features of importance to AWS CBMC users Code Contracts Function and loop contracts
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants