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

This graph shows which files directly or indirectly include 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.