1 CProver Developer Documentation
4 These pages contain user tutorials, automatically-generated API
5 documentation, and higher-level architectural overviews for the
6 CProver codebase. CProver is a platform for software verification. Users can
7 download CProver tools from the <a href="http://www.cprover.org/">CProver
8 website</a>; contributors should use the
9 <a href="https://github.com/diffblue/cbmc">repository</a> hosted on GitHub. CBMC
12 CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99,
13 most of C11 and most compiler extensions provided by gcc and Visual Studio. It
14 also supports SystemC using Scoot. It allows verifying array bounds (buffer
15 overflows), pointer safety, arithmetic exceptions and user-specified assertions.
16 Furthermore, it can check C and C++ for consistency with other languages, such
17 as Verilog. The verification is performed by unwinding the loops in the program
18 and passing the resulting equation to a decision procedure.
20 For further information see [cprover.org](http://www.cprover.org/cbmc).
25 Get the [latest release](https://github.com/diffblue/cbmc/releases)
26 * Releases are tested and for production use.
28 Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
29 * Develop versions are not recommended for production use.
34 If you encounter a problem please file a bug report:
35 * Create an [issue](https://github.com/diffblue/cbmc/issues)
37 Contributing to the code base
38 =============================
40 1. Fork the the CBMC repository on GitHub.
41 2. Clone your fork with `git clone git@github.com:YOURNAME/cbmc.git`
42 3. Create a branch from the `develop` branch (default branch)
43 4. Make your changes - follow the
44 <a href="https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md">
46 5. Push your changes to your branch
47 6. Create a Pull Request targeting the `develop` branch
52 <a href="https://github.com/diffblue/cbmc/blob/develop/LICENSE">4-clause BSD
55 Overview of Documentation
60 * The \ref cbmc-user-manual "CBMC User Manual" details the capabilities of
61 CBMC and describes how to install and use these tools. It
62 also covers the underlying theory and prerequisite concepts behind how
65 * There is a helpful user tutorial on the wiki with lots of linked resources,
66 you can access it <a href=
67 "https://svn.cprover.org/wiki/doku.php?id=cprover_tutorial">here</a>.
71 * The \subpage cprover-architecture-overview "CProver Architecture Overview"
72 is a single document describing the layout of the codebase and many of the
73 important data structures. It probably contains more information than the
74 module pages at the moment, but may be somewhat out-of-date.
76 * For higher-level architectural information, each of the pages under
77 the <a href="modules.html">Modules</a>
78 link gives an overview of a directory in the CProver codebase.
80 * If you already know exactly what you're looking for, the API reference
81 is generated from the codebase. You can search for classes and class
82 members in the search bar at top-right or use one of the links in the
85 * The \subpage tutorial "CBMC Developer Tutorial" helps new contributors
86 to CProver to get their feet wet through a series of programming
87 exercises - mostly modifying goto-instrument, and thus learning to
88 manipulate the main data structures used within CBMC.
90 \defgroup module_hidden _hidden