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

C++ features:
- Do not use 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)

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

You are allowed to break rules if you have a good reason to do so.