6 These pages contain user tutorials, automatically-generated API
7 documentation, and higher-level architectural overviews for the
8 CProver codebase. Users can download CProver tools from the
9 <a href="http://www.cprover.org/">CProver website</a>; contributors
10 should use the <a href="https://github.com/diffblue/cbmc">repository</a>
15 * The \ref cprover-manual "CProver Manual" details the capabilities of
16 CBMC and SATABS and describes how to install and use these tools. It
17 also covers the underlying theory and prerequisite concepts behind how
22 * If you already know exactly what you're looking for, the API reference
23 is generated from the codebase. You can search for classes and class
24 members in the search bar at top-right or use one of the links in the
27 * For higher-level architectural information, each of the pages under
28 the "Modules" link in the sidebar gives an overview of a directory in
31 * The \ref module_cbmc "CBMC guided tour" is a good start for new
32 contributors to CBMC. It describes the stages through which CBMC
33 transforms source files into bug reports and counterexamples, linking
34 to the relevant documentation for each stage.
36 * The \subpage cbmc-hacking "CBMC hacking HOWTO" helps new contributors
37 to CProver to get their feet wet through a series of programming
38 exercises---mostly modifying goto-instrument, and thus learning to
39 manipulate the main data structures used within CBMC.
41 * The \subpage cbmc-guide "CBMC guide" is a single document describing
42 the layout of the codebase and many of the important data structures.
43 It probably contains more information than the module pages at the
44 moment, but may be somewhat out-of-date.
46 \defgroup module_hidden _hidden