builtin_libs.c File Reference

Functions
	__attribute__ ((annotate("__ESBMC_inf_size")))
__PTRDIFF_TYPE__	__CPROVER_POINTER_OFFSET (const void *p)
_Bool	__CPROVER_same_object (const void *p, const void *q)
__SIZE_TYPE__	__ESBMC_builtin_object_size (const void *, int)
static __SIZE_TYPE__	__esbmc_object_bytes (const void *p)
__SIZE_TYPE__	__CPROVER_OBJECT_SIZE (const void *p)
_Bool	__CPROVER_DYNAMIC_OBJECT (const void *p)
_Bool	__CPROVER_LIVE_OBJECT (const void *p)
_Bool	__CPROVER_WRITEABLE_OBJECT (const void *p)
_Bool	__CPROVER_r_ok (const void *p, __SIZE_TYPE__ size)
_Bool	__CPROVER_w_ok (const void *p, __SIZE_TYPE__ size)
_Bool	__CPROVER_rw_ok (const void *p, __SIZE_TYPE__ size)

Function Documentation

__attribute__()

__attribute__

(

(annotate("__ESBMC_inf_size"))

)

__CPROVER_DYNAMIC_OBJECT()

_Bool __CPROVER_DYNAMIC_OBJECT

(

const void *

p

)

__CPROVER_LIVE_OBJECT()

_Bool __CPROVER_LIVE_OBJECT

(

const void *

p

)

__CPROVER_OBJECT_SIZE()

__SIZE_TYPE__ __CPROVER_OBJECT_SIZE

(

const void *

p

)

__CPROVER_POINTER_OFFSET()

__PTRDIFF_TYPE__ __CPROVER_POINTER_OFFSET

(

const void *

p

)

__CPROVER_r_ok()

_Bool __CPROVER_r_ok	(	const void *	p,
		__SIZE_TYPE__	size )

__CPROVER_rw_ok()

_Bool __CPROVER_rw_ok	(	const void *	p,
		__SIZE_TYPE__	size )

__CPROVER_same_object()

_Bool __CPROVER_same_object	(	const void *	p,
		const void *	q )

__CPROVER_w_ok()

_Bool __CPROVER_w_ok	(	const void *	p,
		__SIZE_TYPE__	size )

__CPROVER_WRITEABLE_OBJECT()

_Bool __CPROVER_WRITEABLE_OBJECT

(

const void *

p

)

__ESBMC_builtin_object_size()

__SIZE_TYPE__ __ESBMC_builtin_object_size	(	const void *	,
		int	)

__esbmc_object_bytes()

__SIZE_TYPE__ __esbmc_object_bytes ( const void * p )

static