diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-03-14 19:51:26 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-03-14 19:51:26 +0000 |
| commit | c5135c27ed486e0808c29b20857c54d1fe6bfe3e (patch) | |
| tree | 57c1e469db4fb69fcadab126e437b03f67b09c47 /src/expr/metakind_template.h | |
| parent | 0f4764b2f0e64be5df31cd87a27363cf59045665 (diff) | |
Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1 to handle the UNDEFINED_KIND case.
Diffstat (limited to 'src/expr/metakind_template.h')
| -rw-r--r-- | src/expr/metakind_template.h | 6 |
1 files changed, 5 insertions, 1 deletions
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) */ /** |