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