diff options
| author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2014-10-28 13:31:21 +0100 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-03-20 15:26:52 +0000 |
| commit | d0b5b4ded22d8f4f04b237b5595d3dd586b6ea18 (patch) | |
| tree | 38d50e3c9e2523cde8fa8362c54b69d62192571c /lib | |
| parent | 8d2c8137ad60a3b5d7d5881fe42077fe4298d833 (diff) | |
| download | klee-d0b5b4ded22d8f4f04b237b5595d3dd586b6ea18.tar.gz | |
[Solver] Fix leak intermediate expression not freed
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 6d7dd8b7..a5e4c5ad 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -51,11 +51,6 @@ namespace { STPArrayExprHash::~STPArrayExprHash() { - - // Design decision: STPArrayExprHash is destroyed from the destructor of STPBuilder at the end of the KLEE run; - // Therefore, freeing memory allocated for STP::VCExpr's is currently disabled. - - /* for (ArrayHashIter it = _array_hash.begin(); it != _array_hash.end(); ++it) { ::VCExpr array_expr = it->second; if (array_expr) { @@ -63,16 +58,16 @@ STPArrayExprHash::~STPArrayExprHash() { array_expr = 0; } } - - - for (UpdateNodeHashConstIter it = _update_node_hash.begin(); it != _update_node_hash.end(); ++it) { + + + for (UpdateNodeHashConstIter it = _update_node_hash.begin(); + it != _update_node_hash.end(); ++it) { ::VCExpr un_expr = it->second; if (un_expr) { ::vc_DeleteExpr(un_expr); un_expr = 0; } } - */ } /***/ @@ -218,10 +213,9 @@ ExprHandle STPBuilder::bvVarLeftShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero - res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), - res, - bvZero(width)); + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); + + res = vc_iteExpr(vc, ex, res, bvZero(width)); return res; } @@ -239,8 +233,9 @@ ExprHandle STPBuilder::bvVarRightShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + ex, res, bvZero(width)); return res; @@ -269,8 +264,9 @@ ExprHandle STPBuilder::bvVarArithRightShift(ExprHandle expr, ExprHandle shift) { } // If overshifting, shift to zero + ExprHandle ex = vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)); res = vc_iteExpr(vc, - vc_bvLtExpr(vc, shift, bvConst32(vc_getBVLength(vc,shift), width)), + ex, res, bvZero(width)); return res; |