The CPROVER API Reference

The following sections summarize the functions available to programs that are passed to the CPROVER tools.

Functions

__CPROVER_assume, __CPROVER_assert, assert


void __CPROVER_assume(_Bool assumption);

void __CPROVER_assert(_Bool assertion, const char *description);

void assert(_Bool assertion);

The function __CPROVER_assume adds an expression as a constraint to the program. If the expression evaluates to false, the execution aborts without failure. More detail on the use of assumptions is in the section on Assumptions and Assertions.

__CPROVER_same_object, __CPROVER_POINTER_OBJECT, __CPROVER_POINTER_OFFSET, __CPROVER_DYNAMIC_OBJECT


_Bool __CPROVER_same_object(const void *, const void *);

unsigned __CPROVER_POINTER_OBJECT(const void *p);

signed __CPROVER_POINTER_OFFSET(const void *p);

_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);

The function __CPROVER_same_object returns true if the two pointers given as arguments point to the same object. The function __CPROVER_POINTER_OFFSET returns the offset of the given pointer relative to the base address of the object. The function __CPROVER_DYNAMIC_OBJECT returns true if the pointer passed as arguments points to a dynamically allocated object.

__CPROVER_is_zero_string, __CPROVER_zero_string_length, __CPROVER_buffer_size


_Bool __CPROVER_is_zero_string(const void *);

__CPROVER_size_t __CPROVER_zero_string_length(const void *);

__CPROVER_size_t __CPROVER_buffer_size(const void *);

__CPROVER_initialize


void __CPROVER_initialize(void);

The function __CPROVER_initialize computes the initial state of the program. It is called prior to calling the main procedure of the program.

__CPROVER_input, __CPROVER_output


void __CPROVER_input(const char *id, ...);

void __CPROVER_output(const char *id, ...);

The functions __CPROVER_input and __CPROVER_output are used to report an input or output value. Note that they do not generate input or output values. The first argument is a string constant to distinguish multiple inputs and outputs (inputs are typically generated using nondeterminism, as described here). The string constant is followed by an arbitrary number of values of arbitrary types.

__CPROVER_cover


void __CPROVER_cover(_Bool condition);

__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isfinite, __CPROVER_isfinite, __CPROVER_sign


_Bool __CPROVER_isnan(double f);

_Bool __CPROVER_isfinite(double f);

_Bool __CPROVER_isinf(double f);

_Bool __CPROVER_isnormal(double f);

_Bool __CPROVER_sign(double f);

The function __CPROVER_isnan returns true if the double-precision floating-point number passed as argument is a NaN.

The function __CPROVER_isfinite returns true if the double-precision floating-point number passed as argument is a finite number.

This function __CPROVER_isinf returns true if the double-precision floating-point number passed as argument is plus or minus infinity.

The function __CPROVER_isnormal returns true if the double-precision floating-point number passed as argument is a normal number.

This function __CPROVER_sign returns true if the double-precision floating-point number passed as argument is negative.

__CPROVER_abs, __CPROVER_labs, __CPROVER_fabs, __CPROVER_fabsl, __CPROVER_fabsf


int __CPROVER_abs(int x);

long int __CPROVER_labs(long int x);

double __CPROVER_fabs(double x);

long double __CPROVER_fabsl(long double x);

float __CPROVER_fabsf(float x);

These functions return the absolute value of the given argument.

__CPROVER_array_equal, __CPROVER_array_copy, __CPROVER_array_copy


_Bool __CPROVER_array_equal(const void array1[], const void array2[]);

void __CPROVER_array_copy(const void dest[], const void src[]);

void __CPROVER_array_set(const void dest[], value);

The function __CPROVER_array_equal returns true if the values stored in the given arrays are equal. The function __CPROVER_array_copy copies the contents of the array src to the array dest. The function __CPROVER_array_set initializes the array dest with the given value.

Predefined Types and Symbols

__CPROVER_bitvector


__CPROVER_bitvector [ expression ]

This type is only available in the C frontend. It is used to specify a bit vector with arbitrary but fixed size. The usual integer type modifiers signed and unsigned can be applied. The usual arithmetic promotions will be applied to operands of this type.

__CPROVER_floatbv


__CPROVER_floatbv [ expression ] [ expression ]

This type is only available in the C frontend. It is used to specify an IEEE-754 floating point number with arbitrary but fixed size. The first parameter is the total size (in bits) of the number, and the second is the size (in bits) of the mantissa, or significand (not including the hidden bit, thus for single precision this should be 23).

__CPROVER_fixedbv


__CPROVER_fixedbv [ expression ] [ expression ]

This type is only available in the C frontend. It is used to specify a fixed-point bit vector with arbitrary but fixed size. The first parameter is the total size (in bits) of the type, and the second is the number of bits after the radix point.

__CPROVER_size_t

The type of sizeof expressions.

__CPROVER_rounding_mode


extern int __CPROVER_rounding_mode;

This variable contains the IEEE floating-point arithmetic rounding mode.

__CPROVER_constant_infinity_uint

This is a constant that models a large unsigned integer.

__CPROVER_integer, __CPROVER_rational

__CPROVER_integer is an unbounded, signed integer type. __CPROVER_rational is an unbounded, signed rational number type.

__CPROVER_memory


extern unsigned char __CPROVER_memory[];

This array models the contents of integer-addressed memory.