diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-04-06 06:39:01 +0000 |
| commit | 4143f662e0c5ef311e98dbd554500b98cd02ecdb (patch) | |
| tree | 79abe3f9393d41450ada658dbd3f0914680048c9 /test | |
| parent | 6ad21b68e654b940d97caea6d34404d0a6b6e628 (diff) | |
* Add some protected ContextObj accessors for ContextObj-derived classes:
+ Context* getContext() -- gets the context
+ ContextMemoryManager* getCMM() -- gets the CMM
+ int getLevel() -- the scope level of the ContextObj's most recent update
+ bool isCurrent() -- true iff the most recent update is the current top level
In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
ECData::addPredecessor() function substantially (re: code review bug #64).
* Fix serious bugs in context operations that corrupted the ContextObj
linked lists. Closes bug #85.
* Identified a bug in the way objects of the "Link" class are
allocated; see bug #96.
* Re-enable context white-box tests that ensure proper links in linked
lists. Closes bug #86.
* Re-enable CDMap<>::emptyTrash(). Closes bug #87.
* Add a tracing option (-t foo or --trace foo) to the driver to enable
Trace("foo") output stream. -d foo implies -t foo.
* Minor clean-up of some TheoryUF code; addition of some documentation
(re: code review bug #64).
* Address some things that caused Doxygen discomfort.
* Address an issue raised in NodeManager's code review (bug #65).
* Remove an inaccurate comment in Attribute code (re: code review bug #61).
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/context/context_white.h | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 3e0928baf..0963e4100 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -164,14 +164,14 @@ public: TS_ASSERT(b.d_pScope == t); TS_ASSERT(b.d_pContextObjRestore != NULL); TS_ASSERT(b.d_pContextObjNext == &a); - //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS + TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); d_context->pop(); TS_ASSERT(s->d_pContext == d_context); TS_ASSERT(s->d_pCMM == d_context->d_pCMM); TS_ASSERT(s->d_level == 0); - //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS + TS_ASSERT(s->d_pContextObjList == &c); TS_ASSERT(a.d_pScope == s); TS_ASSERT(a.d_pContextObjRestore == NULL); @@ -181,6 +181,11 @@ public: TS_ASSERT(b.d_pScope == s); TS_ASSERT(b.d_pContextObjRestore == NULL); TS_ASSERT(b.d_pContextObjNext == &a); - TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + TS_ASSERT(b.d_ppContextObjPrev == &c.d_pContextObjNext); + + TS_ASSERT(c.d_pScope == s); + TS_ASSERT(c.d_pContextObjRestore == NULL); + TS_ASSERT(c.d_pContextObjNext == &b); + TS_ASSERT(c.d_ppContextObjPrev == &s->d_pContextObjList); } }; |