1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
2    Licensed under the Apache 2.0 License. */
3 
4 #ifndef KRML_COMPAT_H
5 #define KRML_COMPAT_H
6 
7 #include <inttypes.h>
8 
9 /* A series of macros that define C implementations of types that are not Low*,
10  * to facilitate porting programs to Low*. */
11 
12 typedef const char *Prims_string;
13 
14 typedef struct {
15   uint32_t length;
16   const char *data;
17 } FStar_Bytes_bytes;
18 
19 typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int,
20     krml_checked_int_t;
21 
22 #define RETURN_OR(x)                                                           \
23   do {                                                                         \
24     int64_t __ret = x;                                                         \
25     if (__ret < INT32_MIN || INT32_MAX < __ret) {                              \
26       KRML_HOST_PRINTF(                                                        \
27           "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__,         \
28           __LINE__);                                                           \
29       KRML_HOST_EXIT(252);                                                     \
30     }                                                                          \
31     return (int32_t)__ret;                                                     \
32   } while (0)
33 
34 #endif
35