Squashed 'cbmc/' changes from 64d81f1..739c7f5

739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026
37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table
429c13f Merge pull request diffblue#1520 from smowton/smowton/fix/symbol_table_writer_erase
d9f3a2f Revert "Disable OSX builds"
81bb39c Symbol-table writer: fix use of map key after erasure
021fe8f Merge pull request diffblue#1492 from tautschnig/perf-test
0729e3d Merge pull request diffblue#1517 from NathanJPhillips/bugfix/journaling-symbol-table-constructor
93ae9f3 Merge pull request diffblue#1527 from diffblue/revert-1510-always-inline
c4ed1ae Revert security-scanner version of recording symbol table
e83e307 Fixed scope of moved symbol
535f1df Revert "Fully process always_inline"
0096451 Replace broken copy constructor with move constructor
a6adb19 Fix more catch std::string occurances
22a876f Merge pull request diffblue#1523 from reuk/reuk/update-compiling-instructions
8fe258b Update COMPILING with cmake setup instructions
99592b3 Merge pull request diffblue#1504 from andreast271/update-windows-build
dff22b8 Make Windows compilation instructions more prescriptive
bc3bc8f Merge pull request diffblue#1511 from tautschnig/fix-graphml
358829c Merge pull request diffblue#1510 from tautschnig/always-inline
3e77dd6 Merge pull request diffblue#1496 from smowton/smowton/feature/symbol_table_writer
d115b4e catch by const ref instead of by value or non-const ref
444d824 Fix graphml output of concurrency witnesses
08c512d Make Windows compilation instructions more prescriptive
bcf8ff3 Update documentation for building cbmc on windows. Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line.
728dbb5 Merge pull request diffblue#1508 from smowton/smowton/1420-fragments/value_set_debugging
9d9e50d Merge pull request diffblue#1507 from smowton/smowton/1420-fragments/factor_java_object_init
b2104b0 Merge pull request diffblue#1506 from smowton/smowton/1420-fragments/typecheck_expr_cleanup
7175efe Merge pull request diffblue#1505 from smowton/smowton/1420-fragments/invariants
7537302 Adding a java_lang_object_init function
86513ee Merge pull request diffblue#1324 from reuk/reuk/clang-format
ea4a777 Merge pull request diffblue#1503 from reuk/reuk/rebuild-ansi-c-when-necessary
d9c0598 [pointer-analysis] Better debugging information in pointer analysis
3146336 Remove unnecessary includes in java-typecheck
10b5c8e [java-bytecode/typecheck] Style: Changing assertions in preconditions
2afe377 Fully interpret __attribute__((always_inline))
8eaf89e Apply symbol replacement in type_arg members
13a7553 Rebuild ansi-c library if non-source dependencies change
b97a766 Merge pull request diffblue#1403 from karkhaz/kk-regenerate-arch-flags-binaries
a4dc986 Merge pull request diffblue#1484 from diffblue/interpreter_size_t
9d4e0ca Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs
c3e6726 Script to automate performance evaluation of CBMC on AWS
912ee38 Improve symbol table style
6b1a49d Add missing goto-statistics file to Makefile
d512204 Add cbmc and jbmc as install targets
bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019
c5c77ac Merge pull request diffblue#1495 from diffblue/codeowners2
f154d16 Merge pull request diffblue#1487 from martin-cs/goto-analyzer-6-part2
4955417 initialize_goto_model now returns a goto_model
56f924c Merge pull request diffblue#1483 from diffblue/signature_initialize_goto_model
eef32db Methods for ai_baset to allow access to the ai_base_domaint for a location.
aae984a Disable the regression test for now as it depends on the variable sensitivity domain.
3050c53 Don't stop when recursion found
93f2e1f Use is_bottom() to catch unreachable functions.
5b604ae Update the mock domain with the new ai_domain_baset interface.
f9ca353 Add is_bottom() and is_top() to ai_domain_baset and derived domains.
88d8673 Rename the XML output to something a bit more meaningful.
2110cd1 Make formatting stage non-blocking on Travis
a24ac3d Fixup compiling.md with more clang-format install instructions
c3c24e2 Add symbol table writer
98643d7 initialize_goto_model now returns a goto_model
fd6acc5 initial proposal for owners of code
f39ae5c use mp_integer for addresses
f6ae635 use std::size_t in interpreter
55e6594 Fixup cpplint.py
9d4b827 Update coding standard
8482b35 Add information about using clang-format
1dcc82c Convert COMPILING to markdown format
554cb54 Adjust cpplint to disable whitespace checks by default
6ce0dba Add travis style check
f18979a Add clang-format config
622e2e3 Merge branch 'develop' into show_functions_dfs
bea696a Regenerated cross-compiled arch flag test binaries
1fab1c1 Fixed show-call-sequences deature of goto instrument; added test suite

