CBMC
Loading...
Searching...
No Matches
allocainc.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Big Integers
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
9// Whatever is necessary to use alloca().
10
11#ifndef CPROVER_BIG_INT_ALLOCAINC_H
12#define CPROVER_BIG_INT_ALLOCAINC_H
13
14// clang-format off
15#if defined linux || defined __linux__ \
16 || defined __sun \
17 || defined UWIN \
18 || defined osf1 \
19 || defined __MACH__ \
20 || defined __CYGWIN__ \
21 || defined __EMSCRIPTEN__
22// clang-format on
23
24# include <alloca.h>
25
26#elif defined _MSC_VER \
27 || defined __BORLANDC__ \
28 || defined __MINGW32__
29
30# include <malloc.h>
31
32#elif defined __vax
33
34// In vax-alloca.mar.
35extern "C" void *alloca (unsigned);
36
37#elif defined __VMS
38
39// DEC CXX on VMS alpha.
40# include <builtins.h>
41# define alloca(N) __ALLOCA(N)
42
43#elif defined __xlC__
44
45# pragma alloca
46# include <stdlib.h>
47
48#elif defined __FCC__
49
50# define alloca(X) __builtin_alloca(X)
51
52#elif defined __FreeBSD__ || defined __FreeBSD_kernel__ || \
53 defined __OpenBSD__ || defined __NetBSD__
54
55# include <stdlib.h>
56
57#endif
58
59
60#endif // CPROVER_BIG_INT_ALLOCAINC_H
void * alloca(__CPROVER_size_t alloca_size)
Definition stdlib.c:297