Here a few minimalistic coding rules for the CPROVER source tree. Whitespaces: - Use 2 spaces indent, no tabs. - No lines wider than 80 chars. - When line is wider, do the following: - Subsequent lines should be indented two more than the initial line - Break after = if it is part of an assignment - For chained calls, prefer immediately before . - For other operators (e.g. &&, +) prefer immediately after the operator - For brackets, break after the bracket - In the case of function calls, put each argument on a separate line if they do not fit after one line break - Nested function calls do not need to be broken up into separate lines even if the outer function call does. - If a method is bigger than 50 lines, break it into parts. - Put matching { } into the same column. - No spaces around operators (=, +, ==, ...) Exceptions: Spaces around &&, || and << - Space after comma (parameter lists, argument lists, ...) - Space after colon inside 'for' - For pointers and references, the */& should be attached to the variable name as oppposed to the tyep. E.g. for a pointer to an int the syntax would be: `int *x;` - No whitespaces at end of line - No whitespaces in blank lines - Put argument lists on next line (and ident 2 spaces) if too long - Put parameters on separate lines (and ident 2 spaces) if too long - No whitespaces around colon for inheritance, put inherited into separate lines in case of multiple inheritance - The initializer list follows the constructor without a whitespace around the colon. Break line after the colon if required and indent members. - if(...), else, for(...), do, and while(...) are always in a separate line - Break expressions in if, for, while if necessary and align them with the first character following the opening parenthesis - Use {} instead of ; for the empty statement - Single line blocks without { } are allowed, but put braces around multi-line blocks - Use blank lines to visually separate logically cohesive code blocks within a function - Have a newline at the end of a file Comments: - Do not use /* */ except for file and function comment blocks - Each source and header file must start with a comment block stating the Module name and Author [will be changed when we roll out doxygen] - Each function in the source file (not the header) is preceded by a function comment header consisting of a comment block stating Name, Inputs, Outputs and Purpose [will be changed when we roll out doxygen] - It should look like this: ``` /*******************************************************************\ Function: class_namet::function_name Inputs: arg_name - Description of its purpose long_arg_name - Descriptions should be indented to match the first line of the description Outputs: A description of what the function returns Purpose: A description of what the function does. Again, indentation with the line above \*******************************************************************/ ``` - An empty line should appear between the bottom of the function comment header and the function. - Put comments on a separate line - Use comments to explain the non-obvious - Use #if 0 for commenting out source code - Use #ifdef DEBUG to guard debug code Naming: - Identifiers may use the characters [a-z0-9_] and should start with a lower-case letter (parameters in constructors may start with _). - Use american spelling for identifiers. - Separate basic words by _ - Avoid abbreviations (e.g. prefer symbol_table to of st). - User defined type identifiers have to be terminated by 't'. Moreover, before 't' may not be '_'. - Do not use 'm_' prefix nor '_' suffix for names of attributes of structured types. - Enum values may use the characters [A-Z0-9_] Header files: - Avoid unnecessary #includes, especially in header files - Prefer forward declaration to includes, but forward declare at the top of the header file rather than in line - Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc Make files - Each source file should appear on a separate line - The final source file should still be followed by a trailing slash - The last line should be a comment to not be deleted, i.e. should look like: ``` SRC = source_file.cpp \ source_file2.cpp \ # Empty last line ``` - This ensures the Makefiles can be easily merged. Program Command Line Options - Each program contains a program_name_parse_optionst class which should contain a define PROGRAM_NAME_PARSE_OPTIONS which is a string of all the parse options in brackets (with a colon after the bracket if it takes a parameter) - Each parameter should be one per line to yield easy merging - If parameters are shared between programs, they should be pulled out into a common file and then included using a define - The defines should be OPT_FLAG_NAMES which should go into the OPTIONS define - The defines should include HELP_FLAG_NAMES which should contain the help output of the format: ``` " --flag explanations\n" \ " --another flag more explanation\n" \ <-------30 chars------> - The defines may include PARSE_OPTIONS_FLAG_NAMES which move the options from the command line into the options C++ features: - Do not use namespaces, except for anonymous namespaces. - Prefer use of 'typedef' insted of 'using'. - Prefer use of 'class' instead of 'struct'. - Write type modifiers before the type specifier. - Make references const whenever possible - Make functions const whenever possible - Do not hide base class functions - You are encouraged to use override - Single argument constructors must be explicit - Avoid implicit conversions - Avoid friend declarations - Avoid iterators, use ranged for instead - Avoid allocation with new/delete, use unique_ptr - Avoid pointers, use references - Avoid char *, use std::string - For numbers, use int, unsigned, long, unsigned long, double - Use mp_integer, not BigInt - Use the functions in util for conversions between numbers and strings - Avoid C-style functions. Use classes with an operator() instead. - Use irep_idt for identifiers (not std::string) - Avoid destructive updates if possible. The irept has constant time copy. - Use instances of std::size_t for comparison with return values of .size() of STL containers and algorithms, and use them as indices to arrays or vectors. - Do not use default values in public functions - Use assertions to detect programming errors, e.g. whenever you make assumptions on how your code is used - Use exceptions only when the execution of the program has to abort because of erroneous user input - We allow to use 3rd-party libraries directly. No wrapper matching the coding rules is required. Allowed libraries are: STL. - When throwing, omit the brackets, i.e. `throw "error"`. - Error messages should start with a lower case letter. - Use the auto keyword if and only if one of the following - The type is explictly repeated on the RHS (e.g. a constructor call) - Adding the type will increase confusion (e.g. iterators, function pointers) - Avoid assert, if the condition is an actual invariant, use INVARIANT, PRECONDITION, POSTCONDITION, CHECK_RETURN, UNREACHABLE or DATA_INVARIANT. If there are possible reasons why it might fail, throw an exception. Architecture-specific code: - Avoid if possible. - Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures. - Don't include architecture-specific header files without #ifdef ... Output: - Do not output to cout or cerr directly (except in temporary debug code, and then guard #include by #ifdef DEBUG) - Derive from messaget if the class produces output and use the streams provided (status(), error(), debug(), etc) - Use '\n' instead of std::endl Unit tests: - Unit tests are written using Catch: https://github.com/philsquared/Catch/ - For large classes: - Create a separate file that contains the tests for each method of each class - The file should be named according to `unit/class/path/class_name/function_name.cpp` - For small classes: - Create a separate file that contains the tests for all methods of each class - The file should be named according to unit/class/path/class_name.cpp - Catch supports tagging, tests should be tagged with all the following tags: - [core] should be used for all tests unless the test takes more than 1 second to run, then it should be tagged with [long] - [folder_name] of the file being tested - [class_name] of the class being tested - [function_name] of the function being tested You are allowed to break rules if you have a good reason to do so. Pre-commit hook to run cpplint locally -------------------------------------- To install the hook cp .githooks/pre-commit .git/hooks/pre-commit or use a symbolic link. Then, when running git commit, you should get the linter output (if any) before being prompted to enter a commit message. To bypass the check (e.g. if there was a false positive), add the option --no-verify.