diff --git a/src/library/module.cpp b/src/library/module.cpp index 72bfad1748..c7c1f08fde 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -110,11 +110,12 @@ extern "C" object * lean_read_module_data(object * fname, object * w) { if (size < header_size) { return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); } - char header[header_size]; + char * header = new char[header_size]; in.read(header, header_size); if (strncmp(header, g_olean_header, header_size) != 0) { return set_io_error(w, (sstream() << "failed to read file '" << olean_fn << "', invalid header").str()); } + delete[] header; char * buffer = new char[size - header_size]; in.read(buffer, size - header_size); if (!in) { diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index 91274b0b3f..c03e5bf985 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "runtime/object.h" #include "runtime/allocprof.h" namespace lean { diff --git a/src/runtime/io.h b/src/runtime/io.h index 6aea01a0a5..607ffd5f87 100644 --- a/src/runtime/io.h +++ b/src/runtime/io.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "runtime/object.h" namespace lean { obj_res set_io_result(obj_arg r, obj_arg a);