From a0a70a678ae876f7f4e437555c47a21cd28bf6de Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 21 Jun 2017 11:07:03 +0200
Subject: [PATCH] fix(library/module): check for end-of-file in deserialization

---
 src/library/module.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/library/module.cpp b/src/library/module.cpp
index 51b13cab46..445a47fa0e 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -511,6 +511,10 @@ olean_data parse_olean(std::istream & in, std::string const & file_name, bool ch
     code.resize(code_size);
     d1.read(code);
 
+    if (!in.good()) {
+        throw exception(sstream() << "file '" << file_name << "' has been corrupted");
+    }
+
 //    if (m_senv.env().trust_lvl() <= LEAN_BELIEVER_TRUST_LEVEL) {
     if (check_hash) {
         unsigned computed_hash = olean_hash(code.data(), code_size);
@@ -617,6 +621,9 @@ modification_list parse_olean_modifications(std::vector<char> const & olean_code
 
         obj_counter++;
     }
+    if (!in.good()) {
+        throw exception(sstream() << "file '" << file_name << "' has been corrupted");
+    }
     return ms;
 }