Skip to content

Commit be6883a

Browse files
committed
Malloc should fail on too large allocations
This adds a simple test into the builtin stdlib.c implementation of `malloc`. Also the converter input is now a dependency (in the CMake build).
1 parent be84cd1 commit be6883a

File tree

4 files changed

+24
-1
lines changed

4 files changed

+24
-1
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
#include <stdint.h>
3+
#include <stdlib.h>
4+
5+
int main()
6+
{
7+
int *p = malloc(SIZE_MAX);
8+
assert(p);
9+
10+
return 0;
11+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[main.assertion.\d+\] line \d+ assertion p: FAILURE$
7+
^VERIFICATION FAILED$
8+
--
9+
^warning: ignoring

src/ansi-c/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ endforeach()
1313

1414
add_custom_command(OUTPUT "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
1515
COMMAND converter < ${converter_input_path} > "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
16-
DEPENDS converter
16+
DEPENDS converter ${converter_input_path}
1717
)
1818

1919
add_executable(file_converter file_converter.cpp)

src/ansi-c/library/stdlib.c

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,6 +115,9 @@ inline void *malloc(__CPROVER_size_t malloc_size)
115115
// realistically, malloc may return NULL,
116116
// and __CPROVER_allocate doesn't, but no one cares
117117
__CPROVER_HIDE:;
118+
// 8 is the default object bits for ANSI-C and C++
119+
if (malloc_size >= ((__CPROVER_size_t)1<<(64-8)))
120+
return (void*)0;
118121
void *malloc_res;
119122
malloc_res = __CPROVER_allocate(malloc_size, 0);
120123

0 commit comments

Comments
 (0)