Skip to content

Commit bca7cf1

Browse files
JohnDumbellJohnDumbell
committed
Squashed 'cbmc/' changes from e6d196d..8a7893c
8a7893c Merge pull request diffblue#2375 from diffblue/unit-dependencies 9258284 fix build depenencies of unit test binary f7cd161 Merge pull request diffblue#2371 from diffblue/fix-tests2 82753bc make test independent of index type f5f32da Merge pull request diffblue#2364 from smowton/smowton/fix/autodetect-default-cxx-dialect d437f60 Merge pull request diffblue#2368 from polgreen/doc_replace_func_bodies 6048517 Merge pull request diffblue#2353 from tautschnig/g++8-fixes2 e2e6d82 Merge pull request diffblue#2190 from tautschnig/more-stats 7210136 Make it clearer that <=> will always be stringified 560f82b Travis: test more g++ and clang versions d46a55c Add new goto-instrument option print-global-state-size 961b29a Silence GCC 8's warning about using realloc/memmove on non-POD ca1b03c Documentation wording for replace function bodies d8c5a98 Cleanup options handling of count-eloc, list-eloc, print-path-lengths 6cd6d31 Unit test framwork: use references when catching exceptions 6882da6 Merge pull request diffblue#2367 from diffblue/fix-tests bcc3bef make regression/cbmc/bounds_check1 independent of types used 4de4538 switch regression/cbmc/Typecast2 to preprocessed code 91a9c64 Amend two tests that explicitly target C++98 2b2b797 goto-gcc: select default language standard depending on emulated compiler 52a8afc Merge pull request diffblue#1898 from tautschnig/always-inline cbe691b Merge pull request diffblue#2363 from diffblue/Makefile-TAR 9d40a9e Merge pull request diffblue#2365 from diffblue/solaris_errno 9efd705 add model for ___errno for Solaris 11 eaa2e05 update Solaris instructions 2f142d5 allow customizing the tar command for solver download 8cc1848 Merge pull request diffblue#1860 from tautschnig/restore-irept-sharing fea5db0 Merge pull request diffblue#2361 from diffblue/fix-goto2 7c0d750 Merge pull request diffblue#2362 from smowton/smowton/fix/tolerate-cxx-namespace-attribute e440a25 introduce INCOMPLETE_GOTO and turn guarded goto into a stateless pass 1f1835b C++ frontend: tolerate namespace attributes cbce4bc Unit test of irept's public API abdb044 Unit test to check that irept implements sharing d58fd18 Silence the linter on assert in irep.h 3d64070 Partially revert "Use small intrusive pointer in irep" 688a0ab Macros are not needed outside translation units 9c93f59 Fully interpret __attribute__((always_inline)) d1f617b Apply symbol replacement in type_arg members git-subtree-dir: cbmc git-subtree-split: 8a7893c
1 parent c99cba2 commit bca7cf1

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

+1034
-267
lines changed

‎.travis.yml

+76-5
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

‎CHANGELOG

+1
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

‎COMPILING.md

+8-9
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
```

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

+1-1
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

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

+1-1
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
}

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

+40
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+
}

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

+11
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.

‎regression/cbmc/Typecast2/main.c

-8
This file was deleted.

‎regression/cbmc/Typecast2/main.i

+7
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+
}

‎regression/cbmc/Typecast2/test.desc

+1-1
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$

‎regression/cbmc/bounds_check1/test.desc

+6-6
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

‎regression/cbmc/goto5/main.c

+15
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+
}

‎regression/cbmc/goto5/test.desc

+8
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

‎regression/cpp/auto2/test.desc

+1-1
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
--

‎regression/cpp/auto3/test.desc

+1-1
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

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

+9-9
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

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

+9-9
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)