diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:29:08 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-04 09:29:08 +0000 |
commit | ba9cd4f93ef991fa3794d333e8da19878df06e2d (patch) | |
tree | d0870ebda361f8f07f930053403d832473824e6b /runtime/calloc.c | |
parent | 601569c2e0c9ec4748eefcbdb9f62c93f8aa822c (diff) |
Simplified stdlib wrapper; use it only under MacOS X
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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; -} |