cprover
cprover_builtin_headers.h File Reference

Go to the source code of this file.

Functions

void __CPROVER_assume (__CPROVER_bool assumption)
 
void __VERIFIER_assume (__CPROVER_bool assumption)
 
void __CPROVER_assert (__CPROVER_bool assertion, const char *description)
 
void __CPROVER_precondition (__CPROVER_bool precondition, const char *description)
 
void __CPROVER_postcondition (__CPROVER_bool assertion, const char *description)
 
void __CPROVER_havoc_object (void *)
 
__CPROVER_bool __CPROVER_equal ()
 
__CPROVER_bool __CPROVER_same_object (const void *, const void *)
 
__CPROVER_bool __CPROVER_is_invalid_pointer (const void *)
 
__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)
 
__CPROVER_bool __CPROVER_get_flag (const void *, const char *)
 
void __CPROVER_set_must (const void *, const char *)
 
void __CPROVER_clear_must (const void *, const char *)
 
void __CPROVER_set_may (const void *, const char *)
 
void __CPROVER_clear_may (const void *, const char *)
 
void __CPROVER_cleanup (const void *, const void *)
 
__CPROVER_bool __CPROVER_get_must (const void *, const char *)
 
__CPROVER_bool __CPROVER_get_may (const void *, const char *)
 
void __CPROVER_printf (const char *format,...)
 
void __CPROVER_input (const char *id,...)
 
void __CPROVER_output (const char *id,...)
 
void __CPROVER_cover (__CPROVER_bool condition)
 
void __CPROVER_atomic_begin ()
 
void __CPROVER_atomic_end ()
 
void __CPROVER_fence (const char *kind,...)
 
__CPROVER_size_t __CPROVER_POINTER_OBJECT (const void *)
 
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET (const void *)
 
__CPROVER_size_t __CPROVER_OBJECT_SIZE (const void *)
 
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT (const void *)
 
void __CPROVER_allocated_memory (__CPROVER_size_t address, __CPROVER_size_t extent)
 
int __CPROVER_fpclassify (int, int, int, int, int,...)
 
__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_isgreaterf (float f, float g)
 
int __CPROVER_isgreaterd (double f, double g)
 
int __CPROVER_isgreaterequalf (float f, float g)
 
int __CPROVER_isgreaterequald (double f, double g)
 
int __CPROVER_islessf (float f, float g)
 
int __CPROVER_islessd (double f, double g)
 
int __CPROVER_islessequalf (float f, float g)
 
int __CPROVER_islessequald (double f, double g)
 
int __CPROVER_islessgreaterf (float f, float g)
 
int __CPROVER_islessgreaterd (double f, double g)
 
int __CPROVER_isunorderedf (float f, float g)
 
int __CPROVER_isunorderedd (double f, double g)
 
int __CPROVER_abs (int x)
 
long int __CPROVER_labs (long int x)
 
long int __CPROVER_llabs (long long int x)
 
double __CPROVER_fabs (double x)
 
long double __CPROVER_fabsl (long double x)
 
float __CPROVER_fabsf (float x)
 
__CPROVER_bool __CPROVER_array_equal (const void *array1, const void *array2)
 
void __CPROVER_array_copy (const void *dest, const void *src)
 
void __CPROVER_array_replace (const void *dest, const void *src)
 
void __CPROVER_array_set (const void *dest,...)
 
void __CPROVER_k_induction_hint (unsigned min, unsigned max, unsigned step, unsigned loop_free)
 
int __CPROVER_scanf (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 ()
 

Function Documentation

◆ __CPROVER_abs()

int __CPROVER_abs ( int  x)

◆ __CPROVER_allocated_memory()

void __CPROVER_allocated_memory ( __CPROVER_size_t  address,
__CPROVER_size_t  extent 
)

◆ __CPROVER_array_copy()

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

◆ __CPROVER_array_equal()

__CPROVER_bool __CPROVER_array_equal ( const void *  array1,
const void *  array2 
)

◆ __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 *  ,
const void *   
)

◆ __CPROVER_clear_may()

void __CPROVER_clear_may ( const void *  ,
const char *   
)

