cprover
cprover.h File Reference

Go to the source code of this file.

Classes

struct  __CPROVER_pipet
 

Macros

#define __CPROVER_danger_number_of_ops   1
 
#define __CPROVER_danger_max_solution_size   1
 
#define __CPROVER_danger_number_of_vars   1
 
#define __CPROVER_danger_number_of_consts   1
 

Functions

typedef __typeof__ (sizeof(int)) __CPROVER_size_t
 
void * __CPROVER_allocate (__CPROVER_size_t size, __CPROVER_bool zero)
 
void __CPROVER_assume (__CPROVER_bool assumption) __attribute__((__noreturn__))
 
void __CPROVER_assert (__CPROVER_bool assertion, const char *description)
 
void __CPROVER_precondition (__CPROVER_bool assertion, const char *description)
 
void __CPROVER_postcondition (__CPROVER_bool assertion, const char *description)
 
__CPROVER_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_bool __CPROVER_r_ok (const void *, __CPROVER_size_t)
 
__CPROVER_bool __CPROVER_w_ok (const void *, __CPROVER_size_t)
 
void __CPROVER_printf (const char *format,...)
 
void __CPROVER_input (const char *id,...)
 
void __CPROVER_output (const char *id,...)
 
void __CPROVER_atomic_begin ()
 
void __CPROVER_atomic_end ()
 
void __CPROVER_fence (const char *kind,...)
 
unsigned __CPROVER_POINTER_OBJECT (const void *p)
 
signed __CPROVER_POINTER_OFFSET (const void *p)
 
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT (const void *p)
 
int __CPROVER_fpclassify (int, int, int, int, int,...)
 
__CPROVER_bool __CPROVER_isfinite (double f)
 
__CPROVER_bool __CPROVER_isinf (double f)
 
__CPROVER_bool __CPROVER_isnormal (double f)
 
__CPROVER_bool __CPROVER_sign (double f)
 
__CPROVER_bool __CPROVER_isnanf (float f)
 
__CPROVER_bool __CPROVER_isnand (double f)
 
__CPROVER_bool __CPROVER_isnanld (long double f)
 
__CPROVER_bool __CPROVER_isfinitef (float f)
 
__CPROVER_bool __CPROVER_isfinited (double f)
 
__CPROVER_bool __CPROVER_isfiniteld (long double f)
 
__CPROVER_bool __CPROVER_isinff (float f)
 
__CPROVER_bool __CPROVER_isinfd (double f)
 
__CPROVER_bool __CPROVER_isinfld (long double f)
 
__CPROVER_bool __CPROVER_isnormalf (float f)
 
__CPROVER_bool __CPROVER_isnormald (double f)
 
__CPROVER_bool __CPROVER_isnormalld (long double f)
 
__CPROVER_bool __CPROVER_signf (float f)
 
__CPROVER_bool __CPROVER_signd (double f)
 
__CPROVER_bool __CPROVER_signld (long double f)
 
double __CPROVER_inf (void)
 
float __CPROVER_inff (void)
 
long double __CPROVER_infl (void)
 
int __CPROVER_isgreaterd (double f, double g)
 
int __CPROVER_abs (int)
 
long int __CPROVER_labs (long int)
 
long long int __CPROVER_llabs (long long int)
 
double __CPROVER_fabs (double)
 
long double __CPROVER_fabsl (long double)
 
float __CPROVER_fabsf (float)
 
void __CPROVER_array_copy (const void *dest, const void *src)
 
void __CPROVER_array_set (const void *dest,...)
 
void __CPROVER_array_replace (const void *dest, const void *src)
 
void __CPROVER_set_must (const void *, const char *)
 
void __CPROVER_set_may (const void *, const char *)
 
void __CPROVER_clear_must (const void *, const char *)
 
void __CPROVER_clear_may (const void *, const char *)
 
void __CPROVER_cleanup (const void *, void(*)(void *))
 
__CPROVER_bool __CPROVER_get_must (const void *, const char *)
 
__CPROVER_bool __CPROVER_get_may (const void *, const char *)
 
__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 ()
 

Variables

const void * __CPROVER_deallocated
 
const void * __CPROVER_malloc_object
 
__CPROVER_size_t __CPROVER_malloc_size
 
_Bool __CPROVER_malloc_is_new_array
 
const void * __CPROVER_memory_leak
 
int __CPROVER_malloc_failure_mode
 
__CPROVER_size_t __CPROVER_max_malloc_size
 
