Skip to content

Commit 07fa10e

Browse files
tautschnigtautschnig
authored
Merge pull request #3897 from martin-cs/fix/simplify-exception-handling
Fix/simplify exception handling
2 parents 821a4f7 + 2212653 commit 07fa10e

7 files changed

+44
-280
lines changed

‎src/cbmc/cbmc_parse_options.cpp

+5-120
Original file line numberDiff line numberDiff line change
@@ -433,22 +433,7 @@ int cbmc_parse_optionst::doit()
433433
//
434434

435435
optionst options;
436-
try
437-
{
438-
get_command_line_options(options);
439-
}
440-
441-
catch(const char *error_msg)
442-
{
443-
error() << error_msg << eom;
444-
return CPROVER_EXIT_EXCEPTION;
445-
}
446-
447-
catch(const std::string &error_msg)
448-
{
449-
error() << error_msg << eom;
450-
return CPROVER_EXIT_EXCEPTION;
451-
}
436+
get_command_line_options(options);
452437

453438
eval_verbosity(
454439
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
@@ -575,32 +560,11 @@ int cbmc_parse_optionst::doit()
575560

576561
bool cbmc_parse_optionst::set_properties()
577562
{
578-
try
579-
{
580-
if(cmdline.isset("claim")) // will go away
581-
::set_properties(goto_model, cmdline.get_values("claim"));
563+
if(cmdline.isset("claim")) // will go away
564+
::set_properties(goto_model, cmdline.get_values("claim"));
582565

583-
if(cmdline.isset("property")) // use this one
584-
::set_properties(goto_model, cmdline.get_values("property"));
585-
}
586-
587-
catch(const char *e)
588-
{
589-
error() << e << eom;
590-
return true;
591-
}
592-
593-
catch(const std::string &e)
594-
{
595-
error() << e << eom;
596-
return true;
597-
}
598-
599-
catch(int e)
600-
{
601-
error() << "Numeric exception : " << e << eom;
602-
return true;
603-
}
566+
if(cmdline.isset("property")) // use this one
567+
::set_properties(goto_model, cmdline.get_values("property"));
604568

605569
return false;
606570
}
@@ -618,7 +582,6 @@ int cbmc_parse_optionst::get_goto_program(
618582
return CPROVER_EXIT_INCORRECT_TASK;
619583
}
620584

621-
try
622585
{
623586
goto_model =
624587
initialize_goto_model(cmdline.args, ui_message_handler, options);
@@ -655,42 +618,11 @@ int cbmc_parse_optionst::get_goto_program(
655618
log.status() << config.object_bits_info() << log.eom;
656619
}
657620

658-
catch(incorrect_goto_program_exceptiont &e)
659-
{
660-
log.error() << e.what() << log.eom;
661-
return CPROVER_EXIT_EXCEPTION;
662-
}
663-
664-
catch(const char *e)
665-
{
666-
log.error() << e << log.eom;
667-
return CPROVER_EXIT_EXCEPTION;
668-
}
669-
670-
catch(const std::string &e)
671-
{
672-
log.error() << e << log.eom;
673-
return CPROVER_EXIT_EXCEPTION;
674-
}
675-
676-
catch(int e)
677-
{
678-
log.error() << "Numeric exception : " << e << log.eom;
679-
return CPROVER_EXIT_EXCEPTION;
680-
}
681-
682-
catch(const std::bad_alloc &)
683-
{
684-
log.error() << "Out of memory" << log.eom;
685-
return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
686-
}
687-
688621
return -1; // no error, continue
689622
}
690623

691624
void cbmc_parse_optionst::preprocessing(const optionst &options)
692625
{
693-
try
694626
{
695627
if(cmdline.args.size()!=1)
696628
{
@@ -722,35 +654,13 @@ void cbmc_parse_optionst::preprocessing(const optionst &options)
722654
if(language->preprocess(infile, filename, std::cout))
723655
error() << "PREPROCESSING ERROR" << eom;
724656
}
725-
726-
catch(const char *e)
727-
{
728-
error() << e << eom;
729-
}
730-
731-
catch(const std::string &e)
732-
{
733-
error() << e << eom;
734-
}
735-
736-
catch(int e)
737-
{
738-
error() << "Numeric exception : " << e << eom;
739-
}
740-
741-
catch(const std::bad_alloc &)
742-
{
743-
error() << "Out of memory" << eom;
744-
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
745-
}
746657
}
747658

748659
bool cbmc_parse_optionst::process_goto_program(
749660
goto_modelt &goto_model,
750661
const optionst &options,
751662
messaget &log)
752663
{
753-
try
754664
{
755665
// Remove inline assembler; this needs to happen before
756666
// adding the library.
@@ -878,31 +788,6 @@ bool cbmc_parse_optionst::process_goto_program(
878788
remove_skip(goto_model);
879789
}
880790

881-
catch(const char *e)
882-
{
883-
log.error() << e << eom;
884-
return true;
885-
}
886-
887-
catch(const std::string &e)
888-
{
889-
log.error() << e << eom;
890-
return true;
891-
}
892-
893-
catch(int e)
894-
{
895-
log.error() << "Numeric exception : " << e << eom;
896-
return true;
897-
}
898-
899-
catch(const std::bad_alloc &)
900-
{
901-
log.error() << "Out of memory" << eom;
902-
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
903-
return true;
904-
}
905-
906791
return false;
907792
}
908793

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+5-106
Original file line numberDiff line numberDiff line change
@@ -396,29 +396,8 @@ int goto_analyzer_parse_optionst::doit()
396396

397397
register_languages();
398398

399-
try
400-
{
401-
goto_model =
402-
initialize_goto_model(cmdline.args, get_message_handler(), options);
403-
}
404-
405-
catch(const char *e)
406-
{
407-
error() << e << eom;
408-
return CPROVER_EXIT_EXCEPTION;
409-
}
410-
411-
catch(const std::string &e)
412-
{
413-
error() << e << eom;
414-
return CPROVER_EXIT_EXCEPTION;
415-
}
416-
417-
catch(int e)
418-
{
419-
error() << "Numeric exception: " << e << eom;
420-
return CPROVER_EXIT_EXCEPTION;
421-
}
399+
goto_model =
400+
initialize_goto_model(cmdline.args, get_message_handler(), options);
422401

423402
if(process_goto_program(options))
424403
return CPROVER_EXIT_INTERNAL_ERROR;
@@ -448,34 +427,7 @@ int goto_analyzer_parse_optionst::doit()
448427
return CPROVER_EXIT_SUCCESS;
449428
}
450429

451-
try
452-
{
453-
return perform_analysis(options);
454-
}
455-
456-
catch(const char *e)
457-
{
458-
error() << e << eom;
459-
return CPROVER_EXIT_EXCEPTION;
460-
}
461-
462-
catch(const std::string &e)
463-
{
464-
error() << e << eom;
465-
return CPROVER_EXIT_EXCEPTION;
466-
}
467-
468-
catch(int e)
469-
{
470-
error() << "Numeric exception: " << e << eom;
471-
return CPROVER_EXIT_EXCEPTION;
472-
}
473-
474-
catch(const std::bad_alloc &)
475-
{
476-
error() << "Out of memory" << eom;
477-
return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
478-
}
430+
return perform_analysis(options);
479431
}
480432

481433

@@ -603,8 +555,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
603555
return CPROVER_EXIT_SUCCESS;
604556
}
605557

