Skip to content

Commit b95383a

Browse files
author
Daniel Kroening
committed
Merge branch 'develop' of github.com:diffblue/cbmc into develop
2 parents e7bb127 + f20e8d7 commit b95383a

36 files changed

+495
-474
lines changed

‎.travis.yml

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ jobs:
6666
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
6767
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
6868
env:
69-
- COMPILER="ccache g++-5"
69+
- COMPILER="ccache /usr/bin/g++-5"
7070
- EXTRA_CXXFLAGS="-D_GLIBCXX_DEBUG"
7171

7272
# OS X using g++
@@ -76,10 +76,8 @@ jobs:
7676
compiler: gcc
7777
cache: ccache
7878
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
8179
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
82-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
80+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
8381
env: COMPILER="ccache g++"
8482

8583
# OS X using clang++
@@ -90,7 +88,7 @@ jobs:
9088
cache: ccache
9189
before_install:
9290
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
93-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
91+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
9492
env:
9593
- COMPILER="ccache clang++ -Qunused-arguments -fcolor-diagnostics"
9694
- CCACHE_CPP2=yes
@@ -113,7 +111,7 @@ jobs:
113111
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
114112
# env: COMPILER=g++-5 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover -fno-omit-frame-pointer"
115113
env:
116-
- COMPILER="ccache g++-5"
114+
- COMPILER="ccache /usr/bin/g++-5"
117115
- EXTRA_CXXFLAGS="-DDEBUG"
118116
script: echo "Not running any tests for a debug build."
119117

@@ -138,7 +136,7 @@ jobs:
138136
- export CCACHE_CPP2=yes
139137
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
140138
env:
141-
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
139+
- COMPILER="ccache /usr/bin/clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
142140
- CCACHE_CPP2=yes
143141
- EXTRA_CXXFLAGS="-DNDEBUG"
144142

@@ -163,14 +161,15 @@ jobs:
163161
- export CCACHE_CPP2=yes
164162
# env: COMPILER=clang++-3.7 SAN_FLAGS="-fsanitize=undefined -fno-sanitize-recover=undefined,integer -fno-omit-frame-pointer"
165163
env:
166-
- COMPILER="ccache clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
164+
- COMPILER="ccache /usr/bin/clang++-3.7 -Qunused-arguments -fcolor-diagnostics"
167165
- CCACHE_CPP2=yes
168166
- EXTRA_CXXFLAGS="-DDEBUG -DUSE_STD_STRING"
169167
script: echo "Not running any tests for a debug build."
170168

171169
# cmake build using g++-5
172170
- stage: Test different OS/CXX/Flags
173171
os: linux
172+
compiler: gcc
174173
cache: ccache
175174
env:
176175
- BUILD_SYSTEM=cmake
@@ -180,19 +179,22 @@ jobs:
180179
- ubuntu-toolchain-r-test
181180
packages:
182181
- g++-5
182+
before_install:
183+
- mkdir bin ; ln -s /usr/bin/gcc-5 bin/gcc
183184
install:
184185
- ccache -z
185186
- ccache --max-size=1G
186-
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=g++-5'
187+
- cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-5'
187188
- cmake --build build -- -j4
188189
script: (cd build; ctest -V -L CORE -j2)
189190

190191
- stage: Test different OS/CXX/Flags
191192
os: osx
193+
compiler: clang
192194
cache: ccache
193195
before_install:
194196
- HOMEBREW_NO_AUTO_UPDATE=1 brew install ccache
195-
- export PATH=/usr/local/opt/ccache/libexec:$PATH
197+
- export PATH=$PATH:/usr/local/opt/ccache/libexec
196198
env:
197199
- BUILD_SYSTEM=cmake
198200
- CCACHE_CPP2=yes
@@ -247,11 +249,11 @@ jobs:
247249

248250
install:
249251
- ccache -z
250-
- ccache --max-size=1G
252+
- ccache --max-size=2G
251253
- make -C src minisat2-download
252254
- make -C src/ansi-c library_check
253-
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2
254-
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j2 clobber.dir memory-models.dir
255+
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j3
256+
- make -C src "CXX=${COMPILER}" "CXXFLAGS=-Wall -Werror -pedantic -O2 -g ${EXTRA_CXXFLAGS}" -j3 clobber.dir memory-models.dir
255257

256258
script:
257259
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;

‎CODEOWNERS

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,8 @@ 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

‎regression/cbmc/fgets1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\[main.assertion.3\] assertion p\[1\]=='b': FAILURE
8-
\*\* 1 of \d+ failed
8+
\*\* 2 of \d+ failed
99
--
1010
^warning: ignoring

