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 * \subpage compilation-and-development
73 * \subpage background-concepts
75 * \subpage cbmc-architecture
77 * \subpage folder-walkthrough
79 * \subpage data-structures-core-structures-and-ast
81 * \subpage data-structures-from-ast-to-goto-program
83 * \subpage front-end-languages-generating-codet-from-multiple-languages
87 * \subpage symbolic-executors
89 * \subpage solvers-infrastructure
91 * \subpage static-analysis-apis
93 * \subpage other-tools
95 * For higher-level architectural information, each of the pages under
96 the <a href="modules.html">Modules</a>
97 link gives an overview of a directory in the CProver codebase.
99 * If you already know exactly what you're looking for, the API reference
100 is generated from the codebase. You can search for classes and class
101 members in the search bar at top-right or use one of the links in the
104 * The \subpage tutorial "CBMC Developer Tutorial" helps new contributors
105 to CProver to get their feet wet through a series of programming
106 exercises - mostly modifying goto-instrument, and thus learning to
107 manipulate the main data structures used within CBMC.
109 \defgroup module_hidden _hidden