Skip to content

Commit 739c7f5

Browse files
smowtonsmowton
committed
Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026
2 parents 37b868a + 429c13f commit 739c7f5

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

67 files changed

+3154
-708
lines changed

‎.clang-format

+102
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
---
2+
AccessModifierOffset: '-2'
3+
AlignAfterOpenBracket: AlwaysBreak
4+
AlignConsecutiveAssignments: 'false'
5+
AlignConsecutiveDeclarations: 'false'
6+
AlignEscapedNewlinesLeft: 'false'
7+
AlignOperands: 'true'
8+
AlignTrailingComments: 'true'
9+
AllowAllParametersOfDeclarationOnNextLine: 'false'
10+
AllowShortBlocksOnASingleLine: 'false'
11+
AllowShortCaseLabelsOnASingleLine: 'false'
12+
AllowShortFunctionsOnASingleLine: None
13+
AllowShortIfStatementsOnASingleLine: 'false'
14+
AllowShortLoopsOnASingleLine: 'false'
15+
AlwaysBreakAfterReturnType: None
16+
AlwaysBreakBeforeMultilineStrings: 'true'
17+
AlwaysBreakTemplateDeclarations: 'true'
18+
BinPackArguments: 'false'
19+
BinPackParameters: 'false'
20+
BreakBeforeBinaryOperators: None
21+
BreakBeforeBraces: Allman
22+
BreakBeforeTernaryOperators: 'true'
23+
BreakConstructorInitializersBeforeComma: 'false'
24+
ColumnLimit: '80'
25+
ConstructorInitializerAllOnOneLineOrOnePerLine: 'true'
26+
ConstructorInitializerIndentWidth: '2'
27+
ContinuationIndentWidth: '2'
28+
Cpp11BracedListStyle: 'true'
29+
DerivePointerAlignment: 'false'
30+
DisableFormat: 'false'
31+
ExperimentalAutoDetectBinPacking: 'false'
32+
ForEachMacros: [
33+
'forall_rw_range_set_r_objects',
34+
'Forall_rw_range_set_r_objects',
35+
'forall_rw_range_set_w_objects',
36+
'Forall_rw_range_set_w_objects',
37+
'forall_rw_set_r_entries',
38+
'Forall_rw_set_r_entries',
39+
'forall_rw_set_w_entries',
40+
'Forall_rw_set_w_entries',
41+
'forall_goto_functions',
42+
'Forall_goto_functions',
43+
'forall_goto_program_instructions',
44+
'Forall_goto_program_instructions',
45+
'forall_objects',
46+
'Forall_objects',
47+
'forall_valid_objects',
48+
'Forall_valid_objects',
49+
'forall_nodes',
50+
'Forall_nodes',
51+
'forall_literals',
52+
'Forall_literals',
53+
'forall_operands',
54+
'Forall_operands',
55+
'forall_expr',
56+
'Forall_expr',
57+
'forall_expr_list',
58+
'Forall_expr_list',
59+
'forall_symbolptr_list',
60+
'Forall_symbolptr_list',
61+
'forall_guard',
62+
'Forall_guard',
63+
'forall_irep',
64+
'Forall_irep',
65+
'forall_named_irep',
66+
'Forall_named_irep',
67+
'forall_value_list',
68+
'Forall_value_list',
69+
'forall_symbols',
70+
'Forall_symbols',
71+
'forall_symbol_base_map',
72+
'Forall_symbol_base_map',
73+
'forall_symbol_module_map',
74+
'Forall_symbol_module_map',
75+
'forall_subtypes',
76+
'Forall_subtypes']
77+
IndentCaseLabels: 'false'
78+
IndentWidth: '2'
79+
IndentWrappedFunctionNames: 'false'
80+
KeepEmptyLinesAtTheStartOfBlocks: 'false'
81+
Language: Cpp
82+
MaxEmptyLinesToKeep: '1'
83+
NamespaceIndentation: None
84+
PenaltyBreakString: 10000
85+
PointerAlignment: Right
86+
ReflowComments: 'false'
87+
SortIncludes: 'false'
88+
SpaceAfterCStyleCast: 'false'
89+
SpaceBeforeAssignmentOperators: 'true'
90+
SpaceBeforeParens: Never
91+
SpaceInEmptyParentheses: 'false'
92+
SpacesBeforeTrailingComments: '1'
93+
SpacesInAngles: 'false'
94+
SpacesInCStyleCastParentheses: 'false'
95+
SpacesInContainerLiterals: 'false'
96+
SpacesInParentheses: 'false'
97+
SpacesInSquareBrackets: 'false'
98+
Standard: Cpp11
99+
TabWidth: '2'
100+
UseTab: Never
101+
102+
...

‎.travis.yml

+66
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,33 @@ language: cpp
33
jobs:
44
include:
55

6+
- &formatting-stage
7+
stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
8+
env: NAME="clang-format"
9+
addons:
10+
apt:
11+
packages:
12+
- clang-format-3.8
13+
install:
14+
script: |
15+
# Apparently update-alternatives doesn't work in Travis containers
16+
mkdir -p priority-symlinks
17+
ln -s /usr/bin/clang-format-3.8 priority-symlinks/clang-format
18+
export PATH=${PWD}/priority-symlinks:${PATH}
19+
20+
# Now we can do the formatting pass
21+
clang-format --version
22+
git-clang-format-3.8 "${TRAVIS_BRANCH}"
23+
git diff --color > formatted.diff
24+
if [[ -s formatted.diff ]] ; then
25+
echo 'Formatting error! Apply the following diff and resubmit:'
26+
cat formatted.diff
27+
exit 1
28+
fi
29+
echo 'No formatting errors found'
30+
exit 0
31+
before_cache:
32+
633
- &linter-stage
734
stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
835
env: NAME="CPP-LINT"
@@ -39,6 +66,32 @@ jobs:
3966
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
4067
env: COMPILER="ccache g++-5"
4168

