diff options
Diffstat (limited to 'proofs/lfsc_checker')
-rw-r--r-- | proofs/lfsc_checker/check.cpp | 13 | ||||
-rw-r--r-- | proofs/lfsc_checker/code.cpp | 24 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.cpp | 4 | ||||
-rw-r--r-- | proofs/lfsc_checker/expr.h | 10 |
4 files changed, 42 insertions, 9 deletions
diff --git a/proofs/lfsc_checker/check.cpp b/proofs/lfsc_checker/check.cpp index 9c7a70fe7..cf68edb87 100644 --- a/proofs/lfsc_checker/check.cpp +++ b/proofs/lfsc_checker/check.cpp @@ -353,6 +353,9 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, sym->dec(); // the pivar->val reference if (create) return new CExpr(LAM, sym, range); + if (range) { + range->dec(); + } sym->dec(); // the symbol table reference, otherwise in the new LAM return 0; } @@ -830,6 +833,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, if (mpq_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); i = new RatExpr(num); + mpq_clear(num); } else { @@ -837,6 +841,7 @@ Expr *check(bool create, Expr *expected, Expr **computed = NULL, if (mpz_init_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); i = new IntExpr(num); + mpz_clear(num); } } @@ -1374,6 +1379,14 @@ void cleanup() { p->dec(); } } + + //std::cout << Expr::to_free.size() << std::endl; + expr_ptr_set_t::iterator it, it_end; + for (it = Expr::to_free.begin(), it_end = Expr::to_free.end(); it != it_end; it++) { + (*it)->debug(); + std::cout << (*it)->getrefcnt() << std::endl; + } + } void init() { diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp index 48ebc5578..6f6223c8d 100644 --- a/proofs/lfsc_checker/code.cpp +++ b/proofs/lfsc_checker/code.cpp @@ -538,6 +538,7 @@ Expr *read_code() { report_error("Error reading a mpq numeral."); Expr* e = new RatExpr( num ); + mpq_clear(num); return e; } else @@ -545,7 +546,9 @@ Expr *read_code() { mpz_t num; if (mpz_init_set_str(num,v.c_str(),10) == -1) report_error("Error reading a numeral."); - return new IntExpr(num); + Expr* e = new IntExpr(num); + mpz_clear(num); + return e; } } default: @@ -973,7 +976,7 @@ Expr *check_code(Expr *_e) { if (!mtp) mtp = tp; - else + else { if (mtp != tp) report_error(string("Types for bodies of match cases or the default differ.") +string("\n1. type for first case's body: ") @@ -982,6 +985,7 @@ Expr *check_code(Expr *_e) { : (string("\n2. type for the body of case for ") +pat->toString())) +string(": ")+tp->toString()); + } } @@ -1084,7 +1088,9 @@ Expr *run_code(Expr *_e) { mpz_cdiv_q(r, ((IntExpr *)r1)->n, ((IntExpr *)r2)->n); r1->dec(); r2->dec(); - return new IntExpr(r); + Expr* result = new IntExpr(r); + mpz_clear(r); + return result; } else if( r1->getclass()==RAT_EXPR && r2->getclass()==RAT_EXPR ) { @@ -1098,7 +1104,9 @@ Expr *run_code(Expr *_e) { mpq_div(q, ((RatExpr *)r1)->n, ((RatExpr *)r2)->n); r1->dec(); r2->dec(); - return new RatExpr(q); + Expr* result = new RatExpr(q); + mpq_clear(q); + return result; } else { @@ -1117,14 +1125,18 @@ Expr *run_code(Expr *_e) { mpz_init(r); mpz_neg(r, ((IntExpr *)r1)->n); r1->dec(); - return new IntExpr(r); + Expr* result = new IntExpr(r); + mpz_clear(r); + return result; } else if( r1->getclass() == RAT_EXPR ) { mpq_t q; mpq_init(q); mpq_neg(q, ((RatExpr *)r1)->n); r1->dec(); - return new RatExpr(q); + Expr* result = new RatExpr(q); + mpq_clear(q); + return result; } else { diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index 8c8120edb..0ee164655 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -10,6 +10,7 @@ using namespace std; int HoleExpr::next_id = 0; int Expr::markedCount = 0; +expr_ptr_set_t Expr::to_free; C_MACROS__ADD_CHUNKING_MEMORY_MANAGEMENT_CC(CExpr,kids,32768); @@ -50,6 +51,9 @@ void Expr::destroy(Expr *_e, bool dec_kids) { case INT_EXPR: delete (IntExpr *)_e; break; + case RAT_EXPR: + delete (RatExpr *)_e; + break; case SYMS_EXPR: { SymSExpr *e = (SymSExpr *)_e; if (e->val && e->val->getop() != PROG) { diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h index 3473a9eae..f5cf3d02a 100644 --- a/proofs/lfsc_checker/expr.h +++ b/proofs/lfsc_checker/expr.h @@ -103,12 +103,15 @@ protected: Expr(int _class, int _op) : data(1 << 9 /* refcount 1, not cloned */| (_op << 3) | _class) - { } + { /*Expr::to_free.insert(this);*/ } bool _free_in(Expr *x, expr_ptr_set_t *visited); public: - virtual ~Expr() {} + static expr_ptr_set_t to_free; + virtual ~Expr() { + Expr::to_free.erase(this); + } static int markedCount; inline Expr* followDefs(); @@ -143,8 +146,9 @@ protected: debugrefcnt(ref,DEC); #endif assert(ref >= 0); - if (ref == 0) + if (ref == 0) { destroy(this,dec_kids); + } else data = (ref << 9) | (data & 511); } |