From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 14 Mar 2011 19:51:26 +0000 (+0000)
Subject: Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1... 
X-Git-Tag: cvc5-1.0.0~8661
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5135c27ed486e0808c29b20857c54d1fe6bfe3e;p=cvc5.git

Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1 to handle the UNDEFINED_KIND case.
---

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 515b7978c..5f9aa6619 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -114,6 +114,7 @@ typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
  */
 static inline MetaKind metaKindOf(Kind k) {
   static const MetaKind metaKinds[] = {
+    metakind::INVALID, /* UNDEFINED_KIND */
     metakind::INVALID, /* NULL_EXPR */
 ${metakind_kinds}
     metakind::INVALID /* LAST_KIND */
@@ -121,7 +122,10 @@ ${metakind_kinds}
 
   Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
 
-  return metaKinds[k];
+  // We've asserted that k >= NULL_EXPR (which is 0), but we still
+  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
+  // emits warnings for non-assertion builds, since the check isn't done.
+  return metaKinds[k + 1];
 }/* metaKindOf(k) */
 
 /**