_Bool __CPROVER_malloc_may_fail
 
int __CPROVER_malloc_failure_mode_return_null
 
int __CPROVER_malloc_failure_mode_assert_then_assume
 

Macro Definition Documentation

◆ __CPROVER_danger_max_solution_size

#define __CPROVER_danger_max_solution_size   1

Definition at line 159 of file cprover.h.

◆ __CPROVER_danger_number_of_consts

#define __CPROVER_danger_number_of_consts   1

Definition at line 161 of file cprover.h.

◆ __CPROVER_danger_number_of_ops

#define __CPROVER_danger_number_of_ops   1

Definition at line 158 of file cprover.h.

◆ __CPROVER_danger_number_of_vars

#define __CPROVER_danger_number_of_vars   1

Definition at line 160 of file cprover.h.

Function Documentation

◆ __CPROVER_abs()

int __CPROVER_abs ( int  )

◆ __CPROVER_allocate()

void* __CPROVER_allocate ( __CPROVER_size_t  size,
__CPROVER_bool  zero 
)

◆ __CPROVER_array_copy()

void __CPROVER_array_copy ( const void *  dest,
const void *  src 
)

◆ __CPROVER_array_replace()

void __CPROVER_array_replace ( const void *  dest,
const void *  src 
)

◆ __CPROVER_array_set()

void __CPROVER_array_set ( const void *  dest,
  ... 
)

◆ __CPROVER_assert()

void __CPROVER_assert ( __CPROVER_bool  assertion,
const char *  description 
)

◆ __CPROVER_assume()

void __CPROVER_assume ( __CPROVER_bool  assumption)

◆ __CPROVER_atomic_begin()

void __CPROVER_atomic_begin ( )

◆ __CPROVER_atomic_end()

void __CPROVER_atomic_end ( )

◆ __CPROVER_buffer_size()

__CPROVER_size_t __CPROVER_buffer_size ( const void *  )

◆ __CPROVER_cleanup()

void __CPROVER_cleanup ( const void *  ,
void(*)(void *)   
)

◆ __CPROVER_clear_may()

void __CPROVER_clear_may ( const void *  ,
const char *   
)

◆ __CPROVER_clear_must()

void __CPROVER_clear_must ( const void *  ,
const char *   
)

◆ __CPROVER_DYNAMIC_OBJECT()

__CPROVER_bool __CPROVER_DYNAMIC_OBJECT ( const void *  p)

◆ __CPROVER_fabs()

double __CPROVER_fabs ( double  )

◆ __CPROVER_fabsf()

float __CPROVER_fabsf ( float  )

◆ __CPROVER_fabsl()

long double __CPROVER_fabsl ( long double  )

◆ __CPROVER_fence()

void __CPROVER_fence ( const char *  kind,
  ... 
)

◆ __CPROVER_fpclassify()

int __CPROVER_fpclassify ( int  ,
int  ,
int  ,
int  ,
int  ,
  ... 
)

◆ __CPROVER_get_may()

__CPROVER_bool __CPROVER_get_may ( const void *  ,
const char *   
)

◆ __CPROVER_get_must()

__CPROVER_bool __CPROVER_get_must ( const void *  ,
const char *   
)

◆ __CPROVER_inf()

double __CPROVER_inf ( void  )

◆ __CPROVER_inff()

float __CPROVER_inff ( void  )

◆ __CPROVER_infl()

long double __CPROVER_infl ( void  )

◆ __CPROVER_input()

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

◆ __CPROVER_is_zero_string()

__CPROVER_bool __CPROVER_is_zero_string ( const void *  )

◆ __CPROVER_isfinite()

__CPROVER_bool __CPROVER_isfinite ( double  f)

◆ __CPROVER_isfinited()

__CPROVER_bool __CPROVER_isfinited ( double  f)

◆ __CPROVER_isfinitef()

__CPROVER_bool __CPROVER_isfinitef ( float  f)

◆ __CPROVER_isfiniteld()

__CPROVER_bool __CPROVER_isfiniteld ( long double  f)

◆ __CPROVER_isgreaterd()

int __CPROVER_isgreaterd ( double  f,
double  g 
)

◆ __CPROVER_isinf()

__CPROVER_bool __CPROVER_isinf ( double  f)

◆ __CPROVER_isinfd()

__CPROVER_bool __CPROVER_isinfd ( double  f)

◆ __CPROVER_isinff()

__CPROVER_bool __CPROVER_isinff ( float  f)

