diff options
Diffstat (limited to 'runtime/calloc.c')
-rw-r--r-- | runtime/calloc.c | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/runtime/calloc.c b/runtime/calloc.c new file mode 100644 index 00000000..2526cebf --- /dev/null +++ b/runtime/calloc.c @@ -0,0 +1,13 @@ +#include <stdio.h> +#include <stddef.h> +#include <stdlib.h> + +void * compcert_alloc(int sz) +{ + void * res = malloc(sz); + if (res == NULL) { + fprintf(stderr, "Out of memory in compcert_alloc().\n"); + abort(); + } + return res; +} |