Go to the documentation of this file.
9 #ifndef CPROVER_CPP_LIBRARY_CPROVER_H
10 #define CPROVER_CPP_LIBRARY_CPROVER_H
53 #endif // CPROVER_CPP_LIBRARY_CPROVER_H
typedef __typeof__(sizeof(int)) __CPROVER_size_t
void __CPROVER_atomic_end()
const void * __CPROVER_malloc_object
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
const void * __CPROVER_deallocated
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__))
__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_size_t __CPROVER_malloc_size
void __CPROVER_atomic_begin()
_Bool __CPROVER_malloc_is_new_array
void __CPROVER_cleanup(const void *, void(*)(void *))
void __CPROVER_fence(const char *kind,...)
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 *)
signed __CPROVER_POINTER_OFFSET(const void *p)
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)
unsigned __CPROVER_POINTER_OBJECT(const void *p)
void __CPROVER_input(const char *id,...)
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
void __CPROVER_clear_must(const void *, const char *)
void __CPROVER_array_set(const void *dest,...)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p)