cprover.h File Reference

Go to the source code of this file.

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)
void	__CPROVER_input (const char *description,...)
void	__CPROVER_output (const char *description,...)
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)
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 *)

Variables
const void *	__CPROVER_deallocated
const void *	__CPROVER_new_object
_Bool	__CPROVER_malloc_is_new_array
const void *	__CPROVER_memory_leak

Function Documentation

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

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

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

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

__CPROVER_output()

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

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

void __CPROVER_set_may	(	const void *	,
		const char *
	)

__CPROVER_set_must()

void __CPROVER_set_must	(	const void *	,
		const char *
	)

__typeof__()

typedef __typeof__

(

sizeof(int)

)

Variable Documentation

__CPROVER_deallocated

const void* __CPROVER_deallocated

__CPROVER_malloc_is_new_array

_Bool __CPROVER_malloc_is_new_array

__CPROVER_memory_leak

const void* __CPROVER_memory_leak

__CPROVER_new_object

const void* __CPROVER_new_object