Coding rules and cpplint

.travis.yml

@@ -23,3 +23,8 @@ install:
 
 script:
   - make CXXFLAGS="-Wall -O2 -g -Werror -Wno-deprecated-register -pedantic -Wno-sign-compare" -j2 && cd ../regression && make test
+
+matrix:
+  include:
+    - env: NAME="CPP-LINT"
+      script: cd .. && python scripts/cpplint.py `git diff --name-only master HEAD`

CODING_STANDARD

@@ -1,17 +1,101 @@
-Here a few minimalistic coding rules for the cprover source tree:
-
-a) 2 spaces indent, no tabs
-b) no "using namespace std;"
-c) Avoid new/delete, use containers instead.
-d) Avoid unnecessary #includes, especially in header files
-e) No lines wider than 80 chars
-f) Put matching { } into the same column
-g) If a method is bigger than a page, break it into parts
-h) Avoid destructive updates if possible. The irept has
-   constant time copy.
+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 50 lines, break it into parts.
+- Put matching { } into the same column.
+- 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 '_'.
+- 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
+- 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. 
 
 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
 
-a) Avoid if possible.
-b) Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
-c) Don't include architecture-specific header files without #ifdef ...
+You are allowed to break rules if you have a good reason to do so.