diff options
| author | barrettcw <barrett@cs.stanford.edu> | 2016-08-03 13:59:04 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-08-03 13:59:04 -0700 |
| commit | 53020abb9381f4e29d628c054c990ddb43bba4b2 (patch) | |
| tree | a8ec48bea9f91c896c572366a9f2ac8a2191e4c5 | |
| parent | ed55020a3467c8df9fd4d7eefdcd7cb6db0a4917 (diff) | |
| parent | 2db836a8d785cb4d3c7f364dc5a968b5f6394b5c (diff) | |
Merge pull request #87 from 4tXJ7f/fix_oob_access
Fix out-of-bounds access in ExprManager
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 6 | ||||
| -rw-r--r-- | src/expr/expr_manager_template.h | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 53e16751e..2dc3aebe5 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -75,7 +75,7 @@ ExprManager::ExprManager() : for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { d_exprStatistics[i] = NULL; } - for (unsigned i = 0; i < LAST_TYPE; ++ i) { + for (unsigned i = 0; i <= LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } #endif @@ -84,7 +84,7 @@ ExprManager::ExprManager() : ExprManager::ExprManager(const Options& options) : d_nodeManager(new NodeManager(this, options)) { #ifdef CVC4_STATISTICS_ON - for (unsigned i = 0; i < LAST_TYPE; ++ i) { + for (unsigned i = 0; i <= LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { @@ -106,7 +106,7 @@ ExprManager::~ExprManager() throw() { d_exprStatistics[i] = NULL; } } - for (unsigned i = 0; i < LAST_TYPE; ++ i) { + for (unsigned i = 0; i <= LAST_TYPE; ++ i) { if (d_exprStatisticsVars[i] != NULL) { d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]); delete d_exprStatisticsVars[i]; diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 31c911736..f30b720de 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -57,7 +57,7 @@ private: NodeManager* d_nodeManager; /** Counts of expressions and variables created of a given kind */ - IntStat* d_exprStatisticsVars[LAST_TYPE]; + IntStat* d_exprStatisticsVars[LAST_TYPE + 1]; IntStat* d_exprStatistics[kind::LAST_KIND]; /** |