Skip to content

Commit 390880e

Browse files
committed
Updates posix_memalign to consider malloc may fail
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 94fb414 commit 390880e

File tree

1 file changed

+7
-14
lines changed

1 file changed

+7
-14
lines changed

src/ansi-c/library/stdlib.c

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -525,20 +525,13 @@ __CPROVER_HIDE:;
525525
// As _mid_memalign simplifies for alignment <= MALLOC_ALIGNMENT
526526
// to a malloc call, it should be sound, if we do it too.
527527

528-
// The original posix_memalign check on the pointer is:
529-
530-
// void *tmp = malloc(size);
531-
// if(tmp != NULL){
532-
// *ptr = tmp;
533-
// return 0;
534-
// }
535-
// return ENOMEM;
536-
537-
// As _CPROVER_allocate used in malloc never returns null,
538-
// this check is not applicable and can be simplified:
539-
540-
*ptr = malloc(size);
541-
return 0;
528+
void *tmp = malloc(size);
529+
if(tmp != (void *)0)
530+
{
531+
*ptr = tmp;
532+
return 0;
533+
}
534+
return ENOMEM;
542535
}
543536

544537
/* FUNCTION: random */

0 commit comments

Comments
 (0)