cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/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 \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
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 * \subpage compilation-and-development
72 
73 * \subpage background-concepts
74 
75 * \subpage cbmc-architecture
76 
77 * \subpage folder-walkthrough
78 
79 * \subpage data-structures-core-structures-and-ast
80 
81 * \subpage data-structures-from-ast-to-goto-program
82 
83 * \subpage front-end-languages-generating-codet-from-multiple-languages
84 
85 * \subpage bmct-class
86 
87 * \subpage symbolic-executors
88 
89 * \subpage solvers-infrastructure
90 
91 * \subpage static-analysis-apis
92 
93 * \subpage other-tools
94 
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.
98 
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
102  sidebar.
103 
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.
108 
109 \defgroup module_hidden _hidden