Skip to content

Commit

Permalink
fix contract for lddmc implementation of the vset interface.
Browse files Browse the repository at this point in the history
I.e. vset_next and vset_prev may be called such that dst == src.
In that case dst may not be gc'd.
  • Loading branch information
Meijuh committed Dec 19, 2014
1 parent fca4939 commit 4803d14
Showing 1 changed file with 16 additions and 4 deletions.
20 changes: 16 additions & 4 deletions src/vset-lib/vset_lddmc.c
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

Expand All @@ -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);
}

Expand Down

0 comments on commit 4803d14

Please sign in to comment.