Reformat sources with clang-format

.clang-format

@@ -0,0 +1,102 @@
+---
+AccessModifierOffset: '-2'
+AlignAfterOpenBracket: AlwaysBreak
+AlignConsecutiveAssignments: 'false'
+AlignConsecutiveDeclarations: 'false'
+AlignEscapedNewlinesLeft: 'false'
+AlignOperands: 'true'
+AlignTrailingComments: 'true'
+AllowAllParametersOfDeclarationOnNextLine: 'false'
+AllowShortBlocksOnASingleLine: 'false'
+AllowShortCaseLabelsOnASingleLine: 'false'
+AllowShortFunctionsOnASingleLine: None
+AllowShortIfStatementsOnASingleLine: 'false'
+AllowShortLoopsOnASingleLine: 'false'
+AlwaysBreakAfterReturnType: None
+AlwaysBreakBeforeMultilineStrings: 'true'
+AlwaysBreakTemplateDeclarations: 'true'
+BinPackArguments: 'false'
+BinPackParameters: 'false'
+BreakBeforeBinaryOperators: None
+BreakBeforeBraces: Allman
+BreakBeforeTernaryOperators: 'true'
+BreakConstructorInitializersBeforeComma: 'false'
+ColumnLimit: '80'
+ConstructorInitializerAllOnOneLineOrOnePerLine: 'true'
+ConstructorInitializerIndentWidth: '2'
+ContinuationIndentWidth: '2'
+Cpp11BracedListStyle: 'true'
+DerivePointerAlignment: 'false'
+DisableFormat: 'false'
+ExperimentalAutoDetectBinPacking: 'false'
+ForEachMacros: [
+  'forall_rw_range_set_r_objects',
+  'Forall_rw_range_set_r_objects',
+  'forall_rw_range_set_w_objects',
+  'Forall_rw_range_set_w_objects',
+  'forall_rw_set_r_entries',
+  'Forall_rw_set_r_entries',
+  'forall_rw_set_w_entries',
+  'Forall_rw_set_w_entries',
+  'forall_goto_functions',
+  'Forall_goto_functions',
+  'forall_goto_program_instructions',
+  'Forall_goto_program_instructions',
+  'forall_objects',
+  'Forall_objects',
+  'forall_valid_objects',
+  'Forall_valid_objects',
+  'forall_nodes',
+  'Forall_nodes',
+  'forall_literals',
+  'Forall_literals',
+  'forall_operands',
+  'Forall_operands',
+  'forall_expr',
+  'Forall_expr',
+  'forall_expr_list',
+  'Forall_expr_list',
+  'forall_symbolptr_list',
+  'Forall_symbolptr_list',
+  'forall_guard',
+  'Forall_guard',
+  'forall_irep',
+  'Forall_irep',
+  'forall_named_irep',
+  'Forall_named_irep',
+  'forall_value_list',
+  'Forall_value_list',
+  'forall_symbols',
+  'Forall_symbols',
+  'forall_symbol_base_map',
+  'Forall_symbol_base_map',
+  'forall_symbol_module_map',
+  'Forall_symbol_module_map',
+  'forall_subtypes',
+  'Forall_subtypes']
+IndentCaseLabels: 'false'
+IndentWidth: '2'
+IndentWrappedFunctionNames: 'false'
+KeepEmptyLinesAtTheStartOfBlocks: 'false'
+Language: Cpp
+MaxEmptyLinesToKeep: '1'
+NamespaceIndentation: None
+PenaltyBreakString: 10000
+PointerAlignment: Right
+ReflowComments: 'false'
+SortIncludes: 'false'
+SpaceAfterCStyleCast: 'false'
+SpaceBeforeAssignmentOperators: 'true'
+SpaceBeforeParens: Never
+SpaceInEmptyParentheses: 'false'
+SpacesBeforeTrailingComments: '1'
+SpacesInAngles: 'false'
+SpacesInCStyleCastParentheses: 'false'
+SpacesInContainerLiterals: 'false'
+SpacesInParentheses: 'false'
+SpacesInSquareBrackets: 'false'
+Standard: Cpp11
+TabWidth: '2'
+UseTab: Never
+
+...

.travis.yml

@@ -3,6 +3,32 @@ language: cpp
 jobs:
   include:
 
+    - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
+      env: NAME="clang-format"
+      addons:
+        apt:
+          packages:
+            - clang-format-3.8
+      install:
+      script: |
+        # Apparently update-alternatives doesn't work in Travis containers
+        mkdir -p priority-symlinks
+        ln -s /usr/bin/clang-format-3.8 priority-symlinks/clang-format
+        export PATH=${PWD}/priority-symlinks:${PATH}
+
+        # Now we can do the formatting pass
+        clang-format --version
+        git-clang-format-3.8 "${TRAVIS_BRANCH}"
+        git diff --color > formatted.diff
+        if [[ -s formatted.diff ]] ; then
+          echo 'Formatting error! Apply the following diff and resubmit:'
+          cat formatted.diff
+          exit 1
+        fi
+        echo 'No formatting errors found'
+        exit 0
+      before_cache:
+
     - &linter-stage
       stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
       env: NAME="CPP-LINT"

CODING_STANDARD.md

@@ -1,6 +1,10 @@
 Here a few minimalistic coding rules for the CPROVER source tree.
 
 # Whitespaces
+
+Formatting is enforced using clang-format. For more information about this, see
+`COMPILING.md`. A brief summary of the formatting rules is given below:
+
 - Use 2 spaces indent, no tabs.
 - No lines wider than 80 chars.
   - When line is wider, do the following:
@@ -16,8 +20,7 @@ Here a few minimalistic coding rules for the CPROVER source tree.
         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 `<<`
+- Spaces around binary operators (`=`, `+`, `==` ...)
 - Space after comma (parameter lists, argument lists, ...)
 - Space after colon inside `for`
 - For pointers and references, the `*`/`&` should be attached to the variable
@@ -27,10 +30,10 @@ Here a few minimalistic coding rules for the CPROVER source tree.
 - No whitespaces in blank lines
 - Put argument lists on next line (and indent 2 spaces) if too long
 - Put parameters on separate lines (and indent 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.
+- Spaces around colon for inheritance, put inherited into separate lines in
+  case of multiple inheritance
+- The initializer list follows the constructor with a whitespace around the
+  colon.
 - `if(...)`, `else`, `for(...)`, `do`, and `while(...)` are always in a
   separate line
 - Break expressions in `if`, `for`, `while` if necessary and align them with