69+
# OS X using g++
70+
- stage: Test different OS/CXX/Flags
71+
os: osx
72+
sudo: false
73+
compiler: gcc
74+
cache: ccache
75+
before_install:
76+
#we create symlink to non-ccache gcc, to be used in tests
77+
- mkdir bin ; ln -s /usr/bin/gcc bin/gcc
78+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
79+
- export PATH=/usr/local/opt/ccache/libexec:$PATH
80+
env: COMPILER="ccache g++"
81+
82+
# OS X using clang++
83+
- stage: Test different OS/CXX/Flags
84+
os: osx
85+
sudo: false
86+
compiler: clang
87+
cache: ccache
88+
before_install:
89+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
90+
- export PATH=/usr/local/opt/ccache/libexec:$PATH
91+
env:
92+
- COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
93+
- CCACHE_CPP2=yes
94+
4295
# Ubuntu Linux with glibc using g++-5, debug mode
4396
- stage: Test different OS/CXX/Flags
4497
os: linux
@@ -127,6 +180,18 @@ jobs:
127180
- cmake --build build -- -j4
128181
script: (cd build; ctest -V -L CORE)
129182

183+
- stage: Test different OS/CXX/Flags
184+
os: osx
185+
cache: ccache
186+
env:
187+
- BUILD_SYSTEM=cmake
188+
- CCACHE_CPP2=yes
189+
install:
190+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64'
191+
- cmake --build build -- -j4
192+
script: (cd build; ctest -V -L CORE)
193+
194+
130195
# Run Coverity
131196
- stage: Test different OS/CXX/Flags
132197
os: linux
@@ -165,6 +230,7 @@ jobs:
165230
script: echo "This is coverity build. No need for tests."
166231

167232
allow_failures:
233+
- <<: *formatting-stage
168234
- <<: *linter-stage
169235

170236
install:

‎CODEOWNERS

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# These owners will be the default owners for everything in the repo.
2+
* @kroening @tautschnig @peterschrammel
3+
4+
src/java_bytecode/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
5+
src/jbmc/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli @Degiorgio @NathanJPhillips
6+
src/miniz/ @smowton @mgudemann @cristina-david @jgwilson42 @pkesseli
7+
8+
src/ansi-c/ @marek-trtik @kroening @tautschnig
9+
10+
src/cpp/ @marek-trtik @kroening @tautschnig
11+
12+
CMakeLists.txt @reuk @thk123
13+
14+
cmake/ @reuk @thk123
15+
16+
src/solvers/ @martin-cs @romainbrenguier @antlechner @kroening
17+
18+
src/analyses/ @martin-cs @peterschrammel @thk123 @marek-trtik @NathanJPhillips
19+
20+
src/pointer-analysis/ @martin-cs @peterschrammel @thk123 @marek-trtik
21+
22+
src/goto-analyzer/ @martin-cs @peterschrammel @thk123 @marek-trtik
23+
24+
src/goto-instrument/ @martin-cs @peterschrammel @thk123 @marek-trtik
25+
26+
src/goto-programs/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik
27+
28+
src/linking/ @smowton @kroening @tautschnig @peterschrammel @marek-trtik
29+
30+
unit/ @diffblue/cbmc-developers
31+
32+
regression/ @diffblue/cbmc-developers
33+
34+
.travis.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
35+
appveyor.yml @diffblue/devops @thk123 @forejtv @jgwilson42 @rabiamarzhiya
36+

‎CODING_STANDARD.md

+9-6
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
11
Here a few minimalistic coding rules for the CPROVER source tree.
22

33
# Whitespaces
4+
5+
Formatting is enforced using clang-format. For more information about this, see
6+
`COMPILING.md`. A brief summary of the formatting rules is given below:
7+
48
- Use 2 spaces indent, no tabs.
59
- No lines wider than 80 chars.
610
- When line is wider, do the following:
@@ -16,8 +20,7 @@ Here a few minimalistic coding rules for the CPROVER source tree.
1620
even if the outer function call does.
1721
- If a method is bigger than 50 lines, break it into parts.
1822
- Put matching `{ }` into the same column.
19-
- No spaces around operators (`=`, `+`, `==` ...) Exceptions: Spaces around
20-
`&&`, `||` and `<<`
23+
- Spaces around binary operators (`=`, `+`, `==` ...)
2124
- Space after comma (parameter lists, argument lists, ...)
2225
- Space after colon inside `for`
2326
- 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.
2730
- No whitespaces in blank lines
2831
- Put argument lists on next line (and indent 2 spaces) if too long
2932
- Put parameters on separate lines (and indent 2 spaces) if too long
30-
- No whitespaces around colon for inheritance, put inherited into separate
31-
lines in case of multiple inheritance
32-
- The initializer list follows the constructor without a whitespace around the
33-
colon. Break line after the colon if required and indent members.
33+
- Spaces around colon for inheritance, put inherited into separate lines in
34+
case of multiple inheritance
35+
- The initializer list follows the constructor with a whitespace around the
36+
colon.
3437
- `if(...)`, `else`, `for(...)`, `do`, and `while(...)` are always in a
3538
separate line
3639
- Break expressions in `if`, `for`, `while` if necessary and align them with

0 commit comments

Comments
 (0)