1 files changed, 16 insertions, 0 deletions
diff --git a/lib/freebl/verified/karamel/include/krml/internal/builtin.h b/lib/freebl/verified/karamel/include/krml/internal/builtin.h
new file mode 100644
index 000000000..f55e5f824
--- /dev/null
+++ b/lib/freebl/verified/karamel/include/krml/internal/builtin.h
@@ -0,0 +1,16 @@
+/* Copyright (c) INRIA and Microsoft Corporation. All rights reserved.
+   Licensed under the Apache 2.0 License. */
+
+#ifndef __KRML_BUILTIN_H
+#define __KRML_BUILTIN_H
+
+/* For alloca, when using KaRaMeL's -falloca */
+#if (defined(_WIN32) || defined(_WIN64))
+#include <malloc.h>
+#endif
+
+/* If some globals need to be initialized before the main, then karamel will
+ * generate and try to link last a function with this type: */
+void krmlinit_globals(void);
+
+#endif