cprover
/builddir/build/BUILD/cbmc-cbmc-5.10/doc/architectural/compilation-and-development.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \page compilation-and-development Compilation and Development
3 
4 \author Martin Brain, Peter Schrammel
5 
6 ## Makefiles ##
7 
8 First off, read the \ref cbmc-user-manual "CBMC User Manual". It describes
9 how to get, build and use CBMC. This document covers the
10 internals of the system and how to get started on development.
11 
12 ## CMake files ##
13 
14 To be documented.
15 
16 ## Personal configuration: config.inc, macro DEBUG ##
17 
18 To be documented.
19 
20 ## Running tests ##
21 
22 ### Regression tests ###
23 
24 The regression tests are contained in the `regression/` folder.
25 They are grouped into directories for each of the tools/modules.
26 Each of these contains multiple directories, each of which contains
27 input files and one or more`.desc` files that describe what command
28 to run, what output is expected and so on. There is a Perl script,
29 `test.pl` that is used to invoke the tests as:
30 
31  ../test.pl -c PATH_TO_CBMC
32 
33 The `–help` option gives instructions for use and the
34 format of the description files.
35 
36 To be documented further.
37 
38 ### Unit tests ###
39 
40 To be documented.
41 
42 ## Documentation ##
43 
44 Apart from the (user-orientated) CBMC user manual and this document, most
45 of the rest of the documentation is inline in the code as `doxygen` and
46 some comments. A man page for CBMC, goto-cc and goto-instrument is
47 contained in the `doc/` directory and gives some options for these
48 tools. All of these could be improved and patches are very welcome. In
49 some cases the algorithms used are described in the relevant papers.
50 
51 ## Accessing doxygen documentation ##
52 
53 The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
54 To build it locally, run `doxygen` in `/src`. HTML output will be created in
55 `/doc/html`. The index page is `/doc/html/index.html`.
56 
57 ## Coding standards ##
58 
59 See <a
60 href="https://github.com/diffblue/cbmc/blob/master/CODING_STANDARD.md">
61 `CODING_STANDARD.md`</a> file in the root of the CBMC repository.
62 
63 CPROVER is written in a fairly minimalist subset of C++; templates and
64 meta-programming are avoided except where necessary.
65 External library dependencies are avoided (only STL and a SAT solver
66 are required). Boost is not used. The `util` directory contains many
67 utilities that are not (yet) in the standard library.
68 
69 Patches should be formatted so that code is indented with two space
70 characters, not tab and wrapped to 80 columns. Headers for doxygen
71 should be given (and preferably filled!) and the author will be the
72 person who first created the file. Add doxygen comments to
73 undocumented functions as you touch them. Coding standards
74 and doxygen comments are enforced by CI before a patch can be
75 merged by running `clang-format` and `cpplint`.
76 
77 Identifiers should be lower case with underscores to separate words.
78 Types (classes, structures and typedefs) names must end with a `t`.
79 Types that model types (i.e. C types in the program that is being
80 interpreted) are named with `_typet`. For example `ui_message_handlert`
81 rather than `UI_message_handlert` or `UIMessageHandler` and
82 `union_typet`.