You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
61 lines
2.0 KiB
61 lines
2.0 KiB
/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
|
|
Licensed under the Apache 2.0 License. */
|
|
|
|
#ifndef KRML_TYPES_H
|
|
#define KRML_TYPES_H
|
|
|
|
#include <inttypes.h>
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
|
|
/* Types which are either abstract, meaning that have to be implemented in C, or
|
|
* which are models, meaning that they are swapped out at compile-time for
|
|
* hand-written C types (in which case they're marked as noextract). */
|
|
|
|
typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_;
|
|
typedef int64_t FStar_Int64_t, FStar_Int64_t_;
|
|
typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_;
|
|
typedef int32_t FStar_Int32_t, FStar_Int32_t_;
|
|
typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_;
|
|
typedef int16_t FStar_Int16_t, FStar_Int16_t_;
|
|
typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_;
|
|
typedef int8_t FStar_Int8_t, FStar_Int8_t_;
|
|
|
|
/* Only useful when building Kremlib, because it's in the dependency graph of
|
|
* FStar.Int.Cast. */
|
|
typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_;
|
|
typedef int64_t FStar_Int63_t, FStar_Int63_t_;
|
|
|
|
typedef double FStar_Float_float;
|
|
typedef uint32_t FStar_Char_char;
|
|
typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write;
|
|
|
|
typedef void *FStar_Dyn_dyn;
|
|
|
|
typedef const char *C_String_t, *C_String_t_;
|
|
|
|
typedef int exit_code;
|
|
typedef FILE *channel;
|
|
|
|
typedef unsigned long long TestLib_cycles;
|
|
|
|
typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan;
|
|
|
|
/* The uint128 type is a special case since we offer several implementations of
|
|
* it, depending on the compiler and whether the user wants the verified
|
|
* implementation or not. */
|
|
#if !defined(KRML_VERIFIED_UINT128) && defined(_MSC_VER) && defined(_M_X64)
|
|
# include <emmintrin.h>
|
|
typedef __m128i FStar_UInt128_uint128;
|
|
#elif !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER)
|
|
typedef unsigned __int128 FStar_UInt128_uint128;
|
|
#else
|
|
typedef struct FStar_UInt128_uint128_s {
|
|
uint64_t low;
|
|
uint64_t high;
|
|
} FStar_UInt128_uint128;
|
|
#endif
|
|
|
|
typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t;
|
|
|
|
#endif
|
|
|