From 3fb103dadced1d5cd392c5447d87c3599f8754c6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Jul 2012 16:31:12 -0700 Subject: Debugging a proof error. --- src/misc/vec/vecSet.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 5f8df449..7e5c6c62 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -154,6 +154,25 @@ static inline void Vec_SetRestart( Vec_Set_t * p ) Vec_SetWriteLimit( p->pPages[0], 2 ); } +/**Function************************************************************* + + Synopsis [Returns memory in bytes occupied by the vector.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline double Vec_ReportMemory( Vec_Set_t * p ) +{ + double Mem = sizeof(Vec_Set_t); + Mem += p->nPagesAlloc * sizeof(void *); + Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); + return Mem; +} + /**Function************************************************************* Synopsis [Freeing vector.] -- cgit v1.2.3