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

ltlsynt: fix a memory leak

Browse source 
* bin/ltlsynt.cc: Declare the realizability_simplifier as a unique_ptr
so that it gets deleted after use.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2025-02-06 17:15:48 +01:00
parent aba0e8dd24
commit 27fb175276
2 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
NEWS
View file

@ -117,6 +117,8 @@ New in spot 2.12.2.dev (not yet released)
status and the AIG circuit; it now does the job silently as
requested.
- ltlsynt had a minor memory leak
New in spot 2.12.2 (2025-01-18)
Bug fixes:

12
bin/ltlsynt.cc
View file

@ -489,7 +489,7 @@ namespace
};
// Attempt to remove superfluous atomic propositions
spot::realizability_simplifier* rs = nullptr;
std::unique_ptr<spot::realizability_simplifier> rs = nullptr;
if (opt_polarity != pol_no || opt_gequiv != pol_no)
{
unsigned opt = 0;
@ -502,9 +502,9 @@ namespace
else
opt |= spot::realizability_simplifier::global_equiv;
}
rs =
new spot::realizability_simplifier(original_f, input_aps, opt,
gi ? gi->verbose_stream : nullptr);
rs.reset(new spot::realizability_simplifier(original_f, input_aps, opt,
gi ? gi->verbose_stream
: nullptr));
f = rs->simplified_formula();
}
@ -646,7 +646,7 @@ namespace
}
if (want_game())
{
dispatch_print_hoa(arena, rs);
dispatch_print_hoa(arena, rs.get());
continue;
}
if (!spot::solve_game(arena, *gi))
@ -732,7 +732,7 @@ namespace
if (gi->bv)
sw2.start();
saig = spot::mealy_machines_to_aig(mealy_machines, opt_aiger,
input_aps, sub_outs_str, rs);
input_aps, sub_outs_str, rs.get());
if (gi->bv)
{
gi->bv->aig_time = sw2.stop();