Skip to content

Commit d52cd0d

Browse files
martin-csmartin-cs
authored
Merge pull request #3952 from martin-cs/fix/redirect-exception-handler-output-3
Fix/redirect exception handler output 3
2 parents 5745139 + a959df9 commit d52cd0d

File tree

12 files changed

+84
-246
lines changed

12 files changed

+84
-246
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 6 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,7 @@ Author: Daniel Kroening, [email protected]
5858
#include <goto-analyzer/unreachable_instructions.h>
5959

6060
janalyzer_parse_optionst::janalyzer_parse_optionst(int argc, const char **argv)
61-
: parse_options_baset(JANALYZER_OPTIONS, argc, argv),
61+
: parse_options_baset(JANALYZER_OPTIONS, argc, argv, ui_message_handler),
6262
messaget(ui_message_handler),
6363
ui_message_handler(cmdline, std::string("JANALYZER ") + CBMC_VERSION)
6464
{
@@ -355,29 +355,8 @@ int janalyzer_parse_optionst::doit()
355355

356356
register_languages();
357357

358-
try
359-
{
360-
goto_model =
361-
initialize_goto_model(cmdline.args, get_message_handler(), options);
362-
}
363-
364-
catch(const char *e)
365-
{
366-
error() << e << eom;
367-
return CPROVER_EXIT_EXCEPTION;
368-
}
369-
370-
catch(const std::string &e)
371-
{
372-
error() << e << eom;
373-
return CPROVER_EXIT_EXCEPTION;
374-
}
375-
376-
catch(int e)
377-
{
378-
error() << "Numeric exception: " << e << eom;
379-
return CPROVER_EXIT_EXCEPTION;
380-
}
358+
goto_model =
359+
initialize_goto_model(cmdline.args, get_message_handler(), options);
381360

382361
if(process_goto_program(options))
383362
return CPROVER_EXIT_INTERNAL_ERROR;
@@ -402,34 +381,7 @@ int janalyzer_parse_optionst::doit()
402381
return CPROVER_EXIT_SUCCESS;
403382
}
404383

405-
try
406-
{
407-
return perform_analysis(options);
408-
}
409-
410-
catch(const char *e)
411-
{
412-
error() << e << eom;
413-
return CPROVER_EXIT_EXCEPTION;
414-
}
415-
416-
catch(const std::string &e)
417-
{
418-
error() << e << eom;
419-
return CPROVER_EXIT_EXCEPTION;
420-
}
421-
422-
catch(int e)
423-
{
424-
error() << "Numeric exception: " << e << eom;
425-
return CPROVER_EXIT_EXCEPTION;
426-
}
427-
428-
catch(const std::bad_alloc &)
429-
{
430-
error() << "Out of memory" << eom;
431-
return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
432-
}
384+
return perform_analysis(options);
433385
}
434386

435387
/// Depending on the command line mode, run one of the analysis tasks
@@ -554,8 +506,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
554506
return CPROVER_EXIT_SUCCESS;
555507
}
556508

557-
if(set_properties())
558-
return CPROVER_EXIT_SET_PROPERTIES_FAILED;
509+
if(cmdline.isset("property"))
510+
::set_properties(goto_model, cmdline.get_values("property"));
559511

560512
if(options.get_bool_option("general-analysis"))
561513
{
@@ -637,34 +589,6 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
637589
return CPROVER_EXIT_USAGE_ERROR;
638590
}
639591

