From e885a946842fce1f24112201ce9d5b3bbafdc0d9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 4 Nov 2009 14:10:20 +0000 Subject: [PATCH] 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 --- src/c_interface/c_interface.cpp | 11 +++++++++-- tests/c-api-tests/parsefile-using-cinterface.c | 1 + 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 49be558..b868033 100644 --- 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 created_exprs; + +// persist holds a copy of ASTNodes so that the reference count of objects we have pointers to doesn't hit zero. +vector 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 b729d65..f53de4c 100644 --- 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); } -- 2.47.3