From ba641d7c587453cbd65e720ee43ab1ffcbde4e05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Feb 2015 12:42:53 -0800
Subject: [PATCH] feat(library/normalize): validate unfold-c hints

---
 src/library/normalize.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index 008d4c029..0aea314ad 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -64,6 +64,9 @@ template class scoped_ext<unfold_c_hint_config>;
 typedef scoped_ext<unfold_c_hint_config> unfold_c_hint_ext;
 
 environment add_unfold_c_hint(environment const & env, name const & n, optional<unsigned> idx, bool persistent) {
+    declaration const & d = env.get(n);
+    if (!d.is_definition() || d.is_opaque())
+        throw exception("invalid unfold-c hint, declaration must be a non-opaque definition");
     return unfold_c_hint_ext::add_entry(env, get_dummy_ios(), unfold_c_hint_entry(n, idx), persistent);
 }