Coding rules and cpplint

CODING_STANDARD

@@ -1,17 +1,31 @@
 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.
+- Use 2 spaces indent, no tabs.
+- No lines wider than 80 chars.
+- If a method is bigger than a page, 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'.
+- 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.
+- 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;".
+- 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!
 
 Architecture-specific code:
 
-a) Avoid if possible.
-b) Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
-c) Don't include architecture-specific header files without #ifdef ...
+- Avoid if possible.
+- Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
+- Don't include architecture-specific header files without #ifdef ...