From 4803d1450538c17f3aaed6f9d0b61f4574751e8e Mon Sep 17 00:00:00 2001 From: Jeroen Meijer Date: Fri, 19 Dec 2014 13:06:24 +0100 Subject: [PATCH] fix contract for lddmc implementation of the vset interface. I.e. vset_next and vset_prev may be called such that dst == src. In that case dst may not be gc'd. --- src/vset-lib/vset_lddmc.c | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/vset-lib/vset_lddmc.c b/src/vset-lib/vset_lddmc.c index b86319c55..b78c9ecb6 100644 --- a/src/vset-lib/vset_lddmc.c +++ b/src/vset-lib/vset_lddmc.c @@ -514,8 +514,14 @@ set_next(vset_t dst, vset_t src, vrel_t rel) entermt(dst); LACE_ME; assert(dst->size == src->size); - lddmc_deref(dst->mdd); - dst->mdd = lddmc_ref(lddmc_relprod(src->mdd, rel->mdd, rel->meta)); + if (dst == src) { + MDD old = dst->mdd; + dst->mdd = lddmc_ref(lddmc_relprod(src->mdd, rel->mdd, rel->meta)); + lddmc_deref(old); + } else { + lddmc_deref(dst->mdd); + dst->mdd = lddmc_ref(lddmc_relprod(src->mdd, rel->mdd, rel->meta)); + } leavemt(dst); } @@ -526,8 +532,14 @@ set_prev(vset_t dst, vset_t src, vrel_t rel, vset_t universe) LACE_ME; assert(dst->size == src->size); assert(dst->size == universe->size); - lddmc_deref(dst->mdd); - dst->mdd = lddmc_ref(lddmc_relprev(src->mdd, rel->mdd, rel->meta, universe->mdd)); + if (dst == src) { + MDD old = dst->mdd; + dst->mdd = lddmc_ref(lddmc_relprev(src->mdd, rel->mdd, rel->meta, universe->mdd)); + lddmc_deref(old); + } else { + lddmc_deref(dst->mdd); + dst->mdd = lddmc_ref(lddmc_relprev(src->mdd, rel->mdd, rel->meta, universe->mdd)); + } leavemt(dst); }