Skip to content

Commit 51b6c8c

Browse files
JohnDumbellJohnDumbell
authored
Merge pull request diffblue#461 from diffblue/CBMC_merge_2018-06-20
CBMC merge
2 parents 4258f86 + 93a12ab commit 51b6c8c

Some content is hidden

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

58 files changed

+1035
-268
lines changed

‎cbmc/.travis.yml

Lines changed: 76 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,9 @@ jobs:
103103
- parallel
104104
- libc6-dev-i386
105105
before_install:
106-
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
106+
- mkdir bin
107+
- ln -s /usr/bin/gcc-5 bin/gcc
108+
- ln -s /usr/bin/g++-5 bin/g++
107109
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
108110
env:
109111
- COMPILER="ccache /usr/bin/g++-5"
@@ -136,7 +138,9 @@ jobs:
136138
- libubsan0
137139
- libc6-dev-i386
138140
before_install:
139-
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
141+
- mkdir bin
142+
- ln -s /usr/bin/gcc-5 bin/gcc
143+
- ln -s /usr/bin/g++-5 bin/g++
140144
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
141145
env:
142146
- COMPILER="ccache /usr/bin/g++-5"
@@ -157,12 +161,15 @@ jobs:
157161
packages:
158162
- libwww-perl
159163
- clang-3.7
164+
- g++-5
160165
- libstdc++-5-dev
161166
- libubsan0
162167
- parallel
163168
- libc6-dev-i386
164169
before_install:
165-
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
170+
- mkdir bin
171+
- ln -s /usr/bin/gcc-5 bin/gcc
172+
- ln -s /usr/bin/c++-5 bin/g++
166173
- export CCACHE_CPP2=yes
167174
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
168175
env:
@@ -184,11 +191,14 @@ jobs:
184191
packages:
185192
- libwww-perl
186193
- clang-3.7
194+
- g++-5
187195
- libstdc++-5-dev
188196
- libubsan0
189197
- libc6-dev-i386
190198
before_install:
191-
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
199+
- mkdir bin
200+
- ln -s /usr/bin/gcc-5 bin/gcc
201+
- ln -s /usr/bin/g++-5 bin/g++
192202
- export CCACHE_CPP2=yes
193203
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
194204
env:
@@ -212,14 +222,75 @@ jobs:
212222
- g++-5
213223
- libc6-dev-i386
214224
before_install:
215-
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
225+
- mkdir bin
226+
- ln -s /usr/bin/gcc-5 bin/gcc
227+
- ln -s /usr/bin/g++-5 bin/g++
216228
install:
217229
- ccache -z
218230
- ccache --max-size=1G
219231
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
220232
- cmake --build build -- -j4
221233
script: (cd build; ctest -V -L CORE -j2)
222234

235+
# cmake build using g++-7
236+
- stage: Test different OS/CXX/Flags
237+
os: linux
238+
compiler: gcc
239+
cache: ccache
240+
env:
241+
- BUILD_SYSTEM=cmake
242+
addons:
243+
apt:
244+
sources:
245+
- ubuntu-toolchain-r-test
246+
packages:
247+
- g++-7
248+
- libc6-dev-i386
249+
before_install:
250+
- mkdir bin
251+
- ln -s /usr/bin/gcc-7 bin/gcc
252+
- ln -s /usr/bin/g++-7 bin/g++
253+
install:
254+
- ccache -z
255+
- ccache --max-size=1G
256+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7'
257+
- cmake --build build -- -j4
258+
script: (cd build; ctest -V -L CORE -j2)
259+
260+
# cmake build using clang++-6
261+
- stage: Test different OS/CXX/Flags
262+
os: linux
263+
compiler: clang
264+
cache: ccache
265+
env:
266+
- BUILD_SYSTEM=cmake
267+
addons:
268+
apt:
269+
sources:
270+
- ubuntu-toolchain-r-test
271+
- llvm-toolchain-trusty-6.0
272+
packages:
273+
- libwww-perl
274+
- g++-5
275+
- clang-6.0
276+
- libstdc++-5-dev
277+
- libubsan0
278+
- parallel
279+
- libc6-dev-i386
280+
before_install:
281+
- mkdir bin
282+
# Use gcc/g++ 5 for tests, as Clang doesn't work yet
283+
# See https://github.com/diffblue/cbmc/issues/2370 for details.
284+
- ln -s /usr/bin/gcc-5 bin/gcc-5
285+
- ln -s /usr/bin/g++-5 bin/g++-5
286+
install:
287+
- ccache -z
288+
- ccache --max-size=1G
289+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-6.0' '-DCMAKE_CXX_FLAGS=-Qunused-arguments'
290+
- cmake --build build -- -j4
291+
script: (cd build; ctest -V -L CORE -j2)
292+
293+
# cmake build on OSX, using default clang
223294
- stage: Test different OS/CXX/Flags
224295
os: osx
225296
compiler: clang

