diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index b65ccbe8da7..3b616623b9e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -106,7 +107,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(config.set(cmdline)) { usage_error(); - exit(1); // should contemplate EX_USAGE from sysexits.h + exit(CPROVER_EXIT_USAGE_ERROR); } if(cmdline.isset("program-only")) @@ -224,7 +225,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) { error() << "--partial-loops and --unwinding-assertions " << "must not be given together" << eom; - exit(1); // should contemplate EX_USAGE from sysexits.h + exit(CPROVER_EXIT_USAGE_ERROR); } // remove unused equations @@ -415,7 +416,7 @@ int cbmc_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; // should contemplate EX_OK from sysexits.h + return CPROVER_EXIT_SUCCESS; } // @@ -431,13 +432,13 @@ int cbmc_parse_optionst::doit() catch(const char *error_msg) { error() << error_msg << eom; - return 6; // should contemplate EX_SOFTWARE from sysexits.h + return CPROVER_EXIT_EXCEPTION; } catch(const std::string error_msg) { error() << error_msg << eom; - return 6; // should contemplate EX_SOFTWARE from sysexits.h + return CPROVER_EXIT_EXCEPTION; } eval_verbosity(); @@ -459,18 +460,20 @@ int cbmc_parse_optionst::doit() { error() << "This version of CBMC has no support for " " hardware modules. Please use hw-cbmc." << eom; - return 1; // should contemplate EX_USAGE from sysexits.h + return CPROVER_EXIT_USAGE_ERROR; } register_languages(); if(cmdline.isset("test-preprocessor")) - return test_c_preprocessor(get_message_handler())?8:0; + return test_c_preprocessor(get_message_handler()) + ? CPROVER_EXIT_PREPROCESSOR_TEST_FAILED + : CPROVER_EXIT_SUCCESS; if(cmdline.isset("preprocess")) { preprocessing(); - return 0; // should contemplate EX_OK from sysexits.h + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-parse-tree")) @@ -479,7 +482,7 @@ int cbmc_parse_optionst::doit() is_goto_binary(cmdline.args[0])) { error() << "Please give exactly one source file" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } std::string filename=cmdline.args[0]; @@ -494,7 +497,7 @@ int cbmc_parse_optionst::doit() { error() << "failed to open input file `" << filename << "'" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } std::unique_ptr language= @@ -504,7 +507,7 @@ int cbmc_parse_optionst::doit() { error() << "failed to figure out type of file `" << filename << "'" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } language->get_language_options(cmdline); @@ -515,11 +518,11 @@ int cbmc_parse_optionst::doit() if(language->parse(infile, filename)) { error() << "PARSING ERROR" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } language->show_parse(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } int get_goto_program_ret=get_goto_program(options); @@ -531,11 +534,11 @@ int cbmc_parse_optionst::doit() cmdline.isset("show-properties")) // use this one { show_properties(goto_model, ui_message_handler.get_ui()); - return 0; // should contemplate EX_OK from sysexits.h + return CPROVER_EXIT_SUCCESS; } if(set_properties()) - return 7; // should contemplate EX_USAGE from sysexits.h + return CPROVER_EXIT_SET_PROPERTIES_FAILED; // get solver cbmc_solverst cbmc_solvers( @@ -554,7 +557,7 @@ int cbmc_parse_optionst::doit() catch(const char *error_msg) { error() << error_msg << eom; - return 1; // should contemplate EX_SOFTWARE from sysexits.h + return CPROVER_EXIT_EXCEPTION; } prop_convt &prop_conv=cbmc_solver->prop_conv(); @@ -592,8 +595,9 @@ bool cbmc_parse_optionst::set_properties() return true; } - catch(int) + catch(int e) { + error() << "Numeric exception : " << e << eom; return true; } @@ -606,7 +610,7 @@ int cbmc_parse_optionst::get_goto_program( if(cmdline.args.empty()) { error() << "Please provide a program to verify" << eom; - return 6; + return CPROVER_EXIT_INCORRECT_TASK; } try @@ -616,24 +620,24 @@ int cbmc_parse_optionst::get_goto_program( if(cmdline.isset("show-symbol-table")) { show_symbol_table(goto_model, ui_message_handler.get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(process_goto_program(options)) - return 6; + return CPROVER_EXIT_INTERNAL_ERROR; // show it? if(cmdline.isset("show-loops")) { show_loop_ids(ui_message_handler.get_ui(), goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } // show it? if(cmdline.isset("show-goto-functions")) { show_goto_functions(goto_model, ui_message_handler.get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } status() << config.object_bits_info() << eom; @@ -642,24 +646,25 @@ int cbmc_parse_optionst::get_goto_program( catch(const char *e) { error() << e << eom; - return 6; + return CPROVER_EXIT_EXCEPTION; } catch(const std::string e) { error() << e << eom; - return 6; + return CPROVER_EXIT_EXCEPTION; } - catch(int) + catch(int e) { - return 6; + error() << "Numeric exception : " << e << eom; + return CPROVER_EXIT_EXCEPTION; } catch(std::bad_alloc) { error() << "Out of memory" << eom; - return 6; + return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY; } return -1; // no error, continue @@ -710,13 +715,15 @@ void cbmc_parse_optionst::preprocessing() error() << e << eom; } - catch(int) + catch(int e) { + error() << "Numeric exception : " << e << eom; } catch(std::bad_alloc) { error() << "Out of memory" << eom; + exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); } } @@ -843,14 +850,16 @@ bool cbmc_parse_optionst::process_goto_program( return true; } - catch(int) + catch(int e) { + error() << "Numeric exception : " << e << eom; return true; } catch(std::bad_alloc) { error() << "Out of memory" << eom; + exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY); return true; } @@ -862,19 +871,19 @@ int cbmc_parse_optionst::do_bmc(bmct &bmc) { bmc.set_ui(ui_message_handler.get_ui()); - int result=6; + int result = CPROVER_EXIT_INTERNAL_ERROR; // do actual BMC switch(bmc.run(goto_model.goto_functions)) { case safety_checkert::resultt::SAFE: - result=0; + result = CPROVER_EXIT_VERIFICATION_SAFE; break; case safety_checkert::resultt::UNSAFE: - result=10; + result = CPROVER_EXIT_VERIFICATION_UNSAFE; break; case safety_checkert::resultt::ERROR: - result=6; + result = CPROVER_EXIT_INTERNAL_ERROR; break; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 5fa1567001b..bc6d55d960b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -118,13 +119,13 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("version")) { std::cout << CBMC_VERSION << '\n'; - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.args.size()!=1 && cmdline.args.size()!=2) { help(); - return 0; + return CPROVER_EXIT_USAGE_ERROR; } eval_verbosity(); @@ -269,7 +270,7 @@ int goto_instrument_parse_optionst::doit() value_set_analysist value_set_analysis(ns); value_set_analysis(goto_model.goto_functions); show_value_sets(get_ui(), goto_model, value_set_analysis); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-global-may-alias")) @@ -285,7 +286,7 @@ int goto_instrument_parse_optionst::doit() global_may_alias_analysis(goto_model); global_may_alias_analysis.output(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-local-bitvector-analysis")) @@ -308,7 +309,7 @@ int goto_instrument_parse_optionst::doit() std::cout << '\n'; } - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-custom-bitvector-analysis")) @@ -332,7 +333,7 @@ int goto_instrument_parse_optionst::doit() custom_bitvector_analysis(goto_model); custom_bitvector_analysis.output(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-escape-analysis")) @@ -348,7 +349,7 @@ int goto_instrument_parse_optionst::doit() escape_analysis(goto_model); escape_analysis.output(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("custom-bitvector-analysis")) @@ -377,7 +378,7 @@ int goto_instrument_parse_optionst::doit() cmdline.isset("xml-ui"), std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-points-to")) @@ -393,7 +394,7 @@ int goto_instrument_parse_optionst::doit() points_tot points_to; points_to(goto_model); points_to.output(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-intervals")) @@ -408,21 +409,21 @@ int goto_instrument_parse_optionst::doit() ait interval_analysis; interval_analysis(goto_model); interval_analysis.output(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-call-sequences")) { do_indirect_call_and_rtti_removal(); show_call_sequences(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("check-call-sequence")) { do_remove_returns(); check_call_sequence(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("list-calls-args")) @@ -431,7 +432,7 @@ int goto_instrument_parse_optionst::doit() list_calls_and_arguments(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-rw-set")) @@ -455,13 +456,13 @@ int goto_instrument_parse_optionst::doit() std::cout << rw_set_functiont(value_set_analysis, goto_model, main); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-symbol-table")) { ::show_symbol_table(goto_model, get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-reaching-definitions")) @@ -473,7 +474,7 @@ int goto_instrument_parse_optionst::doit() rd_analysis(goto_model); rd_analysis.output(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-dependence-graph")) @@ -486,44 +487,44 @@ int goto_instrument_parse_optionst::doit() dependence_graph.output(goto_model, std::cout); dependence_graph.output_dot(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("count-eloc")) { count_eloc(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("list-eloc")) { list_eloc(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("print-path-lengths")) { print_path_lengths(goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("list-symbols")) { show_symbol_table_brief(goto_model, get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-uninitialized")) { show_uninitialized(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("interpreter")) { status() << "Starting interpreter" << eom; interpreter(goto_model, get_message_handler()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-claims") || @@ -531,33 +532,33 @@ int goto_instrument_parse_optionst::doit() { const namespacet ns(goto_model.symbol_table); show_properties(goto_model, get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("document-claims-html") || cmdline.isset("document-properties-html")) { document_properties_html(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("document-claims-latex") || cmdline.isset("document-properties-latex")) { document_properties_latex(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-loops")) { show_loop_ids(get_ui(), goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-natural-loops")) { show_natural_loops(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("print-internal-representation")) @@ -570,33 +571,33 @@ int goto_instrument_parse_optionst::doit() if(ins.guard.is_not_nil()) status() << "[guard] " << ins.guard.pretty() << eom; } - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-goto-functions")) { namespacet ns(goto_model.symbol_table); show_goto_functions(goto_model, get_ui()); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("list-undefined-functions")) { list_undefined_functions(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } // experimental: print structs if(cmdline.isset("show-struct-alignment")) { print_struct_alignment_problems(goto_model.symbol_table, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("show-locations")) { show_locations(get_ui(), goto_model); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp")) @@ -621,7 +622,7 @@ int goto_instrument_parse_optionst::doit() if(!out) { error() << "failed to write to `" << cmdline.args[1] << "'"; - return 10; + return CPROVER_EXIT_CONVERSION_FAILED; } (is_cpp ? dump_cpp : dump_c)( goto_model.goto_functions, @@ -640,7 +641,7 @@ int goto_instrument_parse_optionst::doit() ns, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("call-graph")) @@ -655,7 +656,7 @@ int goto_instrument_parse_optionst::doit() else call_graph.output(std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("dot")) @@ -672,7 +673,7 @@ int goto_instrument_parse_optionst::doit() if(!out) { error() << "failed to write to " << cmdline.args[1] << "'"; - return 10; + return CPROVER_EXIT_CONVERSION_FAILED; } dot(goto_model, out); @@ -680,7 +681,7 @@ int goto_instrument_parse_optionst::doit() else dot(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("accelerate")) @@ -715,7 +716,7 @@ int goto_instrument_parse_optionst::doit() { error() << "Failed to open output file " << cmdline.args[1] << eom; - return 1; + return CPROVER_EXIT_CONVERSION_FAILED; } horn_encoding(goto_model, out); @@ -723,7 +724,7 @@ int goto_instrument_parse_optionst::doit() else horn_encoding(goto_model, std::cout); - return 0; + return CPROVER_EXIT_SUCCESS; } if(cmdline.isset("drop-unused-functions")) @@ -747,36 +748,37 @@ int goto_instrument_parse_optionst::doit() if(write_goto_binary( cmdline.args[1], goto_model, get_message_handler())) - return 1; + return CPROVER_EXIT_CONVERSION_FAILED; else - return 0; + return CPROVER_EXIT_SUCCESS; } help(); - return 0; + return CPROVER_EXIT_USAGE_ERROR; } catch(const char *e) { error() << e << eom; - return 11; + return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT; } catch(const std::string e) { error() << e << eom; - return 11; + return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT; } - catch(int) + catch(int e) { - return 11; + error() << "Numeric exception : " << e << eom; + return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT; } catch(std::bad_alloc) { error() << "Out of memory" << eom; - return 11; + return CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT; } // NOLINTNEXTLINE(readability/fn_size) } diff --git a/src/util/exit_codes.h b/src/util/exit_codes.h new file mode 100644 index 00000000000..52dacda4b25 --- /dev/null +++ b/src/util/exit_codes.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + +Module: Exit codes + +Author: Martin Brain, martin.brain@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_EXIT_CODES_H +#define CPROVER_UTIL_EXIT_CODES_H + +/// \file +/// Document and give macros for the exit codes of CPROVER binaries. + +/// Success indicates the required analysis has been performed without error. +#define CPROVER_EXIT_SUCCESS 0 +// should contemplate EX_OK from sysexits.h + +/// Verification successful indiciates the analysis has been performed without +/// error AND the software is safe (w.r.t. the current analysis / config / spec) +#define CPROVER_EXIT_VERIFICATION_SAFE 0 + +/// Verification successful indiciates the analysis has been performed without +/// error AND the software is not safe (w.r.t. current analysis / config / spec) +#define CPROVER_EXIT_VERIFICATION_UNSAFE 10 + +/// A usage error is returned when the command line is invalid or conflicting. +#define CPROVER_EXIT_USAGE_ERROR 1 +// should contemplate EX_USAGE from sysexits.h + +/// An error during parsing of the input program +#define CPROVER_EXIT_PARSE_ERROR 2 +// This should be the same as YY_EXIT_FAILURE + +/// An (unanticipated) exception was thrown during computation. +#define CPROVER_EXIT_EXCEPTION 6 +// should contemplate EX_SOFTWARE from sysexits.h +#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11 + +/// An error has been encountered during processing the requested analysis. +#define CPROVER_EXIT_INTERNAL_ERROR 6 + +/// The command line is correctly structured but cannot be carried out +/// due to missing files, invalid file types, etc. +#define CPROVER_EXIT_INCORRECT_TASK 6 + +/// Memory allocation has failed and this has been detected within the program. +#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY 6 + +/// Failure to identify the properties to verify +#define CPROVER_EXIT_SET_PROPERTIES_FAILED 7 +// should contemplate EX_USAGE from sysexits.h + +/// Failure of the test-preprocessor method +#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED 8 + +/// Failure to convert / write to another format +#define CPROVER_EXIT_CONVERSION_FAILED 10 + +#endif // CPROVER_UTIL_EXIT_CODES_H