‎regression/cbmc/read1/main.c

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
#ifdef _WIN32
2+
#include <io.h>
3+
#else
4+
#include <unistd.h>
5+
#endif
6+
7+
#include <stdio.h>
8+
9+
int main()
10+
{
11+
char data[20];
12+
13+
if(read(0, data, 100) < 0)
14+
printf("An error has occurred");
15+
else
16+
printf("Read occurred");
17+
18+
return 0;
19+
}

‎regression/cbmc/read1/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--bounds-check --pointer-check --unwind 100
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
\[.*] dereference failure: pointer outside object bounds in .*: FAILURE
8+
\*\* 1 of .* failed \(.*\)
9+
--
10+
^warning: ignoring

‎regression/cbmc/return6/f_def.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
unsigned f()
2+
{
3+
return 0x34;
4+
}

‎regression/cbmc/return6/main.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
// Do not declare f().
4+
// This is invalid from C99 upwards, but kind of ok before.
5+
6+
int main()
7+
{
8+
int return_value;
9+
return_value=f();
10+
assert(return_value==0x34);
11+
}

‎regression/cbmc/return6/test.desc

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

‎src/analyses/invariant_propagation.cpp

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -173,10 +173,13 @@ void invariant_propagationt::get_globals(
173173
object_listt &dest)
174174
{
175175
// static ones
176-
forall_symbols(it, ns.get_symbol_table().symbols)
177-
if(it->second.is_lvalue &&
178-
it->second.is_static_lifetime)
179-
get_objects(it->second, dest);
176+
for(const auto &symbol_pair : ns.get_symbol_table().symbols)
177+
{
178+
if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
179+
{
180+
get_objects(symbol_pair.second, dest);
181+
}
182+
}
180183
}
181184

182185
bool invariant_propagationt::check_type(const typet &type) const