640-
bool janalyzer_parse_optionst::set_properties()
641-
{
642-
try
643-
{
644-
if(cmdline.isset("property"))
645-
::set_properties(goto_model, cmdline.get_values("property"));
646-
}
647-
648-
catch(const char *e)
649-
{
650-
error() << e << eom;
651-
return true;
652-
}
653-
654-
catch(const std::string &e)
655-
{
656-
error() << e << eom;
657-
return true;
658-
}
659-
660-
catch(int)
661-
{
662-
return true;
663-
}
664-
665-
return false;
666-
}
667-
668592
bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
669593
{
670594
try

‎jbmc/src/janalyzer/janalyzer_parse_options.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -167,7 +167,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
167167
virtual void get_command_line_options(optionst &options);
168168

169169
virtual bool process_goto_program(const optionst &options);
170-
bool set_properties();
171170

172171
virtual int perform_analysis(const optionst &options);
173172

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 9 additions & 107 deletions
Original file line numberDiff line numberDiff line change
@@ -70,7 +70,7 @@ Author: Daniel Kroening, [email protected]
7070
#include <java_bytecode/simple_method_stubbing.h>
7171

7272
jbmc_parse_optionst::jbmc_parse_optionst(int argc, const char **argv)
73-
: parse_options_baset(JBMC_OPTIONS, argc, argv),
73+
: parse_options_baset(JBMC_OPTIONS, argc, argv, ui_message_handler),
7474
messaget(ui_message_handler),
7575
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
7676
{
@@ -80,7 +80,11 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
8080
int argc,
8181
const char **argv,
8282
const std::string &extra_options)
83-
: parse_options_baset(JBMC_OPTIONS + extra_options, argc, argv),
83+
: parse_options_baset(
84+
JBMC_OPTIONS + extra_options,
85+
argc,
86+
argv,
87+
ui_message_handler),
8488
messaget(ui_message_handler),
8589
ui_message_handler(cmdline, std::string("JBMC ") + CBMC_VERSION)
8690
{
@@ -425,22 +429,7 @@ int jbmc_parse_optionst::doit()
425429
//
426430

427431
optionst options;
428-
try
429-
{
430-
get_command_line_options(options);
431-
}
432-
433-
catch(const char *error_msg)
434-
{
435-
error() << error_msg << eom;
436-
return 6; // should contemplate EX_SOFTWARE from sysexits.h
437-
}
438-
439-
catch(const std::string &error_msg)
440-
{
441-
error() << error_msg << eom;
442-
return 6; // should contemplate EX_SOFTWARE from sysexits.h
443-
}
432+
get_command_line_options(options);
444433

445434
//
446435
// Print a banner
@@ -636,28 +625,8 @@ int jbmc_parse_optionst::doit()
636625

637626
bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model)
638627
{
639-
try
640-
{
641-
if(cmdline.isset("property"))
642-
::set_properties(goto_model, cmdline.get_values("property"));
643-
}
644-
645-
catch(const char *e)
646-
{
647-
error() << e << eom;
648-
return true;
649-
}
650-
651-
catch(const std::string &e)
652-
{
653-
error() << e << eom;
654-
return true;
655-
}
656-
657-
catch(int)
658-
{
659-
return true;
660-
}
628+
if(cmdline.isset("property"))
629+
::set_properties(goto_model, cmdline.get_values("property"));
661630

662631
return false;
663632
}
@@ -672,7 +641,6 @@ int jbmc_parse_optionst::get_goto_program(
672641
return 6;
673642
}
674643

675-
try
676644
{
677645
lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
678646
*this, options, get_message_handler());
@@ -738,29 +706,6 @@ int jbmc_parse_optionst::get_goto_program(
738706
status() << config.object_bits_info() << eom;
739707
}
740708

741-
catch(const char *e)
742-
{
743-
error() << e << eom;
744-
return 6;
745-
}
746-
747-
catch(const std::string &e)
748-
{
749-
error() << e << eom;
750-
return 6;
751-
}
752-
753-
catch(int)
754-
{
755-
return 6;
756-
}
757-
758-
catch(const std::bad_alloc &)
759-
{
760-
error() << "Out of memory" << eom;
761-
return 6;
762-
}
763-
764709
return -1; // no error, continue
765710
}
766711

