projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
7742c42
)
Fix for thos annoying "array index" warnings in production builds
author
Dejan Jovanović
<dejan.jovanovic@gmail.com>
Tue, 17 Apr 2012 20:42:09 +0000
(20:42 +0000)
committer
Dejan Jovanović
<dejan.jovanovic@gmail.com>
Tue, 17 Apr 2012 20:42:09 +0000
(20:42 +0000)
src/expr/node_manager.h
patch
|
blob
|
history
diff --git
a/src/expr/node_manager.h
b/src/expr/node_manager.h
index da999cc829be91f384c04b0cbecec7cabf9a7993..5e27962da7eb315927c35092fc411b073cad34a2 100644
(file)
--- a/
src/expr/node_manager.h
+++ b/
src/expr/node_manager.h
@@
-1383,10
+1383,17
@@
NodeClass NodeManager::mkConstInternal(const T& val) {
nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
nvStack.d_rc = 0;
nvStack.d_nchildren = 1;
+
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Warray-bounds"
+
nvStack.d_children[0] =
const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
expr::NodeValue* nv = poolLookup(&nvStack);
+#pragma GCC diagnostic pop
+
+
if(nv != NULL) {
return NodeClass(nv);
}