bin: plug several memory leaks
* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Destroy the translated formulas. * src/bin/ltlcheck.cc, src/bin/ltlfilt.cc: Free the unicity table on exit.
This commit is contained in:
parent
9f1d369563
commit
d9ceb4adc4
4 changed files with 22 additions and 6 deletions
|
|
@ -224,6 +224,7 @@ namespace
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
delete aut;
|
delete aut;
|
||||||
|
f->destroy();
|
||||||
flush_cout();
|
flush_cout();
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -229,6 +229,7 @@ namespace
|
||||||
}
|
}
|
||||||
|
|
||||||
delete aut;
|
delete aut;
|
||||||
|
f->destroy();
|
||||||
flush_cout();
|
flush_cout();
|
||||||
return 0;
|
return 0;
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -143,11 +143,6 @@ bool want_stats = false;
|
||||||
bool allow_dups = false;
|
bool allow_dups = false;
|
||||||
bool no_checks = false;
|
bool no_checks = false;
|
||||||
|
|
||||||
typedef Sgi::hash_set<const spot::ltl::formula*,
|
|
||||||
const spot::ptr_hash<const spot::ltl::formula> > fset_t;
|
|
||||||
|
|
||||||
fset_t unique_set;
|
|
||||||
|
|
||||||
std::vector<char*> translators;
|
std::vector<char*> translators;
|
||||||
bool global_error_flag = false;
|
bool global_error_flag = false;
|
||||||
|
|
||||||
|
|
@ -727,11 +722,23 @@ namespace
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
typedef
|
||||||
|
Sgi::hash_set<const spot::ltl::formula*,
|
||||||
|
const spot::ptr_hash<const spot::ltl::formula> > fset_t;
|
||||||
|
|
||||||
|
|
||||||
class processor: public job_processor
|
class processor: public job_processor
|
||||||
{
|
{
|
||||||
translator_runner runner;
|
translator_runner runner;
|
||||||
|
fset_t unique_set;
|
||||||
public:
|
public:
|
||||||
|
~processor()
|
||||||
|
{
|
||||||
|
fset_t::iterator i = unique_set.begin();
|
||||||
|
while (i != unique_set.end())
|
||||||
|
(*i++)->destroy();
|
||||||
|
}
|
||||||
|
|
||||||
int
|
int
|
||||||
process_formula(const spot::ltl::formula* f,
|
process_formula(const spot::ltl::formula* f,
|
||||||
const char* filename = 0, int linenum = 0)
|
const char* filename = 0, int linenum = 0)
|
||||||
|
|
|
||||||
|
|
@ -340,6 +340,13 @@ namespace
|
||||||
spot::ltl::ltl_simplifier& simpl;
|
spot::ltl::ltl_simplifier& simpl;
|
||||||
fset_t unique_set;
|
fset_t unique_set;
|
||||||
|
|
||||||
|
~ltl_processor()
|
||||||
|
{
|
||||||
|
fset_t::iterator i = unique_set.begin();
|
||||||
|
while (i != unique_set.end())
|
||||||
|
(*i++)->destroy();
|
||||||
|
}
|
||||||
|
|
||||||
ltl_processor(spot::ltl::ltl_simplifier& simpl)
|
ltl_processor(spot::ltl::ltl_simplifier& simpl)
|
||||||
: simpl(simpl)
|
: simpl(simpl)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue