File tree Expand file tree Collapse file tree 1 file changed +6
-1
lines changed Expand file tree Collapse file tree 1 file changed +6
-1
lines changed Original file line number Diff line number Diff line change @@ -75,6 +75,10 @@ __CPROVER_HIDE:;
75
75
__CPROVER_size_t alloc_size = nmemb * size ;
76
76
#pragma CPROVER check pop
77
77
78
+ __CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool ();
79
+ if (__CPROVER_malloc_may_fail && should_malloc_fail )
80
+ return (void * )0 ;
81
+
78
82
void * malloc_res ;
79
83
// realistically, calloc may return NULL,
80
84
// and __CPROVER_allocate doesn't, but no one cares
@@ -430,7 +434,8 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
430
434
// this shouldn't move if the new size isn't bigger
431
435
void * res ;
432
436
res = malloc (malloc_size );
433
- __CPROVER_array_copy (res , ptr );
437
+ if (res != (void * )0 )
438
+ __CPROVER_array_copy (res , ptr );
434
439
free (ptr );
435
440
436
441
return res ;
You can’t perform that action at this time.
0 commit comments