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.

__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_printf

void __CPROVER_printf(const char *format, ...);

The function **__CPROVER_printf** implements the C printf function (without any return value). The observable effect is that its output is shown within a counterexample trace.

__CPROVER_cover

void __CPROVER_cover(_Bool condition);

This statement defines a custom coverage criterion, for usage with the test suite generation feature.

__CPROVER_isnan, __CPROVER_isfinite, __CPROVER_isinf, __CPROVER_isnormal, __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_overflow_minus, __CPROVER_overflow_mult, __CPROVER_overflow_plus, __CPROVER_overflow_shl, __CPROVER_overflow_unary_minus

__CPROVER_bool __CPROVER_overflow_minus();
__CPROVER_bool __CPROVER_overflow_mult();
__CPROVER_bool __CPROVER_overflow_plus();
__CPROVER_bool __CPROVER_overflow_shl();
__CPROVER_bool __CPROVER_overflow_unary_minus();

These functions take two (__CPROVER_overflow_unary_minus only takes one) arguments of any numeric type. They return true, if, and only if, the named operation would overflow when applied to the arguments. For example, __CPROVER_overflow_plus(x, y) returns true if x + y would result in an arithmetic overflow.

__CPROVER_array_equal, __CPROVER_array_copy, __CPROVER_array_set

_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.

__CPROVER_enum_is_in_range

__CPROVER_bool __CPROVER_enum_is_in_range();

The function **__CPROVER_enum_is_in_range** is used to check that an enumeration has one of the defined enumeration values. In the following example __CPROVER_enum_is_in_range(ev1) will return true and the assertion will pass

enum my_enum { first, second };
 
int main()
{
  enum my_enum ev1 = second;
  assert(__CPROVER_enum_is_in_range(ev1));
}

However, in the example below the assertion will fail

enum my_enum { first, second };
 
int main()
{
  enum my_enum ev1 = second + 1;
  assert(__CPROVER_enum_is_in_range(ev1));
}

Uninterpreted Functions

Uninterpreted functions are documented here.

Memory-Related Functions

The semantics of the primitives listed in this section is described in more detail in the document about Memory Primitives.

__CPROVER_POINTER_OBJECT, __CPROVER_POINTER_OFFSET, __CPROVER_same_object

__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *p);
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *p);
_Bool __CPROVER_same_object(const void *p, const void *q);

The function **__CPROVER_POINTER_OBJECT** returns the ID of the object the pointer points to. The function **__CPROVER_POINTER_OFFSET** returns the offset of the given pointer relative to the base address of the object. The function **__CPROVER_same_object** returns true if the two pointers given as arguments point to the same object.

__CPROVER_OBJECT_SIZE, __CPROVER_DYNAMIC_OBJECT, __CPROVER_r_ok, __CPROVER_w_ok

The following primitives require a pointer that is null or valid in order to have well-defined semantics in all usage cases. See the document about Memory Primitives for more details. It also includes a description of the --pointer-primitive-check option to verify the preconditions of the primitives.

__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p);
_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
void __CPROVER_r_ok(const T *p);
void __CPROVER_r_ok(const void *p, size_t size);
void __CPROVER_w_ok(const T *p);
void __CPROVER_w_ok(const void *p, size_t size);
void __CPROVER_rw_ok(const T *p);
void __CPROVER_rw_ok(const void *p, size_t size);

The function **__CPROVER__OBJECT_SIZE** returns the size of the object the given pointer points to. The function **__CPROVER_DYNAMIC_OBJECT** returns true if the pointer passed as an argument points to a dynamically allocated object.

The function **__CPROVER_r_ok** returns true if reading the piece of memory starting at the given pointer with the given size is safe. **__CPROVER_w_ok** does the same with writing, and **__CPROVER_rw_ok** returns true when it is safe to do both. These predicates can be given an optional size; when the size argument is not given, the size of the subtype (which must not be void) of the pointer type is used.

__CPROVER_havoc_object

This function requires a valid pointer and updates all bytes of the underlying object with nondeterministic values.

void __CPROVER_havoc_object(void *p);

Warning

This primitive havocs object bytes before the given p and after p + sizeof(*p):

struct foo {
  int x;
  int y;
  int z;
};
 
struct foo thefoo = {.x = 1; .y = 2, .z = 3};
 
int* p = &thefoo.y; // pointing to thefoo.y
 
__CPROVER_havoc_object(p); // makes the whole struct nondet
__CPROVER_assert(thefoo.x == 1, "fails because `thefoo.x` is now nondet");
__CPROVER_assert(thefoo.y == 2, "fails because `thefoo.y` is now nondet");
__CPROVER_assert(thefoo.z == 3, "fails because `thefoo.z` is now nondet");

__CPROVER_havoc_slice

This function requires requires that __CPROVER_w_ok(p, size) holds, and updates size consecutive bytes of the underlying object, starting at p, with nondeterministic values.

void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);

Caveat

If the slice contains bytes that can be interpreted as pointers by the program, this will cause these pointers to become invalid (i.e. they will not point to anything meaningful).
If this slice only contains bytes that are not interpreted as pointers by the program, then havocing the slice is equivalent to making the interpretation of these bytes nondeterministic.

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.

__CPROVER::unsignedbv<N> (C++ only)

This type is the equivalent of unsigned __CPROVER_bitvector[N] in the C++ front-end.

__CPROVER::signedbv<N> (C++ only)

This type is the equivalent of signed __CPROVER_bitvector[N] in the C++ front-end.

__CPROVER::fixedbv<N> (C++ only)

This type is the equivalent of **__CPROVER_fixedbv[N,m]** in the C++ front-end.

Concurrency

Asynchronous threads are created by preceding an instruction with a label with the prefix **__CPROVER_ASYNC_**.

Last modified: 2024-11-20 06:00:32 -0800