cprover
|
First off, read the CBMC User Manual. It describes how to get, build and use CBMC. This document covers the internals of the system and how to get started on development.
To be documented.
To be documented.
The regression tests are contained in the regression/
folder. They are grouped into directories for each of the tools/modules. Each of these contains multiple directories, each of which contains input files and one or more<tt>.desc files that describe what command to run, what output is expected and so on. There is a Perl script, test.pl
that is used to invoke the tests as:
../test.pl -c PATH_TO_CBMC
The –help
option gives instructions for use and the format of the description files.
To be documented further.
To be documented.
Apart from the (user-orientated) CBMC user manual and this document, most of the rest of the documentation is inline in the code as doxygen
and some comments. A man page for CBMC, goto-cc and goto-instrument is contained in the doc/
directory and gives some options for these tools. All of these could be improved and patches are very welcome. In some cases the algorithms used are described in the relevant papers.
The doxygen documentation can be accessed online. To build it locally, run doxygen
in /src
. HTML output will be created in /doc/html
. The index page is /doc/html/index.html
.
See CODING_STANDARD.md
file in the root of the CBMC repository.
CPROVER is written in a fairly minimalist subset of C++; templates and meta-programming are avoided except where necessary. External library dependencies are avoided (only STL and a SAT solver are required). Boost is not used. The util
directory contains many utilities that are not (yet) in the standard library.
Patches should be formatted so that code is indented with two space characters, not tab and wrapped to 80 columns. Headers for doxygen should be given (and preferably filled!) and the author will be the person who first created the file. Add doxygen comments to undocumented functions as you touch them. Coding standards and doxygen comments are enforced by CI before a patch can be merged by running clang-format
and cpplint
.
Identifiers should be lower case with underscores to separate words. Types (classes, structures and typedefs) names must end with a t
. Types that model types (i.e. C types in the program that is being interpreted) are named with _typet
. For example ui_message_handlert
rather than UI_message_handlert
or UIMessageHandler
and union_typet
.