◆ __CPROVER_clear_must()

void __CPROVER_clear_must ( const void *  ,
const char *   
)

◆ __CPROVER_cover()

void __CPROVER_cover ( __CPROVER_bool  condition)

◆ __CPROVER_DYNAMIC_OBJECT()

__CPROVER_bool __CPROVER_DYNAMIC_OBJECT ( const void *  )

◆ __CPROVER_equal()

__CPROVER_bool __CPROVER_equal ( )

◆ __CPROVER_fabs()

double __CPROVER_fabs ( double  x)

◆ __CPROVER_fabsf()

float __CPROVER_fabsf ( float  x)

◆ __CPROVER_fabsl()

long double __CPROVER_fabsl ( long double  x)

◆ __CPROVER_fence()

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

◆ __CPROVER_fpclassify()

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

◆ __CPROVER_get_flag()

__CPROVER_bool __CPROVER_get_flag ( const void *  ,
const char *   
)

◆ __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_havoc_object()

void __CPROVER_havoc_object ( void *  )

◆ __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_invalid_pointer()

__CPROVER_bool __CPROVER_is_invalid_pointer ( const void *  )

◆ __CPROVER_is_zero_string()

__CPROVER_bool __CPROVER_is_zero_string ( const void *  )

◆ __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_isgreaterequald()

int __CPROVER_isgreaterequald ( double  f,
double  g 
)

◆ __CPROVER_isgreaterequalf()

int __CPROVER_isgreaterequalf ( float  f,
float  g 
)

◆ __CPROVER_isgreaterf()

int __CPROVER_isgreaterf ( float  f,
float  g 
)

◆ __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_islessd()

int __CPROVER_islessd ( double  f,
double  g 
)

◆ __CPROVER_islessequald()

int __CPROVER_islessequald ( double  f,
double  g 
)

◆ __CPROVER_islessequalf()

int __CPROVER_islessequalf ( float  f,
float  g 
)

◆ __CPROVER_islessf()

int __CPROVER_islessf ( float  f,
float  g 
)

◆ __CPROVER_islessgreaterd()

int __CPROVER_islessgreaterd ( double  f,
double  g 
)

◆ __CPROVER_islessgreaterf()

int __CPROVER_islessgreaterf ( float  f,
float  g 
)

◆ __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_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_isunorderedd()

int __CPROVER_isunorderedd ( double  f,
double  g 
)

◆ __CPROVER_isunorderedf()

int __CPROVER_isunorderedf ( float  f,
float  g 
)

◆ __CPROVER_k_induction_hint()

void __CPROVER_k_induction_hint ( unsigned  min,
unsigned  max,
unsigned  step,
unsigned  loop_free 
)

◆ __CPROVER_labs()

long int __CPROVER_labs ( long int  x)

◆ __CPROVER_llabs()

long int __CPROVER_llabs ( long long int  x)

◆ __CPROVER_OBJECT_SIZE()

__CPROVER_size_t __CPROVER_OBJECT_SIZE ( const void *  )

◆ __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()

__CPROVER_size_t __CPROVER_POINTER_OBJECT ( const void *  )

◆ __CPROVER_POINTER_OFFSET()

__CPROVER_ssize_t __CPROVER_POINTER_OFFSET ( const void *  )

◆ __CPROVER_postcondition()

void __CPROVER_postcondition ( __CPROVER_bool  assertion,
const char *  description 
)

◆ __CPROVER_precondition()

void __CPROVER_precondition ( __CPROVER_bool  precondition,
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_same_object()

__CPROVER_bool __CPROVER_same_object ( const void *  ,
const void *   
)

◆ __CPROVER_scanf()

int __CPROVER_scanf ( const char *  ,
  ... 
)

◆ __CPROVER_set_may()

void __CPROVER_set_may ( const void *  ,
const char *   
)

◆ __CPROVER_set_must()

void __CPROVER_set_must ( const void *  ,
const char *   
)

◆ __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 *  )

◆ __VERIFIER_assume()

void __VERIFIER_assume ( __CPROVER_bool  assumption)