git-subtree-dir: cbmc
git-subtree-split: 739c7f5

Author: smowton

.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,33 @@ language: cpp
 jobs:
   include:
 
+    - &formatting-stage
+      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"
@@ -39,6 +66,32 @@ jobs:
       # env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
       env: COMPILER="ccache g++-5"
 
+    # OS X using g++
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      sudo: false
+      compiler: gcc
+      cache: ccache
+      before_install:
+          #we create symlink to non-ccache gcc, to be used in tests
+        - mkdir bin ; ln -s /usr/bin/gcc bin/gcc
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
+        - export PATH=/usr/local/opt/ccache/libexec:$PATH
+      env: COMPILER="ccache g++"
+
+    # OS X using clang++
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      sudo: false
+      compiler: clang
+      cache: ccache
+      before_install:
+        - HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
+        - export PATH=/usr/local/opt/ccache/libexec:$PATH
+      env:
+        - COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
+        - CCACHE_CPP2=yes
+
     # Ubuntu Linux with glibc using g++-5, debug mode
     - stage: Test different OS/CXX/Flags
       os: linux
@@ -127,6 +180,18 @@ jobs:
         - cmake --build build -- -j4
       script: (cd build; ctest -V -L CORE)
 
+    - stage: Test different OS/CXX/Flags
+      os: osx
+      cache: ccache
+      env:
+        - BUILD_SYSTEM=cmake
+        - CCACHE_CPP2=yes
+      install:
+        - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
+        - cmake --build build -- -j4
+      script: (cd build; ctest -V -L CORE)
+
+
     # Run Coverity
     - stage: Test different OS/CXX/Flags
       os: linux
@@ -165,6 +230,7 @@ jobs:
       script: echo "This is coverity build. No need for tests."
 
   allow_failures:
+    - <<: *formatting-stage
     - <<: *linter-stage
 
 install:

CODEOWNERS

@@ -0,0 +1,36 @@
+# These owners will be the default owners for everything in the repo.
+*       @kroening @tautschnig @peterschrammel
+
+src/java_bytecode/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
+src/jbmc/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
+src/miniz/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli
+
+src/ansi-c/ @marek-trtik @kroening @tautschnig
+
+src/cpp/ @marek-trtik @kroening @tautschnig
+
+CMakeLists.txt @reuk @thk123
+
+cmake/ @reuk @thk123
+
+src/solvers/ @martin-cs @romainbrenguier @antlechner @kroening
+
+src/analyses/ @martin-cs @peterschrammel @thk123 @marek-trtik @NathanJPhillips
+
+src/pointer-analysis/ @martin-cs @peterschrammel @thk123 @marek-trtik 
+
+src/goto-analyzer/ @martin-cs @peterschrammel @thk123 @marek-trtik 
+
+src/goto-instrument/ @martin-cs @peterschrammel @thk123 @marek-trtik  
+
+src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik  
+
+src/linking/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik  
+
+unit/ @diffblue/cbmc-developers
+
+regression/ @diffblue/cbmc-developers
+
+.travis.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
+appveyor.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
+

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