|
| 1 | +/*******************************************************************\ |
| 2 | +
|
| 3 | +Module: Exit codes |
| 4 | +
|
| 5 | +Author: Martin Brain, [email protected] |
| 6 | +
|
| 7 | +\*******************************************************************/ |
| 8 | + |
| 9 | +#ifndef CPROVER_UTIL_EXIT_CODES_H |
| 10 | +#define CPROVER_UTIL_EXIT_CODES_H |
| 11 | + |
| 12 | +/// \file |
| 13 | +/// Document and give macros for the exit codes of CPROVER binaries. |
| 14 | + |
| 15 | +/// Success indicates the required analysis has been performed without error. |
| 16 | +#define CPROVER_EXIT_SUCCESS 0 |
| 17 | +// should contemplate EX_OK from sysexits.h |
| 18 | + |
| 19 | +/// Verification successful indiciates the analysis has been performed without |
| 20 | +/// error AND the software is safe (w.r.t. the current analysis / config / spec) |
| 21 | +#define CPROVER_EXIT_VERIFICATION_SAFE 0 |
| 22 | + |
| 23 | +/// Verification successful indiciates the analysis has been performed without |
| 24 | +/// error AND the software is not safe (w.r.t. current analysis / config / spec) |
| 25 | +#define CPROVER_EXIT_VERIFICATION_UNSAFE 10 |
| 26 | + |
| 27 | +/// A usage error is returned when the command line is invalid or conflicting. |
| 28 | +#define CPROVER_EXIT_USAGE_ERROR 1 |
| 29 | +// should contemplate EX_USAGE from sysexits.h |
| 30 | + |
| 31 | +/// An error during parsing of the input program |
| 32 | +#define CPROVER_EXIT_PARSE_ERROR 2 |
| 33 | +// This should be the same as YY_EXIT_FAILURE |
| 34 | + |
| 35 | +/// An (unanticipated) exception was thrown during computation. |
| 36 | +#define CPROVER_EXIT_EXCEPTION 6 |
| 37 | +// should contemplate EX_SOFTWARE from sysexits.h |
| 38 | +#define CPROVER_EXIT_EXCEPTION_GOTO_INSTRUMENT 11 |
| 39 | + |
| 40 | +/// An error has been encountered during processing the requested analysis. |
| 41 | +#define CPROVER_EXIT_INTERNAL_ERROR 6 |
| 42 | + |
| 43 | +/// The command line is correctly structured but cannot be carried out |
| 44 | +/// due to missing files, invalid file types, etc. |
| 45 | +#define CPROVER_EXIT_INCORRECT_TASK 6 |
| 46 | + |
| 47 | +/// Memory allocation has failed and this has been detected within the program. |
| 48 | +#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY 6 |
| 49 | + |
| 50 | +/// Failure to identify the properties to verify |
| 51 | +#define CPROVER_EXIT_SET_PROPERTIES_FAILED 7 |
| 52 | +// should contemplate EX_USAGE from sysexits.h |
| 53 | + |
| 54 | +/// Failure of the test-preprocessor method |
| 55 | +#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED 8 |
| 56 | + |
| 57 | +/// Failure to convert / write to another format |
| 58 | +#define CPROVER_EXIT_CONVERSION_FAILED 10 |
| 59 | + |
| 60 | +#endif // CPROVER_UTIL_EXIT_CODES_H |
0 commit comments