◆ __CPROVER_isinfld()

__CPROVER_bool __CPROVER_isinfld ( long double  f)

◆ __CPROVER_isnand()

__CPROVER_bool __CPROVER_isnand ( double  f)

◆ __CPROVER_isnanf()

__CPROVER_bool __CPROVER_isnanf ( float  f)

◆ __CPROVER_isnanld()

__CPROVER_bool __CPROVER_isnanld ( long double  f)

◆ __CPROVER_isnormal()

__CPROVER_bool __CPROVER_isnormal ( double  f)

◆ __CPROVER_isnormald()

__CPROVER_bool __CPROVER_isnormald ( double  f)

◆ __CPROVER_isnormalf()

__CPROVER_bool __CPROVER_isnormalf ( float  f)

◆ __CPROVER_isnormalld()

__CPROVER_bool __CPROVER_isnormalld ( long double  f)

◆ __CPROVER_labs()

long int __CPROVER_labs ( long int  )

◆ __CPROVER_llabs()

long long int __CPROVER_llabs ( long long int  )

◆ __CPROVER_output()

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

◆ __CPROVER_overflow_minus()

__CPROVER_bool __CPROVER_overflow_minus ( )

◆ __CPROVER_overflow_mult()

__CPROVER_bool __CPROVER_overflow_mult ( )

◆ __CPROVER_overflow_plus()

__CPROVER_bool __CPROVER_overflow_plus ( )

◆ __CPROVER_overflow_shl()

__CPROVER_bool __CPROVER_overflow_shl ( )

◆ __CPROVER_overflow_unary_minus()

__CPROVER_bool __CPROVER_overflow_unary_minus ( )

◆ __CPROVER_POINTER_OBJECT()

unsigned __CPROVER_POINTER_OBJECT ( const void *  p)

◆ __CPROVER_POINTER_OFFSET()

signed __CPROVER_POINTER_OFFSET ( const void *  p)

◆ __CPROVER_postcondition()

void __CPROVER_postcondition ( __CPROVER_bool  assertion,
const char *  description 
)

◆ __CPROVER_precondition()

void __CPROVER_precondition ( __CPROVER_bool  assertion,
const char *  description 
)

◆ __CPROVER_printf()

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

◆ __CPROVER_r_ok()

__CPROVER_bool __CPROVER_r_ok ( const void *  ,
__CPROVER_size_t   
)

◆ __CPROVER_set_may()

void __CPROVER_set_may ( const void *  ,
const char *   
)

◆ __CPROVER_set_must()

void __CPROVER_set_must ( const void *  ,
const char *   
)

◆ __CPROVER_sign()

__CPROVER_bool __CPROVER_sign ( double  f)

◆ __CPROVER_signd()

__CPROVER_bool __CPROVER_signd ( double  f)

◆ __CPROVER_signf()

__CPROVER_bool __CPROVER_signf ( float  f)

◆ __CPROVER_signld()

__CPROVER_bool __CPROVER_signld ( long double  f)

◆ __CPROVER_w_ok()

__CPROVER_bool __CPROVER_w_ok ( const void *  ,
__CPROVER_size_t   
)

◆ __CPROVER_zero_string_length()

__CPROVER_size_t __CPROVER_zero_string_length ( const void *  )

◆ __typeof__()

typedef __typeof__ ( sizeof(int)  )

Variable Documentation

◆ __CPROVER_deallocated

const void* __CPROVER_deallocated
extern

◆ __CPROVER_malloc_failure_mode

int __CPROVER_malloc_failure_mode
extern

◆ __CPROVER_malloc_failure_mode_assert_then_assume

int __CPROVER_malloc_failure_mode_assert_then_assume
extern

◆ __CPROVER_malloc_failure_mode_return_null

int __CPROVER_malloc_failure_mode_return_null
extern

◆ __CPROVER_malloc_is_new_array

_Bool __CPROVER_malloc_is_new_array
extern

◆ __CPROVER_malloc_may_fail

_Bool __CPROVER_malloc_may_fail
extern

◆ __CPROVER_malloc_object

const void* __CPROVER_malloc_object
extern

◆ __CPROVER_malloc_size

__CPROVER_size_t __CPROVER_malloc_size
extern

◆ __CPROVER_max_malloc_size

__CPROVER_size_t __CPROVER_max_malloc_size
extern

◆ __CPROVER_memory_leak

const void* __CPROVER_memory_leak
extern