mirror of
https://github.com/Z3Prover/z3
synced 2025-12-12 14:46:22 +00:00
60 lines
2.1 KiB
C
60 lines
2.1 KiB
C
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
|
|
Licensed under the Apache 2.0 License. */
|
|
|
|
#ifndef __KREMLIN_TARGET_H
|
|
#define __KREMLIN_TARGET_H
|
|
|
|
#include <stdlib.h>
|
|
#include <inttypes.h>
|
|
#include <limits.h>
|
|
|
|
/******************************************************************************/
|
|
/* Macros that KreMLin will generate. */
|
|
/******************************************************************************/
|
|
|
|
/* For "bare" targets that do not have a C stdlib, the user might want to use
|
|
* [-add-early-include '"mydefinitions.h"'] and override these. */
|
|
#ifndef KRML_HOST_PRINTF
|
|
# define KRML_HOST_PRINTF printf
|
|
#endif
|
|
|
|
#ifndef KRML_HOST_EXIT
|
|
# define KRML_HOST_EXIT exit
|
|
#endif
|
|
|
|
#ifndef KRML_HOST_MALLOC
|
|
# define KRML_HOST_MALLOC malloc
|
|
#endif
|
|
|
|
#ifndef KRML_HOST_CALLOC
|
|
# define KRML_HOST_CALLOC calloc
|
|
#endif
|
|
|
|
#ifndef KRML_HOST_FREE
|
|
# define KRML_HOST_FREE free
|
|
#endif
|
|
|
|
/* In FStar.Buffer.fst, the size of arrays is uint32_t, but it's a number of
|
|
* *elements*. Do an ugly, run-time check (some of which KreMLin can eliminate).
|
|
*/
|
|
|
|
#ifdef __GNUC__
|
|
# define _KRML_CHECK_SIZE_PRAGMA \
|
|
_Pragma("GCC diagnostic ignored \"-Wtype-limits\"")
|
|
#else
|
|
# define _KRML_CHECK_SIZE_PRAGMA
|
|
#endif
|
|
|
|
#define KRML_CHECK_SIZE(size_elt, sz) \
|
|
do { \
|
|
_KRML_CHECK_SIZE_PRAGMA \
|
|
if (((size_t)(sz)) > ((size_t)(SIZE_MAX / (size_elt)))) { \
|
|
KRML_HOST_PRINTF( \
|
|
"Maximum allocatable size exceeded, aborting before overflow at " \
|
|
"%s:%d\n", \
|
|
__FILE__, __LINE__); \
|
|
KRML_HOST_EXIT(253); \
|
|
} \
|
|
} while (0)
|
|
|
|
#endif
|