@@ -776,7 +721,6 @@ void jbmc_parse_optionst::process_goto_function(
776721
bool using_symex_driven_loading =
777722
options.get_bool_option("symex-driven-lazy-loading");
778723

779-
try
780724
{
781725
// Removal of RTTI inspection:
782726
remove_instanceof(
@@ -861,24 +805,6 @@ void jbmc_parse_optionst::process_goto_function(
861805
// update the function member in each instruction
862806
function.update_instructions_function();
863807
}
864-
865-
catch(const char *e)
866-
{
867-
error() << e << eom;
868-
throw;
869-
}
870-
871-
catch(const std::string &e)
872-
{
873-
error() << e << eom;
874-
throw;
875-
}
876-
877-
catch(const std::bad_alloc &)
878-
{
879-
error() << "Out of memory" << eom;
880-
throw;
881-
}
882808
}
883809

884810
bool jbmc_parse_optionst::show_loaded_functions(
@@ -933,7 +859,6 @@ bool jbmc_parse_optionst::process_goto_functions(
933859
goto_modelt &goto_model,
934860
const optionst &options)
935861
{
936-
try
937862
{
938863
status() << "Running GOTO functions transformation passes" << eom;
939864

@@ -1021,29 +946,6 @@ bool jbmc_parse_optionst::process_goto_functions(
1021946
remove_skip(goto_model);
1022947
}
1023948

1024-
catch(const char *e)
1025-
{
1026-
error() << e << eom;
1027-
return true;
1028-
}
1029-
1030-
catch(const std::string &e)
1031-
{
1032-
error() << e << eom;
1033-
return true;
1034-
}
1035-
1036-
catch(int)
1037-
{
1038-
return true;
1039-
}
1040-
1041-
catch(const std::bad_alloc &)
1042-
{
1043-
error() << "Out of memory" << eom;
1044-
return true;
1045-
}
1046-
1047949
return false;
1048950
}
1049951

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 6 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ Author: Peter Schrammel
6363
// TODO: do not use language_uit for this; requires a refactoring of
6464
// initialize_goto_model to support parsing specific command line files
6565
jdiff_parse_optionst::jdiff_parse_optionst(int argc, const char **argv)
66-
: parse_options_baset(JDIFF_OPTIONS, argc, argv),
66+
: parse_options_baset(JDIFF_OPTIONS, argc, argv, ui_message_handler),
6767
jdiff_languagest(cmdline, ui_message_handler, &options),
6868
ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
6969
languages2(cmdline, ui_message_handler, &options)
@@ -74,7 +74,11 @@ ::jdiff_parse_optionst::jdiff_parse_optionst(
7474
int argc,
7575
const char **argv,
7676
const std::string &extra_options)
77-
: parse_options_baset(JDIFF_OPTIONS + extra_options, argc, argv),
77+
: parse_options_baset(
78+
JDIFF_OPTIONS + extra_options,
79+
argc,
80+
argv,
81+
ui_message_handler),
7882
jdiff_languagest(cmdline, ui_message_handler, &options),
7983
ui_message_handler(cmdline, std::string("JDIFF ") + CBMC_VERSION),
8084
languages2(cmdline, ui_message_handler, &options)
@@ -342,7 +346,6 @@ bool jdiff_parse_optionst::process_goto_program(
342346
const optionst &options,
343347
goto_modelt &goto_model)
344348
{
345-
try
346349
{
347350
// remove function pointers
348351
status() << "Removing function pointers and virtual functions" << eom;
@@ -407,31 +410,6 @@ bool jdiff_parse_optionst::process_goto_program(
407410
goto_model.goto_functions.update();
408411
}
409412

410-
catch(const char *e)
411-
{
412-
error() << e << eom;
413-
return true;
414-
}
415-
416-
catch(const std::string &e)
417-
{
418-
error() << e << eom;
419-
return true;
420-
}
421-
422-
catch(int e)
423-
{
424-
error() << "Numeric exception: " << e << eom;
425-
return true;
426-
}
427-
428-
catch(const std::bad_alloc &)
429-
{
430-
error() << "Out of memory" << eom;
431-
exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
432-
return true;
433-
}
434-
435413
return false;
436414
}
437415

‎regression/cbmc/json-ui/no_entry.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
KNOWNBUG
1+
CORE
22
no_entry.c
33
--json-ui
44
activate-multi-line-match
55
^EXIT=6$
66
^SIGNAL=0$
7-
"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR",
7+
"messageText": "the program has no entry point",[\n ]*"messageType": "ERROR"
88
--
99
^warning: ignoring
1010
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)