Skip to content

Commit 207b801

Browse files
NathanJPhillipsNathanJPhillips
committed
Merge branch 'develop' into merge_2018-03-26
2 parents 906aeb3 + 301cd46 commit 207b801

File tree

1,062 files changed

+56571
-10323
lines changed

Some content is hidden

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

1,062 files changed

+56571
-10323
lines changed

‎.gitignore

+3
Original file line numberDiff line numberDiff line change
@@ -102,8 +102,11 @@ src/goto-cc/goto-cc.exe
102102
src/goto-cc/goto-cl.exe
103103
src/goto-instrument/goto-instrument
104104
src/goto-instrument/goto-instrument.exe
105+
src/jbmc/jbmc
105106
src/musketeer/musketeer
106107
src/musketeer/musketeer.exe
108+
src/solvers/smt2/smt2_solver
109+
src/solvers/smt2/smt2_solver.exe
107110
src/symex/symex
108111
src/symex/symex.exe
109112
src/goto-diff/goto-diff

‎.travis.yml

+38-20
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,24 @@ jobs:
4242
env: NAME="DOXYGEN-CHECK"
4343
addons:
4444
apt:
45+
sources:
46+
- sourceline: 'deb http://packages.cloud.google.com/apt cloud-sdk-trusty main'
47+
key_url: 'https://packages.cloud.google.com/apt/doc/apt-key.gpg'
4548
packages:
4649
- doxygen
50+
- google-cloud-sdk
4751
install:
4852
script: scripts/travis_doxygen.sh
4953
before_cache:
54+
after_success:
55+
# Google Cloud Integration
56+
- export BRANCH="${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}"
57+
- openssl aes-256-cbc -k ${GCLOUD_TRAVIS_CBMC_KEY}
58+
-in gcloud-travis-cbmc.json.enc -out gcloud-travis-cbmc.json -d
59+
- export G_KEY=${PWD}/gcloud-travis-cbmc.json
60+
- gcloud auth activate-service-account --key-file ${G_KEY}
61+
62+
- scripts/publish_doc.sh
5063

5164
# Ubuntu Linux with glibc using g++-5
5265
- stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
@@ -62,11 +75,12 @@ jobs:
6275
- libwww-perl
6376
- g++-5
6477
- libubsan0
78+
- parallel
6579
before_install:
6680
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
6781
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
6882
env:
69-
- COMPILER="ccache g++-5"
83+
- COMPILER="ccache /usr/bin/g++-5"
7084
- EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
7185

7286
# OS X using g++
@@ -76,10 +90,8 @@ jobs:
7690
compiler: gcc
7791
cache: ccache
7892
before_install:
79-
#we create symlink to non-ccache gcc, to be used in tests
80-
- mkdir bin ; ln -s /usr/bin/gcc bin/gcc
81-
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
82-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
93+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
94+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
8395
env: COMPILER="ccache g++"
8496

8597
# OS X using clang++
@@ -89,10 +101,11 @@ jobs:
89101
compiler: clang
90102
cache: ccache
91103
before_install:
92-
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
93-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
104+
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache parallel
105+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
94106
env:
95-
- COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
107+
- COMPILER="ccache clang++"
108+
- EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics"
96109
- CCACHE_CPP2=yes
97110

98111
# Ubuntu Linux with glibc using g++-5, debug mode
@@ -113,7 +126,7 @@ jobs:
113126
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
114127
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
115128
env:
116-
- COMPILER="ccache g++-5"
129+
- COMPILER="ccache /usr/bin/g++-5"
117130
- EXTRA_CXXFLAGS="-DDEBUG"
118131
script: echo "Not running any tests for a debug build."
119132

@@ -133,16 +146,17 @@ jobs:
133146
- clang-3.7
134147
- libstdc++-5-dev
135148
- libubsan0
149+
- parallel
136150
before_install:
137151
- mkdir bin ; ln -s /usr/bin/clang-3.7 bin/gcc
138152
- export CCACHE_CPP2=yes
139153
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
140154
env:
141-
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
155+
- COMPILER="ccache /usr/bin/clang++-3.7"
156+
- EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DNDEBUG"
142157
- CCACHE_CPP2=yes
143-
- EXTRA_CXXFLAGS="-DNDEBUG"
144158

145-
# Ubuntu Linux with glibc using clang++-3.7, debug mode
159+
# Ubuntu Linux with glibc using clang++-3.7, debug mode, disable USE_DSTRING
146160
- stage: Test different OS/CXX/Flags
147161
os: linux
148162
sudo: false
@@ -163,14 +177,15 @@ jobs:
163177
- export CCACHE_CPP2=yes
164178
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
165179
env:
166-
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
180+
- COMPILER="ccache /usr/bin/clang++-3.7"
181+
- EXTRA_CXXFLAGS="-Qunused-arguments -fcolor-diagnostics -DDEBUG -DUSE_STD_STRING"
167182
- CCACHE_CPP2=yes
168-
- EXTRA_CXXFLAGS="-DDEBUG"
169183
script: echo "Not running any tests for a debug build."
170184

