CODING_STANDARD

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 <iostream> 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.