cprover
|
Document and give macros for the exit codes of CPROVER binaries. More...
Go to the source code of this file.
Macros | |
#define | CPROVER_EXIT_SUCCESS 0 |
Success indicates the required analysis has been performed without error. More... | |
#define | CPROVER_EXIT_VERIFICATION_SAFE 0 |
Verification successful indiciates the analysis has been performed without error AND the software is safe (w.r.t. More... | |
#define | CPROVER_EXIT_VERIFICATION_UNSAFE 10 |
Verification successful indiciates the analysis has been performed without error AND the software is not safe (w.r.t. More... | |
#define | CPROVER_EXIT_USAGE_ERROR 1 |
A usage error is returned when the command line is invalid or conflicting. More... | |
#define | CPROVER_EXIT_PARSE_ERROR 2 |
An error during parsing of the input program. More... | |
#define | CPROVER_EXIT_EXCEPTION 6 |
An (unanticipated) exception was thrown during computation. More... | |
#define | CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11 |
#define | CPROVER_EXIT_INTERNAL_ERROR 6 |
An error has been encountered during processing the requested analysis. More... | |
#define | CPROVER_EXIT_INCORRECT_TASK 6 |
The command line is correctly structured but cannot be carried out due to missing files, invalid file types, etc. More... | |
#define | CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY 6 |
Memory allocation has failed and this has been detected within the program. More... | |
#define | CPROVER_EXIT_SET_PROPERTIES_FAILED 7 |
Failure to identify the properties to verify. More... | |
#define | CPROVER_EXIT_PREPROCESSOR_TEST_FAILED 8 |
Failure of the test-preprocessor method. More... | |
#define | CPROVER_EXIT_CONVERSION_FAILED 10 |
Failure to convert / write to another format. More... | |
Document and give macros for the exit codes of CPROVER binaries.
Definition in file exit_codes.h.
#define CPROVER_EXIT_CONVERSION_FAILED 10 |
Failure to convert / write to another format.
Definition at line 58 of file exit_codes.h.
Referenced by goto_instrument_parse_optionst::doit().
#define CPROVER_EXIT_EXCEPTION 6 |
An (unanticipated) exception was thrown during computation.
Definition at line 36 of file exit_codes.h.
Referenced by bmct::do_language_agnostic_bmc(), cbmc_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), and cbmc_parse_optionst::get_goto_program().
#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11 |
Definition at line 38 of file exit_codes.h.
Referenced by goto_instrument_parse_optionst::doit().
#define CPROVER_EXIT_INCORRECT_TASK 6 |
The command line is correctly structured but cannot be carried out due to missing files, invalid file types, etc.
Definition at line 45 of file exit_codes.h.
Referenced by jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), and cbmc_parse_optionst::get_goto_program().
#define CPROVER_EXIT_INTERNAL_ERROR 6 |
An error has been encountered during processing the requested analysis.
Definition at line 41 of file exit_codes.h.
Referenced by bmct::do_language_agnostic_bmc(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), jdiff_parse_optionst::get_goto_program(), goto_diff_parse_optionst::get_goto_program(), cbmc_parse_optionst::get_goto_program(), janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY 6 |
Memory allocation has failed and this has been detected within the program.
Definition at line 48 of file exit_codes.h.
Referenced by janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), cbmc_parse_optionst::get_goto_program(), cbmc_parse_optionst::preprocessing(), jdiff_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().
#define CPROVER_EXIT_PARSE_ERROR 2 |
An error during parsing of the input program.
Definition at line 32 of file exit_codes.h.
#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED 8 |
Failure of the test-preprocessor method.
Definition at line 55 of file exit_codes.h.
Referenced by cbmc_parse_optionst::doit().
#define CPROVER_EXIT_SET_PROPERTIES_FAILED 7 |
Failure to identify the properties to verify.
Definition at line 51 of file exit_codes.h.
Referenced by cbmc_parse_optionst::doit(), janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
#define CPROVER_EXIT_SUCCESS 0 |
Success indicates the required analysis has been performed without error.
Definition at line 16 of file exit_codes.h.
Referenced by jdiff_parse_optionst::doit(), goto_diff_parse_optionst::doit(), cbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), janalyzer_parse_optionst::doit(), goto_analyzer_parse_optionst::doit(), cbmc_parse_optionst::get_command_line_options(), jbmc_parse_optionst::get_command_line_options(), cbmc_parse_optionst::get_goto_program(), jbmc_parse_optionst::get_goto_program(), janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
#define CPROVER_EXIT_USAGE_ERROR 1 |
A usage error is returned when the command line is invalid or conflicting.
Definition at line 28 of file exit_codes.h.
Referenced by cbmc_parse_optionst::doit(), goto_instrument_parse_optionst::doit(), cbmc_parse_optionst::get_command_line_options(), jbmc_parse_optionst::get_command_line_options(), janalyzer_parse_optionst::get_command_line_options(), goto_analyzer_parse_optionst::get_command_line_options(), janalyzer_parse_optionst::perform_analysis(), goto_analyzer_parse_optionst::perform_analysis(), and path_strategy_choosert::set_path_strategy_options().
#define CPROVER_EXIT_VERIFICATION_SAFE 0 |
Verification successful indiciates the analysis has been performed without error AND the software is safe (w.r.t.
the current analysis / config / spec)
Definition at line 21 of file exit_codes.h.
Referenced by bmct::do_language_agnostic_bmc(), janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().
#define CPROVER_EXIT_VERIFICATION_UNSAFE 10 |
Verification successful indiciates the analysis has been performed without error AND the software is not safe (w.r.t.
current analysis / config / spec)
Definition at line 25 of file exit_codes.h.
Referenced by bmct::do_language_agnostic_bmc(), janalyzer_parse_optionst::perform_analysis(), and goto_analyzer_parse_optionst::perform_analysis().