compat.h (1306B)
1 /* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. 2 Licensed under the Apache 2.0 and MIT Licenses. */ 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 struct { 13 uint32_t length; 14 const char *data; 15 } FStar_Bytes_bytes; 16 17 typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int, 18 krml_checked_int_t; 19 20 #define RETURN_OR(x) \ 21 do { \ 22 int64_t __ret = x; \ 23 if (__ret < INT32_MIN || INT32_MAX < __ret) { \ 24 KRML_HOST_PRINTF( \ 25 "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__, \ 26 __LINE__); \ 27 KRML_HOST_EXIT(252); \ 28 } \ 29 return (int32_t)__ret; \ 30 } while (0) 31 32 #endif