Introduce vc_setInterfaceFlags function

This patch adds a vc_setInterfaceFlags function to the C interface
with one possible flag, EXPRDELETE, which is set by default.  The flag
controls whether the C interface deletes types and integer constant
expressions at vc_Destroy time.  It is intended that clients which
perform their own memory management of these objects will be able to
clear this flag.

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

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index a352dd85e0e5b2e7de9e90e65c34ae9052eb3e4d..577f43a0dc8d40e16deb3db4235846628b367f1d 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -31,7 +31,7 @@ BEEV::ASTVec *decls = NULL;
 // 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;
+bool cinterface_exprdelete_on_flag = true;
 
 // GLOBAL FUNCTION: parser
 extern int cvcparse(void*);
@@ -148,6 +148,17 @@ void vc_setFlags(VC vc, char c, int param_value) {
   }
 }
 
+void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value) {
+  switch (f) {
+  case EXPRDELETE:
+    cinterface_exprdelete_on_flag = param_value != 0;
+    break;
+  default:
+    BEEV::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized flag\n");
+    break;
+  }
+}
+
 //Create a validity Checker. This is the global STPMgr
 VC vc_createValidityChecker(void) {
   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
@@ -404,8 +415,10 @@ void vc_printQuery(VC vc){
 
 nodestar persistNode(node n)
 {
-  persist.push_back(new node(n));
-  return  persist.back();
+  nodestar np = new node(n);
+  if (cinterface_exprdelete_on_flag)
+    persist.push_back(np);
+  return np;
 }
 
 
@@ -1891,9 +1904,11 @@ void vc_Destroy(VC vc) {
   //     delete aaa;
   //   }
 
-  for (vector<nodestar>::iterator it = persist.begin(); it!= persist.end();it++)
-    delete *it;
-  persist.clear();
+  if (cinterface_exprdelete_on_flag) {
+    for (vector<nodestar>::iterator it = persist.begin(); it!= persist.end();it++)
+      delete *it;
+    persist.clear();
+  }
 
   delete decls;
   delete (stpstar)vc;

diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 6cbdf90c16742184db9249760207fe61c0056a10..a4679e7d0c09393da0099fd1dbb813734d27098e 100644 (file)
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -50,6 +50,17 @@ extern "C" {
   // v  : print nodes
   void vc_setFlags(VC vc, char c, int num_absrefine _CVCL_DEFAULT_ARG(0));
 
+  //! Interface-only flags.
+  enum ifaceflag_t {
+  /*! EXPRDELETE: boolean, default true. For objects created by
+    vc_arrayType, vc_bvType, vc_bv32Type, vc_bvConstExprFromInt, if
+    this flag is set both at the time the objects are created and at
+    the time that vc_Destroy is called, vc_Destroy will automatically
+    delete them. */
+    EXPRDELETE
+  };
+  void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value);
+
   //! Flags can be NULL
   VC vc_createValidityChecker(void);