compat.h (1346B)
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