Skip to content

Commit 5c23e11

Browse files
author
martin
committed
Remove some exception handling in goto-analyzer
This changes the return value in a few exceptional cases in favour of being clearer about when an exception is thrown and simplifying the code.
1 parent 920acd8 commit 5c23e11

File tree

2 files changed

+2
-56
lines changed

2 files changed

+2
-56
lines changed

src/goto-analyzer/goto_analyzer_parse_options.cpp

+2-55
Original file line numberDiff line numberDiff line change
@@ -555,8 +555,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
555555
return CPROVER_EXIT_SUCCESS;
556556
}
557557

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

561561
if(options.get_bool_option("general-analysis"))
562562
{
@@ -665,38 +665,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
665665
return CPROVER_EXIT_USAGE_ERROR;
666666
}
667667

668-
bool goto_analyzer_parse_optionst::set_properties()
669-
{
670-
try
671-
{
672-
if(cmdline.isset("property"))
673-
::set_properties(goto_model, cmdline.get_values("property"));
674-
}
675-
676-
catch(const char *e)
677-
{
678-
error() << e << eom;
679-
return true;
680-
}
681-
682-
catch(const std::string &e)
683-
{
684-
error() << e << eom;
685-
return true;
686-
}
687-
688-
catch(int)
689-
{
690-
return true;
691-
}
692-
693-
return false;
694-
}
695-
696668
bool goto_analyzer_parse_optionst::process_goto_program(
697669
const optionst &options)
698670
{
699-
try
700671
{
701672
#if 0
702673
// Remove inline assembler; this needs to happen before
@@ -738,30 +709,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
738709
// add loop ids
739710
goto_model.goto_functions.compute_loop_numbers();
740711
}
741-
742-
catch(const char *e)
743-
{
744-
error() << e << eom;
745-
return true;
746-
}
747-
748-
catch(const std::string &e)
749-
{
750-
error() << e << eom;
751-
return true;
752-
}
753-
754-
catch(int)
755-
{
756-
return true;
757-
}
758-
759-
catch(const std::bad_alloc &)
760-
{
761-
error() << "Out of memory" << eom;
762-
return true;
763-
}
764-
765712
return false;
766713
}
767714

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

0 commit comments

Comments
 (0)