Skip to content

Commit cf96cef

Browse files
author
martin
committed
Minor changes to erronious exit behaviour.
Change one exit code to something that seems more suitable, output integer exceptions and immediate abort once out of memory is detected.
1 parent c8dfd48 commit cf96cef

File tree

1 file changed

+11
-5
lines changed

1 file changed

+11
-5
lines changed

src/cbmc/cbmc_parse_options.cpp

+11-5
Original file line numberDiff line numberDiff line change
@@ -557,7 +557,7 @@ int cbmc_parse_optionst::doit()
557557
catch(const char *error_msg)
558558
{
559559
error() << error_msg << eom;
560-
return CPROVER_EXIT_USAGE_ERROR; // should contemplate EX_SOFTWARE from sysexits.h
560+
return CPROVER_EXIT_EXCEPTION;
561561
}
562562

563563
prop_convt &prop_conv=cbmc_solver->prop_conv();
@@ -595,8 +595,9 @@ bool cbmc_parse_optionst::set_properties()
595595
return true;
596596
}
597597

598-
catch(int)
598+
catch(int e)
599599
{
600+
error() << "Numeric exception : " << e << eom;
600601
return true;
601602
}
602603

@@ -654,8 +655,9 @@ int cbmc_parse_optionst::get_goto_program(
654655
return CPROVER_EXIT_EXCEPTION;
655656
}
656657

657-
catch(int)
658+
catch(int e)
658659
{
660+
error() << "Numeric exception : " << e << eom;
659661
return CPROVER_EXIT_EXCEPTION;
660662
}
661663

@@ -713,13 +715,15 @@ void cbmc_parse_optionst::preprocessing()
713715
error() << e << eom;
714716
}
715717

716-
catch(int)
718+
catch(int e)
717719
{
720+
error() << "Numeric exception : " << e << eom;
718721
}
719722

720723
catch(std::bad_alloc)
721724
{
722725
error() << "Out of memory" << eom;
726+
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
723727
}
724728
}
725729

@@ -846,14 +850,16 @@ bool cbmc_parse_optionst::process_goto_program(
846850
return true;
847851
}
848852

849-
catch(int)
853+
catch(int e)
850854
{
855+
error() << "Numeric exception : " << e << eom;
851856
return true;
852857
}
853858

854859
catch(std::bad_alloc)
855860
{
856861
error() << "Out of memory" << eom;
862+
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
857863
return true;
858864
}
859865

0 commit comments

Comments
 (0)