From 8460edbe6c3db4afe207b3e1c0963e48d52e274e Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 6 Nov 2009 13:12:40 +0000
Subject: [PATCH] Fix memory leaks triggered by capi testcase 15 (x.c).

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@388 e59a4935-1847-0410-ae03-e826735625c1
---
 src/c_interface/c_interface.cpp |  4 +---
 src/to-sat/CallSAT.cpp          |  6 ++++++
 src/to-sat/ToCNF.cpp            |  2 +-
 tests/c-api-tests/Makefile      |  2 +-
 tests/c-api-tests/x.c           | 24 ++++++++++++++++++++++--
 5 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index fde95a2..609f944 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -973,9 +973,7 @@ Expr vc_bvConstExprFromInt(VC vc,
   }
   node n = b->CreateBVConst(n_bits, v);
   BVTypeCheck(n);
-  nodestar output = new node(n);
-  //if(cinterface_exprdelete_on) created_exprs.push_back(output);
-  return output;
+  return persistNode(n);
 }
 
 Expr vc_bvConstExprFromLL(VC vc,
diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index 01e4abe..7d9ff84 100644
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -87,6 +87,12 @@ namespace BEEV
     ClauseBuckets * cb = Sort_ClauseList_IntoBuckets(cl);
     //bool sat = toSATandSolve(SatSolver, *cl);
     bool sat = CallSAT_On_ClauseBuckets(SatSolver, cb);
+
+    for (ClauseBuckets::iterator it = cb->begin(); it != cb->end(); it++)
+    	delete it->second;
+    delete cb;
+
+
     if(!sat)
       {
 	return sat;
diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp
index 9a3e156..71f5e64 100644
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ToCNF.cpp
@@ -1822,7 +1822,7 @@ namespace BEEV
       }
     store.clear();
     
-    //FIXME: Delete clausesxor
+    delete clausesxor;
   }
 
   //########################################
diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index da75f06..92c69c2 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -61,7 +61,7 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20
 	./a14.out
 15:
 	g++  $(CXXFLAGS)  x.c  -lstp -o a15.out
-	./a15.out
+	$(VALGRIND) ./a15.out
 16:
 	g++ $(CXXFLAGS)  y.c -lstp -o a16.out
 	./a16.out
diff --git a/tests/c-api-tests/x.c b/tests/c-api-tests/x.c
index b04556b..3d23dbc 100644
--- a/tests/c-api-tests/x.c
+++ b/tests/c-api-tests/x.c
@@ -9,6 +9,8 @@ int main(int argc, char *argv[]) {
   Expr nresp1 = vc_varExpr(vc, "nresp1", vc_bv32Type(vc));
   Expr packet_get_int0 = vc_varExpr(vc, "packet_get_int0", vc_bv32Type(vc));
   Expr sz = vc_varExpr(vc, "sz", vc_bv32Type(vc));
+
+  Expr d0,d1,d2;
   Expr exprs[] = {
     // nresp1 == packet_get_int0
     vc_eqExpr(vc, nresp1, packet_get_int0),
@@ -17,15 +19,33 @@ int main(int argc, char *argv[]) {
     vc_bvGtExpr(vc, nresp1, vc_bv32ConstExprFromInt(vc, 0)),
     
     // sz == nresp1 * 4
-    vc_eqExpr(vc, sz, vc_bv32MultExpr(vc, nresp1, vc_bv32ConstExprFromInt(vc, 4))),
+    vc_eqExpr(vc, sz, d0=vc_bv32MultExpr(vc, nresp1, vc_bv32ConstExprFromInt(vc, 4))),
     
     // sz > nresp1 || sz < 0
-    vc_orExpr(vc, vc_sbvGeExpr(vc, sz, nresp1), vc_sbvLtExpr(vc, sz, vc_bv32ConstExprFromInt(vc, 0))),
+    vc_orExpr(vc, d1=vc_sbvGeExpr(vc, sz, nresp1), d2=vc_sbvLtExpr(vc, sz, vc_bv32ConstExprFromInt(vc, 0))),
   };
   
   Expr res = vc_andExprN(vc, exprs, sizeof(exprs)/sizeof(exprs[0]));
   //vc_printExpr(vc, res);
   vc_query(vc,res);
+
+  vc_DeleteExpr(nresp1);
+  vc_DeleteExpr(packet_get_int0);
+  vc_DeleteExpr(sz);
+
+  vc_DeleteExpr(d0);
+  vc_DeleteExpr(d1);
+  vc_DeleteExpr(d2);
+
+  vc_DeleteExpr(exprs[0]);
+  vc_DeleteExpr(exprs[1]);
+  vc_DeleteExpr(exprs[2]);
+  vc_DeleteExpr(exprs[3]);
+  vc_DeleteExpr(res);
+
+
+
+
   vc_Destroy(vc);
   return 0;
 }
-- 
2.47.3