‎cbmc/CHANGELOG

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
of --undefined-function-is-assume-false
77
* The --fixedbv command-line option has been removed
88
(it was marked deprecated in January 2017)
9+
* GOTO-INSTRUMENT: New option --print-global-state-size
910

1011

1112
5.8

‎cbmc/COMPILING.md

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -79,24 +79,23 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
7979

8080
1. As root, get the necessary development tools:
8181
```
82-
pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
83-
pkg install --accept developer/gcc/gcc-c++-5
82+
pkgadd -d http://get.opencsw.org/now
83+
/opt/csw/bin/pkgutil -U
84+
/opt/csw/bin/pkgutil -i gcc5g++ bison flex git
8485
```
8586
2. As a user, get the CBMC source via
8687
```
88+
export PATH=/opt/csw/bin:$PATH
8789
git clone https://github.com/diffblue/cbmc cbmc-git
8890
```
8991
3. Get MiniSat2 by entering
9092
```
91-
cd cbmc-git
92-
wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
93-
gtar xfz minisat_2.2.1.orig.tar.gz
94-
mv minisat2-2.2.1 minisat-2.2.1
95-
(cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
93+
cd cbmc-git/src
94+
gmake minisat2-download DOWNLOADER=wget TAR=gtar
9695
```
97-
4. Type
96+
4. To compile, type
9897
```
99-
cd src; gmake
98+
gmake
10099
```
101100
That should do it. To run, you will need
102101
```

‎cbmc/jbmc/regression/jbmc/json_trace3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Test.class
44
activate-multi-line-match
55
EXIT=0
66
SIGNAL=0
7-
"lhs": "dynamic_2_array\[1L\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "15",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "6"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
7+
"lhs": "dynamic_2_array\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "15",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "6"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
88
--
99
"name": "unknown"
1010
^warning: ignoring

‎cbmc/jbmc/unit/java_bytecode/java_types/erase_type_arguments.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,6 @@ SCENARIO("erase_type_arguments", "[core][java_types]")
6363
REQUIRE_THROWS_AS(
6464
erase_type_arguments(
6565
"testClassName<testTypeArgument1<testTypeArgument2>"),
66-
unsupported_java_class_signature_exceptiont &);
66+
unsupported_java_class_signature_exceptiont);
6767
}
6868
}

‎cbmc/regression/ansi-c/always_inline1/main.c

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
// this is a GCC extension
2+
3+
#ifdef __GNUC__
4+
static inline __attribute__((always_inline)) _Bool
5+
__is_kfree_rcu_offset(unsigned long offset)
6+
{
7+
return offset < 4096;
8+
}
9+
10+
static inline __attribute__((always_inline)) void
11+
kfree_rcu(unsigned long offset)
12+
{
13+
// immediate use of a constant as argument to __builtin_constant_p
14+
((void)sizeof(char[1 - 2 * !!(!__builtin_constant_p(offset))]));
15+
// inlining required to turn the array size into a compile-time constant
16+
((void)sizeof(char[1 - 2 * !!(!__is_kfree_rcu_offset(offset))]));
17+
}
18+
19+
static inline __attribute__((always_inline)) void unused(unsigned long offset)
20+
{
21+
// this would not be constant as it's never used, the front-end needs to
22+
// discard it
23+
((void)sizeof(char[1 - 2 * !!(!__builtin_constant_p(offset))]));
24+
}
25+
26+
// unused, but no 'static'
27+
inline __attribute__((__always_inline__)) int also_unused(int _c)
28+
{
29+
return _c;
30+
}
31+
#endif
32+
33+
int main()
34+
{
35+
#ifdef __GNUC__
36+
kfree_rcu(42);
37+
#endif
38+
39+
return 0;
40+
}

‎cbmc/regression/ansi-c/always_inline1/test.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
The static asserts (arrays that may have a negative size if the assertion fails)
11+
can only be evaluated if always_inline is correctly applied.

‎cbmc/regression/cbmc/Typecast2/main.c

Lines changed: 0 additions & 8 deletions
This file was deleted.

‎cbmc/regression/cbmc/Typecast2/main.i

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
unsigned int i=2;
4+
__CPROVER_assert(0l==(signed long int)(i - (unsigned int)2),
5+
"difference of cast");
6+
return 0;
7+
}

‎cbmc/regression/cbmc/Typecast2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
CORE
2-
main.c
2+
main.i
33
--no-propagation --64
44
^EXIT=0$
55
^SIGNAL=0$

‎cbmc/regression/cbmc/bounds_check1/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ main.c
33
--bounds-check --pointer-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[\(signed long( long)? int\)i2\]: FAILURE
7-
dest\[\(signed long( long)? int\)j2\]: FAILURE
8-
payload\[\(signed long( long)? int\)[kl]2\]: FAILURE
6+
\[\(.*\)i2\]: FAILURE
7+
dest\[\(.*\)j2\]: FAILURE
8+
payload\[\(.*\)[kl]2\]: FAILURE
99
\*\* 10 of 72 failed
1010
--
1111
^warning: ignoring
12-
\[\(signed long( long)? int\)i\]: FAILURE
13-
dest\[\(signed long( long)? int\)j\]: FAILURE
14-
payload\[\(signed long( long)? int\)[kl]\]: FAILURE
12+
\[\(.*\)i\]: FAILURE
13+
dest\[\(.*\)j\]: FAILURE
14+
payload\[\(.*\)[kl]\]: FAILURE

‎cbmc/regression/cbmc/goto5/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
3+
int main(void)
4+
{
5+
int r = 0;
6+
7+
if(r == 0)
8+
{
9+
goto l1;
10+
r = 1;
11+
}
12+
13+
l1:
14+
assert(r != 0); // expected to fail
15+
}

‎cbmc/regression/cbmc/goto5/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring

‎cbmc/regression/cpp/auto2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.cpp
3-
3+
-std=c++98
44
^EXIT=0$
55
^SIGNAL=0$
66
--

‎cbmc/regression/cpp/auto3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.cpp
3-
3+
-std=c++98
44
^EXIT=(64|1)$
55
^SIGNAL=0$
66
parse error

‎cbmc/regression/goto-analyzer/approx-array-variable-const-fp/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,17 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f2 THEN GOTO [0-9]$
6-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f3 THEN GOTO [0-9]$
7-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f4 THEN GOTO [0-9]$
5+
^\s*IF fp_tbl\[.*i\] == f2 THEN GOTO [0-9]$
6+
^\s*IF fp_tbl\[.*i\] == f3 THEN GOTO [0-9]$
7+
^\s*IF fp_tbl\[.*i\] == f4 THEN GOTO [0-9]$
88
^EXIT=0$
99
^SIGNAL=0$
1010
--
11-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f1 THEN GOTO [0-9]$
12-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f5 THEN GOTO [0-9]$
13-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f6 THEN GOTO [0-9]$
14-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f7 THEN GOTO [0-9]$
15-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f8 THEN GOTO [0-9]$
16-
^\s*IF fp_tbl\[\(signed (long )*long int\)i\] == f9 THEN GOTO [0-9]$
11+
^\s*IF fp_tbl\[.*i\] == f1 THEN GOTO [0-9]$
12+
^\s*IF fp_tbl\[.*i\] == f5 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[.*i\] == f6 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[.*i\] == f7 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[.*i\] == f8 THEN GOTO [0-9]$
16+
^\s*IF fp_tbl\[.*i\] == f9 THEN GOTO [0-9]$
1717
^warning: ignoring
1818
function \w+: replacing function pointer by 9 possible targets

‎cbmc/regression/goto-analyzer/no-match-dereference-const-pointer-const-array-literal-pointer-const-fp/test.desc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@ CORE
22
main.c
33
--show-goto-functions --verbosity 10 --pointer-check
44
^Removing function pointers and virtual functions$
5-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f1 THEN GOTO [0-9]$
6-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f2 THEN GOTO [0-9]$
7-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f3 THEN GOTO [0-9]$
8-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f4 THEN GOTO [0-9]$
9-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f5 THEN GOTO [0-9]$
10-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f6 THEN GOTO [0-9]$
11-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f7 THEN GOTO [0-9]$
12-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f8 THEN GOTO [0-9]$
13-
^\s*IF \*container_ptr->fp_tbl\[\(signed (long )*long int\)1\] == f9 THEN GOTO [0-9]$
5+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f1 THEN GOTO [0-9]$
6+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f2 THEN GOTO [0-9]$
7+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f3 THEN GOTO [0-9]$
8+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f4 THEN GOTO [0-9]$
9+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f5 THEN GOTO [0-9]$
10+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f6 THEN GOTO [0-9]$
11+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f7 THEN GOTO [0-9]$
12+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f8 THEN GOTO [0-9]$
13+
^\s*IF \*container_ptr->fp_tbl\[.*1\] == f9 THEN GOTO [0-9]$
1414
^EXIT=0$
1515
^SIGNAL=0$
1616
--

0 commit comments

Comments
 (0)