@@ -3,10 +3,22 @@ Here a few minimalistic coding rules for the CPROVER source tree.
33Whitespaces:
44- Use 2 spaces indent, no tabs.
55- No lines wider than 80 chars.
6+ - When line is wider, do the following:
7+ - Subsequent lines should be indented two more than the initial line
8+ - Break after = if it is part of an assignment
9+ - For chained calls, prefer immediately before .
10+ - For other operators (e.g. &&, +) prefer immediately after the operator
11+ - For brackets, break after the bracket
12+ - In the case of function calls, put each argument on a separate line if
13+ they do not fit after one line break
614- If a method is bigger than 50 lines, break it into parts.
715- Put matching { } into the same column.
8- - No spaces around operators, except &&, ||, and <<
9- - Spaces after , and ; inside 'for'
16+ - No spaces around operators (=, +, ==, ...)
17+ Exceptions: Spaces around &&, || and <<
18+ - Space after comma (parameter lists, argument lists, ...)
19+ - Space after colon inside 'for'
20+ - No whitespaces at end of line
21+ - No whitespaces in blank lines
1022- Put argument lists on next line (and ident 2 spaces) if too long
1123- Put parameters on separate lines (and ident 2 spaces) if too long
1224- No whitespaces around colon for inheritance,
@@ -16,8 +28,6 @@ Whitespaces:
1628- if(...), else, for(...), do, and while(...) are always in a separate line
1729- Break expressions in if, for, while if necessary and align them
1830 with the first character following the opening parenthesis
19- - No whitespaces at end of line
20- - Avoid whitespaces in blank lines
2131- Use {} instead of ; for the empty statement
2232- Single line blocks without { } are allowed,
2333 but put braces around multi-line blocks
@@ -29,9 +39,31 @@ Comments:
2939- Do not use /* */ except for file and function comment blocks
3040- Each source and header file must start with a comment block
3141 stating the Module name and Author [will be changed when we roll out doxygen]
32- - Each function in the source file (not the header) is preceded
33- by a comment block stating Name, Inputs, Outputs and Purpose [will be changed
34- when we roll out doxygen]
42+ - Each function in the source file (not the header) is preceded
43+ by a function comment header consisting of a comment block stating
44+ Name, Inputs, Outputs and Purpose [will be changed when we roll
45+ out doxygen]
46+ - It should look like this:
47+ ```
48+ /*******************************************************************\
49+
50+ Function: class_namet::function_name
51+
52+ Inputs:
53+ arg_name - Description of its purpose
54+ long_arg_name - Descriptions should be indented
55+ to match the first line of the
56+ description
57+
58+ Outputs: A description of what the function returns
59+
60+ Purpose: A description of what the function does.
61+ Again, indentation with the line above
62+
63+ \*******************************************************************/
64+ ```
65+ - An empty line should appear between the bottom of the function comment header
66+ and the function.
3567- Put comments on a separate line
3668- Use comments to explain the non-obvious
3769- Use #if 0 for commenting out source code
@@ -51,6 +83,8 @@ Naming:
5183
5284Header files:
5385- Avoid unnecessary #includes, especially in header files
86+ - Prefer forward declaration to includes, but forward declare at the top
87+ of the header file rather than in line
5488- Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc
5589
5690C++ features:
@@ -85,6 +119,9 @@ C++ features:
85119- We allow to use 3rd-party libraries directly.
86120 No wrapper matching the coding rules is required.
87121 Allowed libraries are: STL.
122+ - Use the auto keyword if and only if one of the following
123+ - The type is explictly repeated on the RHS (e.g. a constructor call)
124+ - Adding the type will increase confusion (e.g. iterators, function pointers)
88125
89126Architecture-specific code:
90127- Avoid if possible.
0 commit comments