1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. 2 Licensed under the Apache 2.0 License. */ 3 4 #ifndef KRML_TYPES_H 5 #define KRML_TYPES_H 6 7 #include <inttypes.h> 8 #include <stdio.h> 9 #include <stdlib.h> 10 11 /* Types which are either abstract, meaning that have to be implemented in C, or 12 * which are models, meaning that they are swapped out at compile-time for 13 * hand-written C types (in which case they're marked as noextract). */ 14 15 typedef uint64_t FStar_UInt64_t, FStar_UInt64_t_; 16 typedef int64_t FStar_Int64_t, FStar_Int64_t_; 17 typedef uint32_t FStar_UInt32_t, FStar_UInt32_t_; 18 typedef int32_t FStar_Int32_t, FStar_Int32_t_; 19 typedef uint16_t FStar_UInt16_t, FStar_UInt16_t_; 20 typedef int16_t FStar_Int16_t, FStar_Int16_t_; 21 typedef uint8_t FStar_UInt8_t, FStar_UInt8_t_; 22 typedef int8_t FStar_Int8_t, FStar_Int8_t_; 23 24 /* Only useful when building Kremlib, because it's in the dependency graph of 25 * FStar.Int.Cast. */ 26 typedef uint64_t FStar_UInt63_t, FStar_UInt63_t_; 27 typedef int64_t FStar_Int63_t, FStar_Int63_t_; 28 29 typedef double FStar_Float_float; 30 typedef uint32_t FStar_Char_char; 31 typedef FILE *FStar_IO_fd_read, *FStar_IO_fd_write; 32 33 typedef void *FStar_Dyn_dyn; 34 35 typedef const char *C_String_t, *C_String_t_; 36 37 typedef int exit_code; 38 typedef FILE *channel; 39 40 typedef unsigned long long TestLib_cycles; 41 42 typedef uint64_t FStar_Date_dateTime, FStar_Date_timeSpan; 43 44 /* The uint128 type is a special case since we offer several implementations of 45 * it, depending on the compiler and whether the user wants the verified 46 * implementation or not. */ 47 #if !defined(KRML_VERIFIED_UINT128) && defined(_MSC_VER) && defined(_M_X64) 48 # include <emmintrin.h> 49 typedef __m128i FStar_UInt128_uint128; 50 #elif !defined(KRML_VERIFIED_UINT128) && !defined(_MSC_VER) 51 typedef unsigned __int128 FStar_UInt128_uint128; 52 #else 53 typedef struct FStar_UInt128_uint128_s { 54 uint64_t low; 55 uint64_t high; 56 } FStar_UInt128_uint128; 57 #endif 58 59 typedef FStar_UInt128_uint128 FStar_UInt128_t, FStar_UInt128_t_, uint128_t; 60 61 #endif 62