mirror of
https://github.com/Mbed-TLS/mbedtls.git
synced 2025-04-17 11:43:37 +00:00
bee486146e
These files are automatically generated by the Everest toolchain from F*
files. They do not respect the mbedTLS code style guidelines as manual
modification would invalidate verification guarantees. The files in
3rdparty/everest/include/kremli{n,b} are a customized (minimzed) version of the
support headers expected by the code extracted using KreMLin.
103 lines
3.6 KiB
C
103 lines
3.6 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 <stdio.h>
|
|
#include <stdbool.h>
|
|
#include <inttypes.h>
|
|
#include <limits.h>
|
|
|
|
#include "kremlin/internal/callconv.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
|
|
|
|
#if ( \
|
|
(defined __STDC_VERSION__) && (__STDC_VERSION__ >= 199901L) && \
|
|
(!(defined KRML_HOST_EPRINTF)))
|
|
# define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
|
|
#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
|
|
|
|
#ifndef KRML_HOST_TIME
|
|
|
|
# include <time.h>
|
|
|
|
/* Prims_nat not yet in scope */
|
|
inline static int32_t krml_time() {
|
|
return (int32_t)time(NULL);
|
|
}
|
|
|
|
# define KRML_HOST_TIME krml_time
|
|
#endif
|
|
|
|
/* In statement position, exiting is easy. */
|
|
#define KRML_EXIT \
|
|
do { \
|
|
KRML_HOST_PRINTF("Unimplemented function at %s:%d\n", __FILE__, __LINE__); \
|
|
KRML_HOST_EXIT(254); \
|
|
} while (0)
|
|
|
|
/* In expression position, use the comma-operator and a malloc to return an
|
|
* expression of the right size. KreMLin passes t as the parameter to the macro.
|
|
*/
|
|
#define KRML_EABORT(t, msg) \
|
|
(KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n", __FILE__, __LINE__, msg), \
|
|
KRML_HOST_EXIT(255), *((t *)KRML_HOST_MALLOC(sizeof(t))))
|
|
|
|
/* 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)
|
|
|
|
#if defined(_MSC_VER) && _MSC_VER < 1900
|
|
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) _snprintf_s(buf, sz, _TRUNCATE, fmt, arg)
|
|
#else
|
|
# define KRML_HOST_SNPRINTF(buf, sz, fmt, arg) snprintf(buf, sz, fmt, arg)
|
|
#endif
|
|
|
|
#endif
|