From: trevor_hansen Date: Tue, 8 Feb 2011 12:29:21 +0000 (+0000) Subject: Patch from Khoo Yit Phang. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c61596221db9a96d7d880ad8240d0c3e24d4b89b;p=francis%2Fstp.git Patch from Khoo Yit Phang. Fix the weird type of STPMgr::CreateBVConst (to have only one reference level). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1129 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 197baca..8eab3db 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -204,7 +204,7 @@ namespace BEEV } - ASTNode STPMgr::CreateBVConst(string*& strval, int base, int bit_width) + ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width) { if (bit_width <= 0) @@ -223,17 +223,17 @@ namespace BEEV if (2 == base) { e = CONSTANTBV::BitVector_from_Bin(bv, - (unsigned char*) strval->c_str()); + (unsigned char*) strval.c_str()); } else if (10 == base) { e = CONSTANTBV::BitVector_from_Dec(bv, - (unsigned char*) strval->c_str()); + (unsigned char*) strval.c_str()); } else if (16 == base) { e = CONSTANTBV::BitVector_from_Hex(bv, - (unsigned char*) strval->c_str()); + (unsigned char*) strval.c_str()); } else { diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index bf68c34..6650852 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -275,7 +275,7 @@ namespace BEEV ASTNode CreateZeroConst(unsigned int width); ASTNode CreateBVConst(CBV bv, unsigned width); ASTNode CreateBVConst(const char *strval, int base); - ASTNode CreateBVConst(string*& strval, int base, int bit_width); + ASTNode CreateBVConst(string& strval, int base, int bit_width); ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); /**************************************************************** diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index d9139b9..5738611 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -981,18 +981,14 @@ Type vc_bv32Type(VC vc) { } Expr vc_bvConstExprFromDecStr(VC vc, - const size_t width, + int width, const char* decimalInput ) { bmstar b = (bmstar)(((stpstar)vc)->bm); - - string *param = new string(decimalInput); - // funny type to get it to compile. fix later when I - // understand what this does. - node n = b->CreateBVConst((string*&)param, (int)10,(int)width); + string str(decimalInput); + node n = b->CreateBVConst(str, 10, width); BVTypeCheck(n); nodestar output = new node(n); - delete param; return output; } diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index a4679e7..275bd92 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -233,7 +233,7 @@ extern "C" { Type vc_bvType(VC vc, int no_bits); Type vc_bv32Type(VC vc); - Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, const char* decimalInput ); + Expr vc_bvConstExprFromDecStr(VC vc, int width, const char* decimalInput ); Expr vc_bvConstExprFromStr(VC vc, const char* binary_repr); Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value); Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value); diff --git a/src/parser/CVC.y b/src/parser/CVC.y index fe057ba..0d4221d 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -729,21 +729,21 @@ Expr : TERMID_TOK { $$ = new ASTNode(parserInterface->letMgr.Res } | NUMERAL_TOK BIN_BASED_NUMBER { - std::string* vals = new std::string($2); + std::string vals($2); $$ = new ASTNode(parserInterface->CreateBVConst(vals, 2, $1)); - free($2); delete vals; + free($2); } | NUMERAL_TOK DEC_BASED_NUMBER { - std::string* vals = new std::string($2); + std::string vals($2); $$ = new ASTNode(parserInterface->CreateBVConst(vals, 10, $1)); - free($2); delete vals; + free($2); } | NUMERAL_TOK HEX_BASED_NUMBER { - std::string* vals = new std::string($2); + std::string vals($2); $$ = new ASTNode(parserInterface->CreateBVConst(vals, 16, $1)); - free($2); delete vals; + free($2); } | Expr '[' Expr ']' { diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index 0b8cb7f..6a74888 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -72,7 +72,7 @@ public: return bm.CreateOneConst(width); } - ASTNode CreateBVConst(string*& strval, int base, int bit_width) + ASTNode CreateBVConst(string& strval, int base, int bit_width) { return bm.CreateBVConst(strval, base, bit_width); } diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index 53f7f70..9dd8391 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -683,12 +683,12 @@ an_terms an_term an_term: BVCONST_TOK { - $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32)); + $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 10, 32)); delete $1; } | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK { - $$ = new ASTNode(parserInterface->CreateBVConst($1,10,$3)); + $$ = new ASTNode(parserInterface->CreateBVConst(*$1,10,$3)); delete $1; } | an_nonbvconst_term diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y index 463260b..927dec1 100644 --- a/src/parser/smtlib2.y +++ b/src/parser/smtlib2.y @@ -930,21 +930,21 @@ TERMID_TOK } | UNDERSCORE_TOK BVCONST_DECIMAL_TOK NUMERAL_TOK { - $$ = new ASTNode(parserInterface->CreateBVConst($2, 10, $3)); + $$ = new ASTNode(parserInterface->CreateBVConst(*$2, 10, $3)); $$->SetValueWidth($3); delete $2; } | BVCONST_HEXIDECIMAL_TOK { unsigned width = $1->length()*4; - $$ = new ASTNode(parserInterface->CreateBVConst($1, 16, width)); + $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 16, width)); $$->SetValueWidth(width); delete $1; } | BVCONST_BINARY_TOK { unsigned width = $1->length(); - $$ = new ASTNode(parserInterface->CreateBVConst($1, 2, width)); + $$ = new ASTNode(parserInterface->CreateBVConst(*$1, 2, width)); $$->SetValueWidth(width); delete $1; }