606-
if(set_properties())
607-
return CPROVER_EXIT_SET_PROPERTIES_FAILED;
558+
if(cmdline.isset("property"))
559+
::set_properties(goto_model, cmdline.get_values("property"));
608560

609561
if(options.get_bool_option("general-analysis"))
610562
{
@@ -713,38 +665,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
713665
return CPROVER_EXIT_USAGE_ERROR;
714666
}
715667

716-
bool goto_analyzer_parse_optionst::set_properties()
717-
{
718-
try
719-
{
720-
if(cmdline.isset("property"))
721-
::set_properties(goto_model, cmdline.get_values("property"));
722-
}
723-
724-
catch(const char *e)
725-
{
726-
error() << e << eom;
727-
return true;
728-
}
729-
730-
catch(const std::string &e)
731-
{
732-
error() << e << eom;
733-
return true;
734-
}
735-
736-
catch(int)
737-
{
738-
return true;
739-
}
740-
741-
return false;
742-
}
743-
744668
bool goto_analyzer_parse_optionst::process_goto_program(
745669
const optionst &options)
746670
{
747-
try
748671
{
749672
#if 0
750673
// Remove inline assembler; this needs to happen before
@@ -786,30 +709,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
786709
// add loop ids
787710
goto_model.goto_functions.compute_loop_numbers();
788711
}
789-
790-
catch(const char *e)
791-
{
792-
error() << e << eom;
793-
return true;
794-
}
795-
796-
catch(const std::string &e)
797-
{
798-
error() << e << eom;
799-
return true;
800-
}
801-
802-
catch(int)
803-
{
804-
return true;
805-
}
806-
807-
catch(const std::bad_alloc &)
808-
{
809-
error() << "Out of memory" << eom;
810-
return true;
811-
}
812-
813712
return false;
814713
}
815714

‎src/goto-analyzer/goto_analyzer_parse_options.h

-1
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,6 @@ class goto_analyzer_parse_optionst:
172172
virtual void get_command_line_options(optionst &options);
173173

174174
virtual bool process_goto_program(const optionst &options);
175-
bool set_properties();
176175

177176
virtual int perform_analysis(const optionst &options);
178177

‎src/goto-diff/goto_diff_parse_options.cpp

-26
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,6 @@ bool goto_diff_parse_optionst::process_goto_program(
386386
const optionst &options,
387387
goto_modelt &goto_model)
388388
{
389-
try
390389
{
391390
// Remove inline assembler; this needs to happen before
392391
// adding the library.
@@ -450,31 +449,6 @@ bool goto_diff_parse_optionst::process_goto_program(
450449
remove_skip(goto_model);
451450
}
452451

453-
catch(const char *e)
454-
{
455-
error() << e << eom;
456-
return true;
457-
}
458-
459-
catch(const std::string &e)
460-
{
461-
error() << e << eom;
462-
return true;
463-
}
464-
465-
catch(int e)
466-
{
467-
error() << "Numeric exception: " << e << eom;
468-
return true;
469-
}
470-
471-
catch(const std::bad_alloc &)
472-
{
473-
error() << "Out of memory" << eom;
474-
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
475-
return true;
476-
}
477-
478452
return false;
479453
}
480454

0 commit comments

Comments
 (0)