‎src/ansi-c/library/stdio.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -247,6 +247,9 @@ char *fgets(char *str, int size, FILE *stream)
247247
{
248248
int str_length=__VERIFIER_nondet_int();
249249
__CPROVER_assume(str_length>=0 && str_length<size);
250+
// check that the memory is accessible
251+
(void)*(char *)str;
252+
(void)*(((const char *)str) + str_length - 1);
250253
char contents_nondet[str_length];
251254
__CPROVER_array_replace(str, contents_nondet);
252255
if(!error)

‎src/ansi-c/library/unistd.c

Lines changed: 43 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -123,27 +123,30 @@ inline int _close(int fildes)
123123
// write to _write; this is covered by the explicit definition of
124124
// _write below
125125
#ifdef _MSC_VER
126-
#define ssize_t signed long
126+
#define ret_type int
127+
#define size_type unsigned
127128
#else
128129
#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
129130
#include <sys/types.h>
130131
#define __CPROVER_SYS_TYPES_H_INCLUDED
131132
#endif
133+
#define ret_type ssize_t
134+
#define size_type size_t
132135
#endif
133136

134137
extern struct __CPROVER_pipet __CPROVER_pipes[];
135138
// offset to make sure we don't collide with other fds
136139
extern const int __CPROVER_pipe_offset;
137140

138-
ssize_t __VERIFIER_nondet_ssize_t();
141+
ret_type __VERIFIER_nondet_ret_type();
139142

140-
ssize_t write(int fildes, const void *buf, size_t nbyte)
143+
ret_type write(int fildes, const void *buf, size_type nbyte)
141144
{
142145
__CPROVER_HIDE:;
143146
if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
144147
{
145-
ssize_t retval=__VERIFIER_nondet_ssize_t();
146-
__CPROVER_assume(retval>=-1 && retval<=(ssize_t)nbyte);
148+
ret_type retval=__VERIFIER_nondet_ret_type();
149+
__CPROVER_assume(retval>=-1 && retval<=(ret_type)nbyte);
147150
return retval;
148151
}
149152

@@ -156,7 +159,7 @@ ssize_t write(int fildes, const void *buf, size_t nbyte)
156159
sizeof(__CPROVER_pipes[fildes].data) >=
157160
__CPROVER_pipes[fildes].next_avail+nbyte)
158161
{
159-
for(size_t i=0; i<nbyte; ++i)
162+
for(size_type i=0; i<nbyte; ++i)
160163
__CPROVER_pipes[fildes].data[i+__CPROVER_pipes[fildes].next_avail]=
161164
((char*)buf)[i];
162165
__CPROVER_pipes[fildes].next_avail+=nbyte;
@@ -169,17 +172,20 @@ ssize_t write(int fildes, const void *buf, size_t nbyte)
169172
/* FUNCTION: _write */
170173

171174
#ifdef _MSC_VER
172-
#define ssize_t signed long
175+
#define ret_type int
176+
#define size_type unsigned
173177
#else
174178
#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
175179
#include <sys/types.h>
176180
#define __CPROVER_SYS_TYPES_H_INCLUDED
177181
#endif
182+
#define ret_type ssize_t
183+
#define size_type size_t
178184
#endif
179185

180-
ssize_t write(int fildes, const void *buf, size_t nbyte);
186+
ret_type write(int fildes, const void *buf, size_type nbyte);
181187

182-
inline ssize_t _write(int fildes, const void *buf, size_t nbyte)
188+
inline ret_type _write(int fildes, const void *buf, size_type nbyte)
183189
{
184190
__CPROVER_HIDE:;
185191
return write(fildes, buf, nbyte);
@@ -191,42 +197,54 @@ inline ssize_t _write(int fildes, const void *buf, size_t nbyte)
191197
// read to _read; this is covered by the explicit definition of _read
192198
// below
193199
#ifdef _MSC_VER
194-
#define ssize_t signed long
200+
#define ret_type int
201+
#define size_type unsigned
195202
#else
196203
#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
197204
#include <sys/types.h>
198205
#define __CPROVER_SYS_TYPES_H_INCLUDED
199206
#endif
207+
#define ret_type ssize_t
208+
#define size_type size_t
200209
#endif
201210

202211
extern struct __CPROVER_pipet __CPROVER_pipes[];
203212
// offset to make sure we don't collide with other fds
204213
extern const int __CPROVER_pipe_offset;
205214

206215
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
207-
ssize_t __VERIFIER_nondet_ssize_t();
216+
ret_type __VERIFIER_nondet_ret_type();
217+
size_type __VERIFIER_nondet_size_type();
208218

209-
ssize_t read(int fildes, void *buf, size_t nbyte)
219+
ret_type read(int fildes, void *buf, size_type nbyte)
210220
{
211221
__CPROVER_HIDE:;
212222
if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset)
213223
{
214-
ssize_t nread=__VERIFIER_nondet_ssize_t();
215-
__CPROVER_assume(0<=nread && (size_t)nread<=nbyte);
224+
ret_type nread=__VERIFIER_nondet_ret_type();
225+
__CPROVER_assume(0<=nread && (size_type)nread<=nbyte);
216226

227+
__CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
217228
#if 0
218-
size_t i;
229+
size_type i;
219230
for(i=0; i<nbyte; i++)
220231
{
221232
char nondet_char;
222233
((char *)buf)[i]=nondet_char;
223234
}
224235
#else
225-
char nondet_bytes[nbyte];
226-
__CPROVER_array_replace((char*)buf, nondet_bytes);
236+
if(nbyte>0)
237+
{
238+
size_type str_length=__VERIFIER_nondet_size_type();
239+
__CPROVER_assume(error ? str_length<=nbyte : str_length==nbyte);
240+
// check that the memory is accessible
241+
(void)*(char *)buf;
242+
(void)*(((const char *)buf) + str_length - 1);
243+
char contents_nondet[str_length];
244+
__CPROVER_array_replace((char*)buf, contents_nondet);
245+
}
227246
#endif
228247

229-
__CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
230248
return error ? -1 : nread;
231249
}
232250

@@ -237,7 +255,7 @@ ssize_t read(int fildes, void *buf, size_t nbyte)
237255
__CPROVER_atomic_begin();
238256
if(!__CPROVER_pipes[fildes].widowed)
239257
{
240-
for(size_t i=0; i<nbyte &&
258+
for(size_type i=0; i<nbyte &&
241259
__CPROVER_pipes[fildes].next_unread <
242260
__CPROVER_pipes[fildes].next_avail;
243261
++i)
@@ -258,17 +276,20 @@ ssize_t read(int fildes, void *buf, size_t nbyte)
258276
/* FUNCTION: _read */
259277

260278
#ifdef _MSC_VER
261-
#define ssize_t signed long
279+
#define ret_type int
280+
#define size_type unsigned
262281
#else
263282
#ifndef __CPROVER_SYS_TYPES_H_INCLUDED
264283
#include <sys/types.h>
265284
#define __CPROVER_SYS_TYPES_H_INCLUDED
266285
#endif
286+
#define ret_type ssize_t
287+
#define size_type size_t
267288
#endif
268289

269-
ssize_t read(int fildes, void *buf, size_t nbyte);
290+
ret_type read(int fildes, void *buf, size_type nbyte);
270291

271-
inline ssize_t _read(int fildes, void *buf, size_t nbyte)
292+
inline ret_type _read(int fildes, void *buf, size_type nbyte)
272293
{
273294
__CPROVER_HIDE:;
274295
return read(fildes, buf, nbyte);

0 commit comments

Comments
 (0)