Refined coding rules

Author: peterschrammel

CODING_STANDARD

@@ -1,31 +1,101 @@
-Here a few minimalistic coding rules for the cprover source tree:
+Here a few minimalistic coding rules for the CPROVER source tree.
 
+Whitespaces:
 - Use 2 spaces indent, no tabs.
 - No lines wider than 80 chars.
-- If a method is bigger than a page, break it into parts.
+- If a method is bigger than 50 lines, break it into parts.
 - Put matching { } into the same column.
-- Do not use namespaces.
-- Prefer use of 'typedef' insted of 'using'.
-- Prefer use of 'class' instead of 'struct'.
+- No spaces around operators, except &&, ||, and <<
+- Spaces after , and ; inside 'for'
+- 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
+- No whitespaces at end of line
+- Avoid whitespaces in blank lines
+- 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 comment block stating Name, Inputs,  Outputs and Purpose [will be changed
+  when we roll out doxygen]
+- 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 '_'.
-- Avoid new/delete, use containers instead. In other words, do not perform
-  heap operations directly.
-- Write type modifiers before the type specifier.
 - Do not use 'm_' prefix nor '_' suffix for names of attributes of structured
   types.
-- Avoid destructive updates if possible. The irept has
-  constant time copy.
+- Enum values may use the characters [A-Z0-9_]
+
+Header files:
 - Avoid unnecessary #includes, especially in header files
-- We allow to use 3rd libraries directly. No wrapper matching the coding rules
-  is required. Allowed libraries are: C++ standard library.
-- No "using namespace std;".
+- 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
-  SLT containers and algorithms, and use them as indices to arrays or vectors.
-- Prohibited stuff from the standard library: ??? TODO!
+  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. 
 
 Architecture-specific code:
-
 - Avoid if possible.
 - Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
-- Don't include architecture-specific header files without #ifdef ...
+- 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.