Skip to content

Commit 7b5dd17

Browse files
tautschnigtautschnig
authored
Merge pull request #1834 from diffblue/library-preconditions
Library preconditions
2 parents ef08ae2 + f6f45fc commit 7b5dd17

File tree

7 files changed

+200
-122
lines changed

7 files changed

+200
-122
lines changed

‎regression/cbmc/strcat1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\[main.assertion.6\] assertion strlen\(A3\) == 4: FAILURE
8-
\*\* 1 of 8 failed
8+
\*\* 1 of 9 failed
99
--
1010
^warning: ignoring

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

+10-7
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
1212
in_addr_t inet_addr(const char *cp)
1313
{
1414
__CPROVER_HIDE:;
15-
(void)*cp;
1615
#ifdef __CPROVER_STRING_ABSTRACTION
17-
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument");
16+
__CPROVER_precondition(__CPROVER_is_zero_string(cp),
17+
"inet_addr zero-termination of argument");
1818
#endif
19+
(void)*cp;
1920

2021
in_addr_t result=__VERIFIER_nondet_in_addr_t();
2122
return result;
@@ -37,11 +38,12 @@ int __VERIFIER_nondet_int();
3738
int inet_aton(const char *cp, struct in_addr *pin)
3839
{
3940
__CPROVER_HIDE:;
40-
(void)*cp;
41-
(void)*pin;
4241
#ifdef __CPROVER_STRING_ABSTRACTION
43-
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument");
42+
__CPROVER_precondition(__CPROVER_is_zero_string(cp),
43+
"inet_aton zero-termination of name argument");
4444
#endif
45+
(void)*cp;
46+
(void)*pin;
4547

4648
int result=__VERIFIER_nondet_int();
4749
return result;
@@ -63,10 +65,11 @@ in_addr_t __VERIFIER_nondet_in_addr_t();
6365
in_addr_t inet_network(const char *cp)
6466
{
6567
__CPROVER_HIDE:;
66-
(void)*cp;
6768
#ifdef __CPROVER_STRING_ABSTRACTION
68-
__CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument");
69+
__CPROVER_precondition(__CPROVER_is_zero_string(cp),
70+
"inet_network zero-termination of name argument");
6971
#endif
72+
(void)*cp;
7073

7174
in_addr_t result=__VERIFIER_nondet_in_addr_t();
7275
return result;

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

+3-2
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,11 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
77
struct hostent *gethostbyname(const char *name)
88
{
99
__CPROVER_HIDE:;
10-
(void)*name;
1110
#ifdef __CPROVER_STRING_ABSTRACTION
12-
__CPROVER_assert(__CPROVER_is_zero_string(name), "gethostbyname zero-termination of name argument");
11+
__CPROVER_precondition(__CPROVER_is_zero_string(name),
12+
"gethostbyname zero-termination of name argument");
1313
#endif
14+
(void)*name;
1415

1516
__CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool();
1617
if(error) return 0;

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

+33-28
Original file line numberDiff line numberDiff line change
@@ -72,30 +72,32 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
7272
inline void __delete(void *ptr)
7373
{
7474
__CPROVER_HIDE:;
75+
// is it dynamic?
76+
__CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
77+
"delete argument must be dynamic object");
78+
__CPROVER_precondition(__CPROVER_POINTER_OFFSET(ptr)==0,
79+
"delete argument must have offset zero");
80+
81+
// catch double delete
82+
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
83+
84+
// catch people who call delete for objects allocated with new[]
85+
__CPROVER_precondition(ptr==0 ||
86+
__CPROVER_malloc_object!=ptr ||
87+
!__CPROVER_malloc_is_new_array,
88+
"delete of array object");
89+
7590
// If ptr is NULL, no operation is performed.
7691
// This is a requirement by the standard, not generosity!
7792
if(ptr!=0)
7893
{
79-
// is it dynamic?
80-
__CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
81-
"delete argument must be dynamic object");
82-
__CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
83-
"delete argument must have offset zero");
84-
85-
// catch double delete
86-
__CPROVER_assert(__CPROVER_deallocated!=ptr, "double delete");
87-
88-
// catch people who call delete for objects allocated with new[]
89-
__CPROVER_assert(__CPROVER_malloc_object!=ptr ||
90-
!__CPROVER_malloc_is_new_array,
91-
"delete of array object");
92-
9394
// non-deterministically record as deallocated
9495
__CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
9596
__CPROVER_deallocated=record?ptr:__CPROVER_deallocated;
9697

9798
// detect memory leaks
98-
if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
99+
if(__CPROVER_memory_leak==ptr)
100+
__CPROVER_memory_leak=0;
99101
}
100102
}
101103

@@ -108,22 +110,25 @@ inline void __delete_array(void *ptr)
108110
__CPROVER_HIDE:;
109111
// If ptr is NULL, no operation is performed.
110112
// This is a requirement by the standard, not generosity!
111-
if(ptr!=0)
112-
{
113-
// is it dynamic?
114-
__CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
115-
"delete argument must be dynamic object");
116-
__CPROVER_assert(__CPROVER_POINTER_OFFSET(ptr)==0,
117-
"delete argument must have offset zero");
118113

119-
// catch double delete
120-
__CPROVER_assert(__CPROVER_deallocated!=ptr, "double delete");
114+
// is it dynamic?
115+
__CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
116+
"delete argument must be dynamic object");
117+
__CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
118+
"delete argument must have offset zero");
121119

