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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index fde95a2ab6eb8e2ab98f21811dd67ef789c54a60..609f94430b6e6b0d12f59bfa6eac38a068ce8448 100644 (file)
--- 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 01e4abe2ec291d1c166db492889a88194f222929..7d9ff84727e4a7ff7dad7e4f0d0bddf422371fce 100644 (file)
--- 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 9a3e156470e114c076793e8e344086b988594b2c..71f5e64d9f13ff0a222f6dac3f10966192239697 100644 (file)
--- 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 da75f06b2d0b70c68cb63efcd07d9cb14e9889c3..92c69c2c6587a55dd741f5c9bfb79a85b28b1c64 100644 (file)
--- 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 b04556b1e024811bb13b0809270063cd231b80d1..3d23dbc0996634adb0bd265c2b6794b86adde7d1 100644 (file)
--- 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;
 }