1 files changed, 32 insertions, 0 deletions
diff --git a/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h b/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h
new file mode 100644
index 0000000000..964d1c52aa
--- /dev/null
+++ b/security/nss/lib/freebl/verified/karamel/include/krml/internal/compat.h
@@ -0,0 +1,32 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef KRML_COMPAT_H
+#define KRML_COMPAT_H
+
+#include <inttypes.h>
+
+/* A series of macros that define C implementations of types that are not Low*,
+ * to facilitate porting programs to Low*. */
+
+typedef struct {
+    uint32_t length;
+    const char *data;
+} FStar_Bytes_bytes;
+
+typedef int32_t Prims_pos, Prims_nat, Prims_nonzero, Prims_int,
+    krml_checked_int_t;
+
+#define RETURN_OR(x)                                                         \
+    do {                                                                     \
+        int64_t __ret = x;                                                   \
+        if (__ret < INT32_MIN || INT32_MAX < __ret) {                        \
+            KRML_HOST_PRINTF(                                                \
+                "Prims.{int,nat,pos} integer overflow at %s:%d\n", __FILE__, \
+                __LINE__);                                                   \
+            KRML_HOST_EXIT(252);                                             \
+        }                                                                    \
+        return (int32_t)__ret;                                               \
+    } while (0)
+
+#endif