122-
// catch people who call delete[] for objects allocated with new
123-
__CPROVER_assert(__CPROVER_malloc_object!=ptr ||
124-
__CPROVER_malloc_is_new_array,
125-
"delete[] of non-array object");
120+
// catch double delete
121+
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
122+
"double delete");
126123

124+
// catch people who call delete[] for objects allocated with new
125+
__CPROVER_precondition(ptr==0 ||
126+
__CPROVER_malloc_object!=ptr ||
127+
__CPROVER_malloc_is_new_array,
128+
"delete[] of non-array object");
129+
130+
if(ptr!=0)
131+
{
127132
// non-deterministically record as deallocated
128133
__CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
129134
__CPROVER_deallocated=record?ptr:__CPROVER_deallocated;

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

+18-16
Original file line numberDiff line numberDiff line change
@@ -162,24 +162,26 @@ inline void free(void *ptr)
162162
__CPROVER_precondition(ptr==0 || __CPROVER_POINTER_OFFSET(ptr)==0,
163163
"free argument has offset zero");
164164

165-
if(ptr!=0)
166-
{
167-
// catch double free
168-
if(__CPROVER_deallocated==ptr)
169-
__CPROVER_assert(0, "double free");
165+
// catch double free
166+
__CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr,
167+
"double free");
170168

171-
// catch people who try to use free(...) for stuff
172-
// allocated with new[]
173-
__CPROVER_assert(__CPROVER_malloc_object!=ptr ||
174-
!__CPROVER_malloc_is_new_array,
175-
"free called for new[] object");
169+
// catch people who try to use free(...) for stuff
170+
// allocated with new[]
171+
__CPROVER_precondition(ptr==0 ||
172+
__CPROVER_malloc_object!=ptr ||
173+
!__CPROVER_malloc_is_new_array,
174+
"free called for new[] object");
176175

176+
if(ptr!=0)
177+
{
177178
// non-deterministically record as deallocated
178179
__CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool();
179180
if(record) __CPROVER_deallocated=ptr;
180181

181182
// detect memory leaks
182-
if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0;
183+
if(__CPROVER_memory_leak==ptr)
184+
__CPROVER_memory_leak=0;
183185
}
184186
}
185187

@@ -206,7 +208,7 @@ inline long strtol(const char *nptr, char **endptr, int base)
206208
{
207209
__CPROVER_HIDE:;
208210
#ifdef __CPROVER_STRING_ABSTRACTION
209-
__CPROVER_assert(__CPROVER_is_zero_string(nptr),
211+
__CPROVER_precondition(__CPROVER_is_zero_string(nptr),
210212
"zero-termination of argument of strtol");
211213
#endif
212214

@@ -329,7 +331,7 @@ inline char *getenv(const char *name)
329331

330332
(void)*name;
331333
#ifdef __CPROVER_STRING_ABSTRACTION
332-
__CPROVER_assert(__CPROVER_is_zero_string(name),
334+
__CPROVER_precondition(__CPROVER_is_zero_string(name),
333335
"zero-termination of argument of getenv");
334336
#endif
335337

@@ -367,6 +369,9 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
367369
{
368370
__CPROVER_HIDE:;
369371

372+
__CPROVER_precondition(ptr==0 || __CPROVER_DYNAMIC_OBJECT(ptr),
373+
"realloc argument is dynamic object");
374+
370375
// if ptr is NULL, this behaves like malloc
371376
if(ptr==0)
372377
return malloc(malloc_size);
@@ -379,9 +384,6 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
379384
return malloc(1);
380385
}
381386

382-
__CPROVER_assert(__CPROVER_DYNAMIC_OBJECT(ptr),
383-
"realloc argument is dynamic object");
384-
385387
// this shouldn't move if the new size isn't bigger
386388
void *res;
387389
res=malloc(malloc_size);

0 commit comments

Comments
 (0)