Bugfixes.

* Create a copy of the output of vc_bvType(,). The copies persists until vc_destroy() is called when they are cleaned up automatically.
* Explicitly delete an expression in on of our test cases.

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 49be558ab2cc64d33a5f823869f0180e8ec290ee..b8680337ff76206d08f683b7f7d9a3ffe2730a6f 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -26,6 +26,9 @@ typedef BEEV::ASTVec                     nodelist;
 typedef BEEV::CompleteCounterExample*    CompleteCEStar;
 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;
 bool cinterface_exprdelete_on_flag = false;
 
 // GLOBAL FUNCTION: parser
@@ -913,9 +916,11 @@ Type vc_bvType(VC vc, int num_bits) {
     }
 
   node e = b->CreateBVConst(32, num_bits);
-  nodestar output = new node(b->CreateNode(BEEV::BITVECTOR,e));
+  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 output;
+  return &persist[index];
 }
 
 Type vc_bv32Type(VC vc) {
@@ -1744,6 +1749,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
   node oo = b->CreateNode(BEEV::NOT,query);
   node o = b->CreateNode(BEEV::AND,asserts,oo);
   nodestar output = new node(o);
+  delete AssertsQuery;
   return output;
 } //end of vc_parseExpr()
 
@@ -1845,6 +1851,7 @@ void vc_Destroy(VC vc) {
   //     BEEV::ASTNode * aaa = *it;
   //     delete aaa;
   //   }
+  persist.clear();
   delete decls;
   delete (stpstar)vc;
 }

diff --git a/tests/c-api-tests/parsefile-using-cinterface.c b/tests/c-api-tests/parsefile-using-cinterface.c
index b729d658f1e87150a921d6f5f9b09210395b0091..f53de4cb5418cf0233f01515db74d8d880d71503 100644 (file)
--- a/tests/c-api-tests/parsefile-using-cinterface.c
+++ b/tests/c-api-tests/parsefile-using-cinterface.c
@@ -12,6 +12,7 @@ int main() {
   Expr c = vc_parseExpr(vc,"./t.cvc"); 
   
   vc_printExpr(vc, c);
+  vc_DeleteExpr(c);
   printf("\n");
   vc_Destroy(vc);
 }