CBMC documentation

[ylevhariamzn]

CBMC version: 5.87
Operating system: Rocky red hat
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

I am a new user to CBMC in AWS (verifying boot code for various HW that we are developing), I am using the documentation quite frequently, but there are just too much sources, some are not that consistent, I would really appreciate a central (working) documentation set with more examples, I would like to push this tool in my SW team.

[rod-chapman]

I agree and sympathize with Joseph. For example, we have
http://www.cprover.org/cprover-manual/
and
https://diffblue.github.io/cbmc/
and
https://model-checking.github.io/cbmc-training/index.html

Which one of these is actually up-to-date? (Answer: none of them!)
The first of these is particularly confusing, since it appears to be obsolete, but is still the first hit you get from Google in response to the query "cmbc manual". That's a problem.

We really need a documentation set (a user manual, reference manual, a beginner's tutorial) that are always consistent, up-to-date, and formally tagged to correspond to a particular toolset release.

[thomasspriggs]

The first google result for me when searching "cbmc documentation" is https://diffblue.github.io/cbmc/ This site is generated by git hub actions when PRs are merged to the develop branch. So the website is up to date with the latest documentation source as it stands in the develop branch. As we do releases once every two weeks, the generated documentation may be up to two weeks ahead of the latest release. This is in the case where the documentation source has been updated in the same PR as user facing features are changed, as is best practice. This site may be behind current release in cases where updating the documentation in line with the features has been missed. Such instances need to be identified before they can be fixed.

The user guide is here - https://diffblue.github.io/cbmc/user_guide.html
The reference manual is here - https://diffblue.github.io/cbmc/reference_guide.html
The tutorial is here - https://diffblue.github.io/cbmc/cprover-manual/md_cbmc_tutorial.html

If there are specific instances where the https://diffblue.github.io/cbmc/ site is out of date these should be raised as issues or as fix PRs on this CBMC repository.

The http://www.cprover.org/cprover-manual/ is out of date and IMHO should be taken down and replaced with a forwarding link to the https://diffblue.github.io/cbmc/ site.

The https://model-checking.github.io/cbmc-training/index.html website is a separate documentation website written by individuals within AWS. It is not part of the cbmc repository and the commit history does not show contributions from those within Diffblue. The source for this website can be found here - https://github.com/model-checking/cbmc-training

[rod-chapman]

"As we do releases once every two weeks, the generated documentation may be up to two weeks ahead of the latest release. This is in the case where the documentation source has been updated in the same PR as user facing features are changed, as is best practice."

A bit of digging around in GitHub shows that the "develop" branch of
https://github.com/diffblue/cbmc/tree/develop/doc/doxygen-root
has not had a substantial change for 6 months or more.

Apart from minor typos, https://github.com/diffblue/cbmc/tree/develop/src/goto-instrument/contracts/doc/user has not seen a substantial update for 9 months.

This does not fill me with confidence. Am I looking at the right branch?

[thomasspriggs]

"As we do releases once every two weeks, the generated documentation may be up to two weeks ahead of the latest release. This is in the case where the documentation source has been updated in the same PR as user facing features are changed, as is best practice."

A bit of digging around in GitHub shows that the "develop" branch of https://github.com/diffblue/cbmc/tree/develop/doc/doxygen-root has not had a substantial change for 6 months or more.

Apart from minor typos, https://github.com/diffblue/cbmc/tree/develop/src/goto-instrument/contracts/doc/user has not seen a substantial update for 9 months.

This does not fill me with confidence. Am I looking at the right branch?

The output HTML and web page resources are stored in https://github.com/diffblue/cbmc/tree/gh-pages
Note that this includes both the documentation from the separate /doc sub directory and the documentation which is generated from the doxygen comments in the source files.

As I haven't been working on the contracts support myself, I cannot comment on the number of documentation updates which have been made vs the number of user facing changes which have been made for it.