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 [CPROVER User Manual](http://www.cprover.org/cprover-manual/) details the
61 capabilities of 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 following pages attempt to provide the information that a developer needs to
72 work on CBMC, in a sensible order. In many cases they link to the appropriate
73 class-level or module-level documentation.
75 * \subpage compilation-and-development
77 * \subpage background-concepts
79 * \subpage cbmc-architecture
81 * \subpage folder-walkthrough
83 * \subpage code-walkthrough
85 * \subpage other-tools
87 * The \subpage tutorial "CBMC Developer Tutorial" helps new contributors
88 to CProver to get their feet wet through a series of programming
89 exercises - mostly modifying goto-instrument, and thus learning to
90 manipulate the main data structures used within CBMC.
92 For higher-level architectural information, each of the pages under
93 the <a href="modules.html">Modules</a>
94 link gives an overview of a directory in the CProver codebase.
96 If you already know exactly what you're looking for, the best place
97 to look is the API reference, which
98 is generated from the codebase. You can search for classes and class
99 members in the search bar at top-right or use one of the links in the
102 \defgroup module_hidden _hidden