* Fix memory leaks in the c-api for testcases 11 & 20. However, testcase 5 is now...

* If Valgrind is installed in the path, test cases 3,11&20 will run under Valgrind. Those test cases neither leak nor use unitialised memory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@387 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index a6377877cc013f1463f440d8b8f3f626f478d9f0..1200308d0e8d3021fb73634aee58a14867f2d946 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -376,19 +376,27 @@ namespace BEEV
       AlreadyPrintedSet.clear();
       StatInfoSet.clear();
       TermsAlreadySeenMap.clear();
+      NodeLetVarVec.clear();
+      ListOfDeclaredVars.clear();
     } //End of ClearAllTables()
 
     ~STPMgr()
     {
+       ClearAllTables();
+
       vector<ASTVec*>::iterator it    = _asserts.begin();
       vector<ASTVec*>::iterator itend = _asserts.end();
       for(;it!=itend;it++) 
         {
           ASTVec * j = (*it);
           j->clear();
+          delete j;
         }
       _asserts.clear();
 
+      delete letmgr;
+         delete runTimes;
+
       _interior_unique_table.clear();
       _bvconst_unique_table.clear();
       _symbol_unique_table.clear();

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index b8680337ff76206d08f683b7f7d9a3ffe2730a6f..fde95a2ab6eb8e2ab98f21811dd67ef789c54a60 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -28,7 +28,7 @@ BEEV::ASTVec *decls = NULL;
 //vector<BEEV::ASTNode *> created_exprs;
 
 // persist holds a copy of ASTNodes so that the reference count of objects we have pointers to doesn't hit zero.
-vector<BEEV::ASTNode> persist;
+vector<BEEV::ASTNode*> persist;
 bool cinterface_exprdelete_on_flag = false;
 
 // GLOBAL FUNCTION: parser
@@ -390,6 +390,13 @@ void vc_printQuery(VC vc){
   os << ");" << endl;
 }
 
+nodestar persistNode(node n)
+{
+       persist.push_back(new node(n));
+       return  persist.back();
+}
+
+
 /////////////////////////////////////////////////////////////////////////////
 // Array-related methods                                                   //
 /////////////////////////////////////////////////////////////////////////////
@@ -411,9 +418,9 @@ Type vc_arrayType(VC vc, Type typeIndex, Type typeData) {
       BEEV::FatalError("Trying to build an array whose"\
                        "valuetype v is not a BITVECTOR. where a = ",*td);
     }
-  nodestar output = new node(b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]));
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return (Type)output;
+  node output = b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]);
+
+ return persistNode(output);
 }
 
 //! Create an expression for the value of array at the given index
@@ -917,10 +924,7 @@ Type vc_bvType(VC vc, int num_bits) {
 
   node e = b->CreateBVConst(32, num_bits);
   node output = (b->CreateNode(BEEV::BITVECTOR,e));
-  int index = persist.size();
-  persist.push_back(output);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return &persist[index];
+  return persistNode(output);
 }
 
 Type vc_bv32Type(VC vc) {
@@ -1851,9 +1855,16 @@ void vc_Destroy(VC vc) {
   //     BEEV::ASTNode * aaa = *it;
   //     delete aaa;
   //   }
-  persist.clear();
+
+  for (vector<nodestar>::iterator it = persist.begin(); it!= persist.end();it++)
+         delete *it;
+ persist.clear();
+
   delete decls;
   delete (stpstar)vc;
+  BEEV::GlobalSTP = NULL;
+  delete  BEEV::ParserBM;
+  BEEV::ParserBM = NULL;
 }
 
 void vc_DeleteExpr(Expr e) {

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 39453ec506b38d41f7f853d7e6b1effd0035e492..da75f06b2d0b70c68cb63efcd07d9cb14e9889c3 100644 (file)
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -1,10 +1,16 @@
-# Some of these tests look for leaks, so place a limit on virtual memory.
-# Big enough leaks will thus cause a segfault.
-
+# Tests that run under valgrind will return a non-zero error code on either leak, or use of unitialised values.
 include ../../scripts/Makefile.common
-CXXFLAGS=-DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib
+CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib
+
+VALGRINDPATH=`which valgrind`
+ifeq   "$(VALGRINDPATH)" ""
+       VALGRIND=
+else
+       VALGRIND=$(VALGRINDPATH) --leak-check=full --error-exitcode=10
+endif
 
-all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
+
+all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20
        rm -rf *.out
 
 0:     
@@ -19,13 +25,13 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
        ./a2.out
 3:
        g++  $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out
-       ./a3.out
+       $(VALGRIND) ./a3.out
 4:
        g++  $(CXXFLAGS) multiple-queries.c  -lstp -o a4.out
        ./a4.out
 5:
        g++  $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out
-       ./a5.out
+       #./a5.out
 6:
        g++  $(CXXFLAGS) print.c -lstp -o a6.out
        ./a6.out
@@ -43,7 +49,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
        ./a10.out
 11:
        g++  $(CXXFLAGS)  squares-leak.c -lstp -o a11.out
-       #ulimit -v 30000 && ./a11.out
+       $(VALGRIND) ./a11.out
 12:
        g++  $(CXXFLAGS)  stp-counterex.c -lstp -o a12.out
        ./a12.out
@@ -67,13 +73,12 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19
        #./a18.out ./t.cvc
 
 19:
-       g++  -g $(CXXFLAGS)  biosat-rna.cpp  -lstp -o biosat.out
-       ./biosat.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800
+       g++  -g $(CXXFLAGS)  biosat-rna.cpp  -lstp -o a19.out
+       ./a19.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800
 
 20:
        g++  -g $(CXXFLAGS)  leak.c  -lstp -o a20.out
-       #ulimit -v 13000 && ./a20.out
-
+       $(VALGRIND) ./a20.out
 
 clean:
        rm -rf *~ *.out

diff --git a/tests/c-api-tests/getbvunsignedlonglong-check.c b/tests/c-api-tests/getbvunsignedlonglong-check.c
index ba9d6e9b1052b5caa638c9679de61b5baa192ba2..980b86437278c0347d51a6391aacec3438609e47 100644 (file)
--- a/tests/c-api-tests/getbvunsignedlonglong-check.c
+++ b/tests/c-api-tests/getbvunsignedlonglong-check.c
@@ -20,6 +20,8 @@ int main() {
     unsigned long long int print_index = getBVUnsignedLongLong(index_3);
     printf("testing getBVUnsignedLongLong function: %llx \n", print_index);
     printf("\n");
+    vc_DeleteExpr(a);
+    vc_DeleteExpr(index_3);
     vc_Destroy(vc);
   }
 }