Go to the documentation of this file.
9 #ifndef CPROVER_ANSI_C_LIBRARY_CPROVER_H
10 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
44 const unsigned __CPROVER_constant_infinity_uint;
45 typedef void __CPROVER_integer;
46 typedef void __CPROVER_rational;
47 void __CPROVER_initialize(
void);
60 __CPROVER_thread_local
unsigned long __CPROVER_thread_id=0;
61 __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
62 unsigned long __CPROVER_next_thread_id=0;
65 void CBMC_trace(
int lvl,
const char *event, ...);
73 extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];
75 __CPROVER_size_t address, __CPROVER_size_t extent);
78 extern __CPROVER_thread_local
const char __func__[__CPROVER_constant_infinity_uint];
81 extern __CPROVER_thread_local
const char __FUNCTION__[__CPROVER_constant_infinity_uint];
82 extern __CPROVER_thread_local
const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];
137 unsigned step,
unsigned loop_free);
140 void __CPROVER_predicate(__CPROVER_bool predicate);
141 void __CPROVER_parameter_predicates();
142 void __CPROVER_return_predicates();
153 extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
155 extern const int __CPROVER_pipe_offset;
156 extern unsigned __CPROVER_pipe_count;
167 #define __CPROVER_danger_number_of_ops 1
168 #define __CPROVER_danger_max_solution_size 1
169 #define __CPROVER_danger_number_of_vars 1
170 #define __CPROVER_danger_number_of_consts 1
179 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_isnanld(long double f)
__CPROVER_bool __CPROVER_signld(long double f)
__CPROVER_bool __CPROVER_isinfd(double f)
typedef __typeof__(sizeof(int)) __CPROVER_size_t
_Bool __CPROVER_is_zero_string(const void *)
float __CPROVER_fmodf(float, float)
void __CPROVER_atomic_end()
__CPROVER_bool __CPROVER_isinff(float f)
__CPROVER_bool __CPROVER_overflow_mult()
int __CPROVER_fpclassify(int, int, int, int, int,...)
const void * __CPROVER_malloc_object
__CPROVER_bool __CPROVER_signf(float f)
__CPROVER_bool __CPROVER_overflow_plus()
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
long long int __CPROVER_llabs(long long int)
__CPROVER_bool __CPROVER_isfinitef(float f)
long double __CPROVER_fmodl(long double, long double)
__CPROVER_bool __CPROVER_overflow_shl()
const void * __CPROVER_deallocated
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__))
long double __CPROVER_infl(void)
_Bool __CPROVER_malloc_may_fail
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
const void * __CPROVER_memory_leak
void __CPROVER_output(const char *id,...)
void __CPROVER_array_copy(const void *dest, const void *src)
__CPROVER_bool __CPROVER_isnand(double f)
__CPROVER_size_t __CPROVER_malloc_size
void __CPROVER_atomic_begin()
__CPROVER_size_t __CPROVER_buffer_size(const void *)
long double __CPROVER_remainderl(long double, long double)
__CPROVER_bool __CPROVER_sign(double f)
__CPROVER_bool __CPROVER_isinfld(long double f)
_Bool __CPROVER_malloc_is_new_array
void __CPROVER_cleanup(const void *, void(*)(void *))
__CPROVER_bool __CPROVER_overflow_unary_minus()
long int __CPROVER_labs(long int)
float __CPROVER_inff(void)
int __CPROVER_malloc_failure_mode
__CPROVER_bool __CPROVER_isfinite(double f)
__CPROVER_bool __CPROVER_w_ok()
void __CPROVER_fence(const char *kind,...)
void __CPROVER_printf(const char *format,...)
double __CPROVER_fmod(double, double)
void __CPROVER_set_may(const void *, const char *)
void __CPROVER_array_replace(const void *dest, const void *src)
void __CPROVER_set_must(const void *, const char *)
__CPROVER_bool __CPROVER_overflow_minus()
__CPROVER_bool __CPROVER_isfinited(double f)
signed __CPROVER_POINTER_OFFSET(const void *p)
int __CPROVER_isgreaterd(double f, double g)
void __CPROVER_clear_may(const void *, const char *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_precondition(__CPROVER_bool assertion, const char *description)
__CPROVER_bool __CPROVER_isinf(double f)
long double __CPROVER_fabsl(long double)
unsigned __CPROVER_POINTER_OBJECT(const void *p)
void __CPROVER_input(const char *id,...)
__CPROVER_size_t __CPROVER_max_malloc_size
float __CPROVER_fabsf(float)
float __CPROVER_remainderf(float, float)
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
__CPROVER_bool __CPROVER_isnanf(float f)
__CPROVER_bool __CPROVER_isfiniteld(long double f)
double __CPROVER_inf(void)
__CPROVER_bool __CPROVER_isnormalf(float f)
double __CPROVER_fabs(double)
__CPROVER_bool __CPROVER_isnormald(double f)
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
int __CPROVER_malloc_failure_mode_return_null
double __CPROVER_remainder(double, double)
__CPROVER_bool __CPROVER_isnormalld(long double f)
void __CPROVER_clear_must(const void *, const char *)
__CPROVER_bool __CPROVER_rw_ok()
void __CPROVER_array_set(const void *dest,...)
__CPROVER_bool __CPROVER_isnormal(double f)
__CPROVER_bool __CPROVER_r_ok()
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p)
__CPROVER_bool __CPROVER_signd(double f)