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

* iface/dve2/dve2check.cc (main): Catch out-of-memory errors

Browse source 
during emptiness check or counterexample generation.
This commit is contained in:
Alexandre Duret-Lutz 2011-04-06 09:37:48 +02:00
parent 5fdfe28689
commit 0368d653ca
2 changed files with 31 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2011-04-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* iface/dve2/dve2check.cc (main): Catch out-of-memory errors
during emptiness check or counterexample generation.
2011-04-03 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-04-03 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc: Use

29
iface/dve2/dve2check.cc
View file

@ -29,9 +29,10 @@
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
#include "misc/timer.hh" #include "misc/timer.hh"
#include "misc/memusage.hh"
#include <cstring> #include <cstring>
void static void
syntax(char* prog) syntax(char* prog)
{ {
// Display the supplied name unless it appears to be a libtool wrapper. // Display the supplied name unless it appears to be a libtool wrapper.
@ -256,7 +257,18 @@ main(int argc, char **argv)
do do
{ {
tm.start("running emptiness check"); tm.start("running emptiness check");
spot::emptiness_check_result* res = ec->check(); spot::emptiness_check_result* res;
try
{
res = ec->check();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory during emptiness check."
<< std::endl;
exit_code = 2;
exit(exit_code);
}
tm.stop("running emptiness check"); tm.stop("running emptiness check");
ec->print_stats(std::cout); ec->print_stats(std::cout);
@ -283,8 +295,19 @@ main(int argc, char **argv)
else if (accepting_run) else if (accepting_run)
{ {
spot::tgba_run* run;
tm.start("computing accepting run"); tm.start("computing accepting run");
spot::tgba_run* run = res->accepting_run(); try
{
run = res->accepting_run();
}
catch (std::bad_alloc)
{
std::cerr << "Out of memory while looking for counterexample."
<< std::endl;
exit_code = 2;
exit(exit_code);
}
tm.stop("computing accepting run"); tm.stop("computing accepting run");
if (!run) if (!run)