@@ -112,9 +112,9 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
112
112
113
113
inline void * malloc (__CPROVER_size_t malloc_size )
114
114
{
115
- __CPROVER_HIDE :;
116
115
// realistically, malloc may return NULL,
117
116
// but we only do so if `--malloc-may-fail` is set
117
+ __CPROVER_HIDE :;
118
118
119
119
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool ();
120
120
if (__CPROVER_malloc_may_fail && should_malloc_fail )
@@ -124,17 +124,20 @@ inline void *malloc(__CPROVER_size_t malloc_size)
124
124
malloc_res = __CPROVER_allocate (malloc_size , 0 );
125
125
126
126
// make sure it's not recorded as deallocated
127
- __CPROVER_deallocated = (malloc_res == __CPROVER_deallocated )?0 :__CPROVER_deallocated ;
127
+ __CPROVER_deallocated =
128
+ (malloc_res == __CPROVER_deallocated ) ? 0 : __CPROVER_deallocated ;
128
129
129
130
// record the object size for non-determistic bounds checking
130
- __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool ();
131
- __CPROVER_malloc_object = record_malloc ?malloc_res :__CPROVER_malloc_object ;
132
- __CPROVER_malloc_size = record_malloc ?malloc_size :__CPROVER_malloc_size ;
133
- __CPROVER_malloc_is_new_array = record_malloc ?0 :__CPROVER_malloc_is_new_array ;
131
+ __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool ();
132
+ __CPROVER_malloc_object =
133
+ record_malloc ? malloc_res : __CPROVER_malloc_object ;
134
+ __CPROVER_malloc_size = record_malloc ? malloc_size : __CPROVER_malloc_size ;
135
+ __CPROVER_malloc_is_new_array =
136
+ record_malloc ? 0 : __CPROVER_malloc_is_new_array ;
134
137
135
138
// detect memory leaks
136
- __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool ();
137
- __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak ;
139
+ __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool ();
140
+ __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak ;
138
141
139
142
return malloc_res ;
140
143
}
0 commit comments