alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

lpar13: avoid leak when counterexample detected

Browse source 
* spot/mc/lpar13.hh: Here.
This commit is contained in:
Etienne Renault 2020-06-09 17:04:26 +02:00
parent 13402a63c4
commit 9411dab738
1 changed files with 13 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/mc/lpar13.hh
View file

@ -95,6 +95,11 @@ namespace spot
virtual ~lpar13() virtual ~lpar13()
{ {
map.clear(); map.clear();
while (!todo.empty())
{
sys_.recycle(todo.back().it_kripke, tid_);
todo.pop_back();
}
} }
bool run() bool run()
@ -353,14 +358,19 @@ namespace spot
while (!bfs.empty()) while (!bfs.empty())
{ {
auto* e = bfs.front(); auto* e = bfs.front();
sys_.recycle(e->it_kripke, tid_);
bfs.pop(); bfs.pop();
delete e; delete e;
} }
sys_.recycle(front->it_kripke, tid_);
delete front;
// update acceptance // update acceptance
acc |= mark; acc |= mark;
if (twa_->acc().accepting(acc)) if (twa_->acc().accepting(acc))
return res; {
return res;
}
const product_state* q = &(it->first); const product_state* q = &(it->first);
ctrx_element* root = new ctrx_element({ ctrx_element* root = new ctrx_element({
@ -386,6 +396,8 @@ namespace spot
front->it_prop->reset(); front->it_prop->reset();
front->it_kripke->next(); front->it_kripke->next();
} }
sys_.recycle(front->it_kripke, tid_);
delete front;
} }
// never reach here; // never reach here;