Skip to content

Commit 241b666

Browse files
committed
Extend changes to calloc and handle in realloc
the fact that malloc may now fail.
1 parent c7e0e4a commit 241b666

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/ansi-c/library/stdlib.c

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,10 @@ __CPROVER_HIDE:;
7575
__CPROVER_size_t alloc_size = nmemb * size;
7676
#pragma CPROVER check pop
7777

78+
__CPROVER_bool should_malloc_fail = __VERIFIER_nondet___CPROVER_bool();
79+
if(__CPROVER_malloc_may_fail && should_malloc_fail)
80+
return (void *)0;
81+
7882
void *malloc_res;
7983
// realistically, calloc may return NULL,
8084
// and __CPROVER_allocate doesn't, but no one cares
@@ -430,7 +434,8 @@ inline void *realloc(void *ptr, __CPROVER_size_t malloc_size)
430434
// this shouldn't move if the new size isn't bigger
431435
void *res;
432436
res=malloc(malloc_size);
433-
__CPROVER_array_copy(res, ptr);
437+
if(res != (void *)0)
438+
__CPROVER_array_copy(res, ptr);
434439
free(ptr);
435440

436441
return res;

0 commit comments

Comments
 (0)