cprover
/builddir/build/BUILD/cbmc-cbmc-5.11/doc/architectural/front-page.md
Go to the documentation of this file.
1 CProver Developer Documentation
2 =====================
3 
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
10 is part of CProver.
11 
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.
19 
20 For further information see [cprover.org](http://www.cprover.org/cbmc).
21 
22 Versions
23 ========
24 
25 Get the [latest release](https://github.com/diffblue/cbmc/releases)
26 * Releases are tested and for production use.
27 
28 Get the current *develop* version: `git clone https://github.com/diffblue/cbmc.git`
29 * Develop versions are not recommended for production use.
30 
31 Report bugs
32 ===========
33 
34 If you encounter a problem please file a bug report:
35 * Create an [issue](https://github.com/diffblue/cbmc/issues)
36 
37 Contributing to the code base
38 =============================
39 
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">
45 coding guidelines</a>
46 5. Push your changes to your branch
47 6. Create a Pull Request targeting the `develop` branch
48 
49 License
50 =======
51 
52 <a href="https://github.com/diffblue/cbmc/blob/develop/LICENSE">4-clause BSD
53 license</a>.
54 
55 Overview of Documentation
56 =======
57 
58 ### For users:
59 
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
63  these tools work.
64 
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>.
68 
69 ### For contributors:
70 
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.
74 
75 * \subpage compilation-and-development
76 
77 * \subpage background-concepts
78 
79 * \subpage cbmc-architecture
80 
81 * \subpage folder-walkthrough
82 
83 * \subpage code-walkthrough
84 
85 * \subpage other-tools
86 
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.
91 
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.
95 
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
100 sidebar.
101 
102 \defgroup module_hidden _hidden