diff options
Diffstat (limited to 'runtime/calloc.c')
| -rw-r--r-- | runtime/calloc.c | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/runtime/calloc.c b/runtime/calloc.c deleted file mode 100644 index 8e5e0b6..0000000 --- a/runtime/calloc.c +++ /dev/null @@ -1,28 +0,0 @@ -/* *********************************************************************/ -/* */ -/* The Compcert verified compiler */ -/* */ -/* Xavier Leroy, INRIA Paris-Rocquencourt */ -/* */ -/* Copyright Institut National de Recherche en Informatique et en */ -/* Automatique. All rights reserved. This file is distributed */ -/* under the terms of the GNU General Public License as published by */ -/* the Free Software Foundation, either version 2 of the License, or */ -/* (at your option) any later version. This file is also distributed */ -/* under the terms of the INRIA Non-Commercial License Agreement. */ -/* */ -/* *********************************************************************/ - -#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; -} |