CBMC
exit_codes.h File Reference

Document and give macros for the exit codes of CPROVER binaries. More...

+ This graph shows which files directly or indirectly include this file:

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 indicates the analysis has been performed without error AND the software is safe (w.r.t. More...
 
#define CPROVER_EXIT_VERIFICATION_UNSAFE   10
 Verification successful indicates the analysis has been performed without error AND the software is not safe (w.r.t. More...
 
#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE   5
 Verification inconclusive indicates the analysis has been performed without error AND the software is neither safe nor unsafe (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_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...
 

Detailed Description

Document and give macros for the exit codes of CPROVER binaries.

Definition in file exit_codes.h.

Macro Definition Documentation

◆ CPROVER_EXIT_CONVERSION_FAILED

#define CPROVER_EXIT_CONVERSION_FAILED   10

Failure to convert / write to another format.

Definition at line 62 of file exit_codes.h.

◆ CPROVER_EXIT_EXCEPTION

#define CPROVER_EXIT_EXCEPTION   6

An (unanticipated) exception was thrown during computation.

Definition at line 41 of file exit_codes.h.

◆ CPROVER_EXIT_INCORRECT_TASK

#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 49 of file exit_codes.h.

◆ CPROVER_EXIT_INTERNAL_ERROR

#define CPROVER_EXIT_INTERNAL_ERROR   6

An error has been encountered during processing the requested analysis.

Definition at line 45 of file exit_codes.h.

◆ CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY

#define CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY   6

Memory allocation has failed and this has been detected within the program.

Definition at line 52 of file exit_codes.h.

◆ CPROVER_EXIT_PARSE_ERROR

#define CPROVER_EXIT_PARSE_ERROR   2

An error during parsing of the input program.

Definition at line 37 of file exit_codes.h.

◆ CPROVER_EXIT_PREPROCESSOR_TEST_FAILED

#define CPROVER_EXIT_PREPROCESSOR_TEST_FAILED   8

Failure of the test-preprocessor method.

Definition at line 59 of file exit_codes.h.

◆ CPROVER_EXIT_SET_PROPERTIES_FAILED

#define CPROVER_EXIT_SET_PROPERTIES_FAILED   7

Failure to identify the properties to verify.

Definition at line 55 of file exit_codes.h.

◆ CPROVER_EXIT_SUCCESS

#define CPROVER_EXIT_SUCCESS   0

Success indicates the required analysis has been performed without error.

Definition at line 16 of file exit_codes.h.

◆ CPROVER_EXIT_USAGE_ERROR

#define CPROVER_EXIT_USAGE_ERROR   1

A usage error is returned when the command line is invalid or conflicting.

Definition at line 33 of file exit_codes.h.

◆ CPROVER_EXIT_VERIFICATION_INCONCLUSIVE

#define CPROVER_EXIT_VERIFICATION_INCONCLUSIVE   5

Verification inconclusive indicates the analysis has been performed without error AND the software is neither safe nor unsafe (w.r.t.

current analysis / config / spec)

Definition at line 30 of file exit_codes.h.

◆ CPROVER_EXIT_VERIFICATION_SAFE

#define CPROVER_EXIT_VERIFICATION_SAFE   0

Verification successful indicates 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.

◆ CPROVER_EXIT_VERIFICATION_UNSAFE

#define CPROVER_EXIT_VERIFICATION_UNSAFE   10

Verification successful indicates 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.