From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 22 Oct 2009 18:18:03 +0000 (+0000)
Subject: Fixed a serious memory error in vc_Destroy(). Deleting the STPMgr independent of... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f717ed3c7117e306be18fe8131c546440750608f;p=francis%2Fstp.git

Fixed a serious memory error in vc_Destroy(). Deleting the STPMgr independent of STP was causing a segfault. It has been fixed, and tested for in m32 mode and 64bit mode

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

diff --git a/src/AST/ASTSymbol.cpp b/src/AST/ASTSymbol.cpp
index c6540f4..6e1ea6d 100644
--- a/src/AST/ASTSymbol.cpp
+++ b/src/AST/ASTSymbol.cpp
@@ -37,17 +37,17 @@ namespace BEEV
     delete this;
   }//End of cleanup()
 
-  unsigned long hash(unsigned char *str)
+  unsigned long long hash(unsigned char *str)
   {
-    unsigned long hash = 5381;
-    int c;
+    unsigned long long hash = 5381;
+    long long c;
     
     while (c = *str++)
       hash = ((hash << 5) + hash) + c; /* hash * 33 + c */
 
     //cout << "Hash value computed is: " << hash << endl;
     
-    return hash;
+    return (unsigned long long)hash;
   }
 
 
diff --git a/src/AST/ASTSymbol.h b/src/AST/ASTSymbol.h
index e779c61..c30b558 100644
--- a/src/AST/ASTSymbol.h
+++ b/src/AST/ASTSymbol.h
@@ -12,7 +12,7 @@
 
 namespace BEEV
 {
-  unsigned long hash(unsigned char *str);
+  unsigned long long hash(unsigned char *str);
 
   /******************************************************************
    *  Class ASTSymbol:                                              *
diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index efd58b0..4c9899d 100644
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -89,12 +89,12 @@ namespace BEEV
     
     void ClearAllTables(void)
     {
-      bm->ClearAllTables();
       simp->ClearAllTables();
       bvsolver->ClearAllTables();
       arrayTransformer->ClearAllTables();
       tosat->ClearAllTables();
       Ctr_Example->ClearAllTables();
+      bm->ClearAllTables();
     }
   }; //End of Class STP
 };//end of namespace
diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 8125219..478068f 100644
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -370,15 +370,17 @@ namespace BEEV
 
     void ClearAllTables(void) 
     {
-      // _interior_unique_table.clear();
-      // _bvconst_unique_table.clear();
-      // _symbol_unique_table.clear();
       NodeLetVarMap.clear();
       NodeLetVarMap1.clear();
       PLPrintNodeSet.clear();
       AlreadyPrintedSet.clear();
       StatInfoSet.clear();
-      //_asserts.clear();
+      
+      //DO NOT UNCOMMENT
+      //   _asserts.clear();
+      //   _interior_unique_table.clear();
+      //   _bvconst_unique_table.clear();
+      //   _symbol_unique_table.clear();      
     } //End of ClearAllTables()
 
   };//End of Class STPMgr
diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index 3e816c8..fdfea21 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1718,7 +1718,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
     BEEV::FatalError("");
   }
 
-  //BEEV::GlobalSTP = (stpstar)vc;
+  BEEV::GlobalSTP = (stpstar)vc;
   CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
   if(0 != c) {
     cout << CONSTANTBV::BitVector_Error(c) << endl;
@@ -1729,7 +1729,7 @@ Expr vc_parseExpr(VC vc, const char* infile) {
   cvcparse((void*)AssertsQuery);
   BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
   BEEV::ASTNode query   = (*(BEEV::ASTVec*)AssertsQuery)[1];
-  //BEEV::GlobalSTP->TopLevelSTP(asserts, query);
+  BEEV::GlobalSTP->TopLevelSTP(asserts, query);
 
   node oo = b->CreateNode(BEEV::NOT,query);
   node o = b->CreateNode(BEEV::AND,asserts,oo);
@@ -1836,7 +1836,7 @@ void vc_Destroy(VC vc) {
   //     delete aaa;
   //   }
   delete decls;
-  delete b;
+  delete (stpstar)vc;
 }
 
 void vc_DeleteExpr(Expr e) {
diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index d1da623..5880fce 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -1,4 +1,5 @@
-CXXFLAGS=-DEXT_HASH_MAP -m32 -I../../src/c_interface -L../../lib
+include ../../scripts/Makefile.common
+CXXFLAGS=-DEXT_HASH_MAP $(CFLAGS) $(CFLAGS_M32) -I../../src/c_interface -L../../lib
 
 
 all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19