|
1 |
| -Here a few minimalistic coding rules for the cprover source tree: |
2 |
| - |
3 |
| -a) 2 spaces indent, no tabs |
4 |
| -b) no "using namespace std;" |
5 |
| -c) Avoid new/delete, use containers instead. |
6 |
| -d) Avoid unnecessary #includes, especially in header files |
7 |
| -e) No lines wider than 80 chars |
8 |
| -f) Put matching { } into the same column |
9 |
| -g) If a method is bigger than a page, break it into parts |
10 |
| -h) Avoid destructive updates if possible. The irept has |
11 |
| - constant time copy. |
| 1 | +Here a few minimalistic coding rules for the CPROVER source tree. |
| 2 | + |
| 3 | +Whitespaces: |
| 4 | +- Use 2 spaces indent, no tabs. |
| 5 | +- No lines wider than 80 chars. |
| 6 | +- If a method is bigger than 50 lines, break it into parts. |
| 7 | +- Put matching { } into the same column. |
| 8 | +- No spaces around operators, except &&, ||, and << |
| 9 | +- Spaces after , and ; inside 'for' |
| 10 | +- Put argument lists on next line (and ident 2 spaces) if too long |
| 11 | +- Put parameters on separate lines (and ident 2 spaces) if too long |
| 12 | +- No whitespaces around colon for inheritance, |
| 13 | + put inherited into separate lines in case of multiple inheritance |
| 14 | +- The initializer list follows the constructor without a whitespace |
| 15 | + around the colon. Break line after the colon if required and indent members. |
| 16 | +- if(...), else, for(...), do, and while(...) are always in a separate line |
| 17 | +- Break expressions in if, for, while if necessary and align them |
| 18 | + with the first character following the opening parenthesis |
| 19 | +- No whitespaces at end of line |
| 20 | +- Avoid whitespaces in blank lines |
| 21 | +- Use {} instead of ; for the empty statement |
| 22 | +- Single line blocks without { } are allowed, |
| 23 | + but put braces around multi-line blocks |
| 24 | +- Use blank lines to visually separate logically cohesive code blocks |
| 25 | + within a function |
| 26 | +- Have a newline at the end of a file |
| 27 | + |
| 28 | +Comments: |
| 29 | +- Do not use /* */ except for file and function comment blocks |
| 30 | +- Each source and header file must start with a comment block |
| 31 | + 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] |
| 35 | +- Put comments on a separate line |
| 36 | +- Use comments to explain the non-obvious |
| 37 | +- Use #if 0 for commenting out source code |
| 38 | +- Use #ifdef DEBUG to guard debug code |
| 39 | + |
| 40 | +Naming: |
| 41 | +- Identifiers may use the characters [a-z0-9_] and should start with a |
| 42 | + lower-case letter (parameters in constructors may start with _). |
| 43 | +- Use american spelling for identifiers. |
| 44 | +- Separate basic words by _ |
| 45 | +- Avoid abbreviations (e.g. prefer symbol_table to of st). |
| 46 | +- User defined type identifiers have to be terminated by 't'. Moreover, |
| 47 | + before 't' may not be '_'. |
| 48 | +- Do not use 'm_' prefix nor '_' suffix for names of attributes of structured |
| 49 | + types. |
| 50 | +- Enum values may use the characters [A-Z0-9_] |
| 51 | + |
| 52 | +Header files: |
| 53 | +- Avoid unnecessary #includes, especially in header files |
| 54 | +- Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc |
| 55 | + |
| 56 | +C++ features: |
| 57 | +- Do not use namespaces. |
| 58 | +- Prefer use of 'typedef' insted of 'using'. |
| 59 | +- Prefer use of 'class' instead of 'struct'. |
| 60 | +- Write type modifiers before the type specifier. |
| 61 | +- Make references const whenever possible |
| 62 | +- Make functions const whenever possible |
| 63 | +- Do not hide base class functions |
| 64 | +- You are encouraged to use override |
| 65 | +- Single argument constructors must be explicit |
| 66 | +- Avoid implicit conversions |
| 67 | +- Avoid friend declarations |
| 68 | +- Avoid iterators, use ranged for instead |
| 69 | +- Avoid allocation with new/delete, use unique_ptr |
| 70 | +- Avoid pointers, use references |
| 71 | +- Avoid char *, use std::string |
| 72 | +- For numbers, use int, unsigned, long, unsigned long, double |
| 73 | +- Use mp_integer, not BigInt |
| 74 | +- Use the functions in util for conversions between numbers and strings |
| 75 | +- Avoid C-style functions. Use classes with an operator() instead. |
| 76 | +- Use irep_idt for identifiers (not std::string) |
| 77 | +- Avoid destructive updates if possible. The irept has constant time copy. |
| 78 | +- Use instances of std::size_t for comparison with return values of .size() of |
| 79 | + STL containers and algorithms, and use them as indices to arrays or vectors. |
| 80 | +- Do not use default values in public functions |
| 81 | +- Use assertions to detect programming errors, e.g. whenever you make |
| 82 | + assumptions on how your code is used |
| 83 | +- Use exceptions only when the execution of the program has to abort |
| 84 | + because of erroneous user input |
| 85 | +- We allow to use 3rd-party libraries directly. |
| 86 | + No wrapper matching the coding rules is required. |
| 87 | + Allowed libraries are: STL. |
12 | 88 |
|
13 | 89 | Architecture-specific code:
|
| 90 | +- Avoid if possible. |
| 91 | +- Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures. |
| 92 | +- Don't include architecture-specific header files without #ifdef ... |
| 93 | + |
| 94 | +Output: |
| 95 | +- Do not output to cout or cerr directly (except in temporary debug code, |
| 96 | + and then guard #include <iostream> by #ifdef DEBUG) |
| 97 | +- Derive from messaget if the class produces output and use the streams provided |
| 98 | + (status(), error(), debug(), etc) |
| 99 | +- Use '\n' instead of std::endl |
14 | 100 |
|
15 |
| -a) Avoid if possible. |
16 |
| -b) Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures. |
17 |
| -c) Don't include architecture-specific header files without #ifdef ... |
| 101 | +You are allowed to break rules if you have a good reason to do so. |
0 commit comments