171185
# cmake build using g++-5
172186
- stage: Test different OS/CXX/Flags
173187
os: linux
188+
compiler: gcc
174189
cache: ccache
175190
env:
176191
- BUILD_SYSTEM=cmake
@@ -180,19 +195,22 @@ jobs:
180195
- ubuntu-toolchain-r-test
181196
packages:
182197
- g++-5
198+
before_install:
199+
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
183200
install:
184201
- ccache -z
185202
- ccache --max-size=1G
186-
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
203+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
187204
- cmake --build build -- -j4
188205
script: (cd build; ctest -V -L CORE -j2)
189206

190207
- stage: Test different OS/CXX/Flags
191208
os: osx
209+
compiler: clang
192210
cache: ccache
193211
before_install:
194212
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
195-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
213+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
196214
env:
197215
- BUILD_SYSTEM=cmake
198216
- CCACHE_CPP2=yes
@@ -251,13 +269,13 @@ install:
251269
- make -C src minisat2-download
252270
- make -C src boost-download
253271
- make -C src/ansi-c library_check
254-
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j2
255-
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir
272+
- make -C src "CXX=${COMPILER} -DUSE_BOOST ${EXTRA_CXXFLAGS}" -j3
273+
- make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
256274

257275
script:
258276
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
259-
- env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
260-
- make -C unit "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
277+
- env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
278+
- make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
261279
- make -C unit test
262280

263281
before_cache:

‎CODEOWNERS

+2-3
Original file line numberDiff line numberDiff line change
@@ -46,12 +46,11 @@ src/cpp/ @kroening @tautschnig @peterschrammel
4646

4747
# These files change frequently and changes are low-risk
4848

49+
src/util/irep_ids.def @diffblue/cbmc-developers
50+
4951
unit/ @diffblue/cbmc-developers
5052
regression/ @diffblue/cbmc-developers
5153

52-
CMakeLists.txt @reuk @chrisr-diffblue
53-
cmake/ @reuk @chrisr-diffblue
54-
5554
scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
5655
.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel
5756
appveyor.yml @diffblue/devops @thk123 @forejtv @peterschrammel

‎COMPILING.md

+5-5
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,11 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
2121
The GNU Make needs to be version 3.81 or higher.
2222
On Debian-like distributions, do
2323
```
24-
apt-get install g++ gcc flex bison make git libwww-perl patch
24+
apt-get install g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk
2525
```
2626
On Red Hat/Fedora or derivates, do
2727
```
28-
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
28+
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
2929
```
3030
Note that you need g++ version 4.9 or newer.
3131
2. As a user, get the CBMC source via
@@ -91,7 +91,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
9191

9292
1. As root, get the necessary tools:
9393
```
94-
pkg install bash gmake git www/p5-libwww patch flex bison
94+
pkg install bash gmake git www/p5-libwww patch flex bison openjdk
9595
```
9696
2. As a user, get the CBMC source via
9797
```
@@ -186,11 +186,11 @@ require manual modification of build files.
186186
--version`. To install all build dependencies:
187187
- On Debian-like distributions, do
188188
```
189-
apt-get install cmake g++ gcc flex bison make git libwww-perl patch
189+
apt-get install cmake g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk
190190
```
191191
- On Red Hat/Fedora or derivates, do
192192
```
193-
yum install cmake gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
193+
yum install cmake gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
194194
```
195195
- On macOS, do
196196
```

‎README.md

+2
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33

44
[CProver Wiki](http://www.cprover.org/wiki)
55

6+
[CProver Documentation](http://cprover.diffblue.com)
7+
68
About
79
=====
810

‎appveyor.yml

+1
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ install:
1717
Move-Item win_bison.exe bin\bison.exe -force
1818
Move-Item win_flex.exe bin\flex.exe -force
1919
Move-Item FlexLexer.h include\FlexLexer.h -force
20+
Remove-Item bin\data -Force -Recurse -ErrorAction SilentlyContinue
2021
Move-Item data bin\data -force
2122
bison -V
2223
flex -V

‎buildspec.yml

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
version: 0.2
2+
3+
phases:
4+
install:
5+
commands:
6+
- echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list
7+
- apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F
8+
- apt-get update -y
9+
- apt-get install -y g++-5 flex bison make git libwww-perl patch ccache
10+
- apt-get install -y openjdk-7-jdk
11+
- update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1
12+
- update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1
13+
build:
14+
commands:
15+
- echo Build started on `date`
16+
- (cd src ; make minisat2-download)
17+
- (cd src ; make CXX="ccache g++" -j2)
18+
- (cd regression ; make test)
19+
post_build:
20+
commands:
21+
- echo Build completed on `date`
22+
artifacts:
23+
files:
24+
cache:
25+
paths:
26+
- '/root/.ccache/**/*'

0 commit comments

Comments
 (0)