cprover_builtin_headers.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
void	__CPROVER_assume (__CPROVER_bool assumption)
void	__VERIFIER_assume (__CPROVER_bool assumption)
void	__CPROVER_assert (__CPROVER_bool assertion, const char *description)
void	__CPROVER_precondition (__CPROVER_bool precondition, const char *description)
void	__CPROVER_postcondition (__CPROVER_bool assertion, const char *description)
void	__CPROVER_havoc_object (void *)
void	__CPROVER_havoc_slice (void *, __CPROVER_size_t)
__CPROVER_bool	__CPROVER_same_object (const void *, const void *)
__CPROVER_bool	__CPROVER_is_invalid_pointer (const void *)
_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_is_list (const void *)
__CPROVER_bool	__CPROVER_is_dll (const void *)
__CPROVER_bool	__CPROVER_is_cyclic_dll (const void *)
__CPROVER_bool	__CPROVER_is_sentinel_dll (const void *,...)
__CPROVER_bool	__CPROVER_is_cstring (const char *)
__CPROVER_size_t	__CPROVER_cstrlen (const char *)
__CPROVER_bool	__CPROVER_separate (const void *, const void *,...)
__CPROVER_bool	__CPROVER_get_flag (const void *, const char *)
void	__CPROVER_set_must (const void *, const char *)
void	__CPROVER_clear_must (const void *, const char *)
void	__CPROVER_set_may (const void *, const char *)
void	__CPROVER_clear_may (const void *, const char *)
void	__CPROVER_cleanup (const void *, const void *)
__CPROVER_bool	__CPROVER_get_must (const void *, const char *)
__CPROVER_bool	__CPROVER_get_may (const void *, const char *)
void	__CPROVER_printf (const char *format,...)
void	__CPROVER_input (const char *id,...)
void	__CPROVER_output (const char *id,...)
void	__CPROVER_cover (__CPROVER_bool condition)
void	__CPROVER_atomic_begin (void)
void	__CPROVER_atomic_end (void)
void	__CPROVER_fence (const char *kind,...)
__CPROVER_bool	__CPROVER_is_freeable (const void *mem)
__CPROVER_bool	__CPROVER_was_freed (const void *mem)
__CPROVER_bool	__CPROVER_pointer_equals (void *p, void *q)
__CPROVER_bool	__CPROVER_is_fresh (const void *mem, __CPROVER_size_t size)
__CPROVER_bool	__CPROVER_obeys_contract (void(*)(void), void(*)(void))
__CPROVER_bool	__CPROVER_pointer_in_range_dfcc (void *lb, void *ptr, void *ub)
void	__CPROVER_old (const void *)
void	__CPROVER_loop_entry (const void *)
__CPROVER_bool	__CPROVER_LIVE_OBJECT (const void *)
__CPROVER_bool	__CPROVER_WRITEABLE_OBJECT (const void *)
__CPROVER_size_t	__CPROVER_POINTER_OBJECT (const void *)
__CPROVER_size_t	__CPROVER_POINTER_OFFSET (const void *)
__CPROVER_size_t	__CPROVER_OBJECT_SIZE (const void *)
__CPROVER_bool	__CPROVER_DYNAMIC_OBJECT (const void *)
__CPROVER_bool	__CPROVER_pointer_in_range (const void *, const void *, const void *)
void	__CPROVER_allocated_memory (__CPROVER_size_t address, __CPROVER_size_t extent)
int	__CPROVER_fpclassify (int, int, int, int, int,...)
__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_isgreaterf (float f, float g)
int	__CPROVER_isgreaterd (double f, double g)
int	__CPROVER_isgreaterequalf (float f, float g)
int	__CPROVER_isgreaterequald (double f, double g)
int	__CPROVER_islessf (float f, float g)
int	__CPROVER_islessd (double f, double g)
int	__CPROVER_islessequalf (float f, float g)
int	__CPROVER_islessequald (double f, double g)
int	__CPROVER_islessgreaterf (float f, float g)
int	__CPROVER_islessgreaterd (double f, double g)
int	__CPROVER_isunorderedf (float f, float g)
int	__CPROVER_isunorderedd (double f, double g)
float	__CPROVER_round_to_integralf (float, int)
double	__CPROVER_round_to_integrald (double, int)
long double	__CPROVER_round_to_integralld (long double, int)
int	__CPROVER_abs (int x)
long int	__CPROVER_labs (long int x)
long long int	__CPROVER_llabs (long long int x)
double	__CPROVER_fabs (double x)
long double	__CPROVER_fabsl (long double x)
float	__CPROVER_fabsf (float x)
double	__CPROVER_fmod (double, double)
float	__CPROVER_fmodf (float, float)
long double	__CPROVER_fmodl (long double, long double)
double	__CPROVER_remainder (double, double)
float	__CPROVER_remainderf (float, float)
long double	__CPROVER_remainderl (long double, long double)
__CPROVER_bool	__CPROVER_array_equal (const void *array1, const void *array2)
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_k_induction_hint (unsigned min, unsigned max, unsigned step, unsigned loop_free)
int	__CPROVER_scanf (const char *,...)
void	__CPROVER_assignable (void *ptr, __CPROVER_size_t size, __CPROVER_bool is_ptr_to_ptr)
void	__CPROVER_object_whole (void *ptr)
void	__CPROVER_object_from (void *ptr)
void	__CPROVER_object_upto (void *ptr, __CPROVER_size_t size)
void	__CPROVER_freeable (void *ptr)

Function Documentation

__CPROVER_abs()

int __CPROVER_abs

(

int

x

)

__CPROVER_allocated_memory()

void __CPROVER_allocated_memory	(	__CPROVER_size_t	address,
		__CPROVER_size_t	extent
	)

__CPROVER_array_copy()

void __CPROVER_array_copy	(	const void *	dest,
		const void *	src
	)

__CPROVER_array_equal()

__CPROVER_bool __CPROVER_array_equal	(	const void *	array1,
		const void *	array2
	)

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

void __CPROVER_assignable	(	void *	ptr,
		__CPROVER_size_t	size,
		__CPROVER_bool	is_ptr_to_ptr
	)

__CPROVER_assume()

void __CPROVER_assume

(

__CPROVER_bool

assumption

)

__CPROVER_atomic_begin()

void __CPROVER_atomic_begin

(

void

)

__CPROVER_atomic_end()

void __CPROVER_atomic_end

(

void

)

__CPROVER_buffer_size()

__CPROVER_size_t __CPROVER_buffer_size

(

const void *

)

__CPROVER_cleanup()

void __CPROVER_cleanup	(	const void *	,
		const void *
	)

__CPROVER_clear_may()

void __CPROVER_clear_may	(	const void *	,
		const char *
	)

__CPROVER_clear_must()

void __CPROVER_clear_must	(	const void *	,
		const char *
	)

__CPROVER_cover()

void __CPROVER_cover

(

__CPROVER_bool

condition

)

__CPROVER_cstrlen()

__CPROVER_size_t __CPROVER_cstrlen

(

const char *

)

__CPROVER_DYNAMIC_OBJECT()

__CPROVER_bool __CPROVER_DYNAMIC_OBJECT

(

const void *

)

__CPROVER_fabs()

double __CPROVER_fabs

(

double

x

)

__CPROVER_fabsf()

float __CPROVER_fabsf

(

float

x

)

__CPROVER_fabsl()

long double __CPROVER_fabsl

(

long double

x

)

__CPROVER_fence()

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

__CPROVER_fmod()

double __CPROVER_fmod	(	double	,
		double
	)

__CPROVER_fmodf()

float __CPROVER_fmodf	(	float	,
		float
	)

__CPROVER_fmodl()

long double __CPROVER_fmodl	(	long double	,
		long double
	)

__CPROVER_fpclassify()

int __CPROVER_fpclassify	(	int	,
		int	,
		int	,
		int	,
		int	,
			...
	)

__CPROVER_freeable()

void __CPROVER_freeable

(

void *

ptr

)

__CPROVER_get_flag()

__CPROVER_bool __CPROVER_get_flag	(	const void *	,
		const char *
	)

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

void __CPROVER_havoc_object

(

void *

)

__CPROVER_havoc_slice()

void __CPROVER_havoc_slice	(	void *	,
		__CPROVER_size_t
	)

__CPROVER_inf()

double __CPROVER_inf

(

void

)

__CPROVER_inff()

float __CPROVER_inff

(

void

)

__CPROVER_infl()

long double __CPROVER_infl

(

void

)

__CPROVER_input()

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

__CPROVER_is_cstring()

__CPROVER_bool __CPROVER_is_cstring

(

const char *

)

__CPROVER_is_cyclic_dll()

__CPROVER_bool __CPROVER_is_cyclic_dll

(

const void *

)

__CPROVER_is_dll()

__CPROVER_bool __CPROVER_is_dll

(

const void *

)

__CPROVER_is_freeable()

__CPROVER_bool __CPROVER_is_freeable

(

const void *

mem

)

__CPROVER_is_fresh()

__CPROVER_bool __CPROVER_is_fresh	(	const void *	mem,
		__CPROVER_size_t	size
	)

__CPROVER_is_invalid_pointer()

__CPROVER_bool __CPROVER_is_invalid_pointer

(

const void *

)

__CPROVER_is_list()

__CPROVER_bool __CPROVER_is_list

(

const void *

)

__CPROVER_is_sentinel_dll()

__CPROVER_bool __CPROVER_is_sentinel_dll	(	const void *	,
			...
	)

__CPROVER_is_zero_string()

_Bool __CPROVER_is_zero_string

(

const void *

)

__CPROVER_isfinited()

__CPROVER_bool __CPROVER_isfinited

(

double

f

)

__CPROVER_isfinitef()

__CPROVER_bool __CPROVER_isfinitef

(

float

f

)

__CPROVER_isfiniteld()

__CPROVER_bool __CPROVER_isfiniteld

(

long double

f

)

__CPROVER_isgreaterd()

int __CPROVER_isgreaterd	(	double	f,
		double	g
	)

Definition at line 49 of file math.c.

__CPROVER_isgreaterequald()

int __CPROVER_isgreaterequald	(	double	f,
		double	g
	)

Definition at line 57 of file math.c.

__CPROVER_isgreaterequalf()

int __CPROVER_isgreaterequalf	(	float	f,
		float	g
	)

Definition at line 53 of file math.c.

__CPROVER_isgreaterf()

int __CPROVER_isgreaterf	(	float	f,
		float	g
	)

Definition at line 45 of file math.c.

__CPROVER_isinfd()

__CPROVER_bool __CPROVER_isinfd

(

double

f

)

__CPROVER_isinff()

__CPROVER_bool __CPROVER_isinff

(

float

f

)

__CPROVER_isinfld()

__CPROVER_bool __CPROVER_isinfld

(

long double

f

)

__CPROVER_islessd()

int __CPROVER_islessd	(	double	f,
		double	g
	)

Definition at line 65 of file math.c.

__CPROVER_islessequald()

int __CPROVER_islessequald	(	double	f,
		double	g
	)

Definition at line 73 of file math.c.

__CPROVER_islessequalf()

int __CPROVER_islessequalf	(	float	f,
		float	g
	)

Definition at line 69 of file math.c.

__CPROVER_islessf()

int __CPROVER_islessf	(	float	f,
		float	g
	)

Definition at line 61 of file math.c.

__CPROVER_islessgreaterd()

int __CPROVER_islessgreaterd	(	double	f,
		double	g
	)

Definition at line 81 of file math.c.

__CPROVER_islessgreaterf()

int __CPROVER_islessgreaterf	(	float	f,
		float	g
	)

Definition at line 77 of file math.c.

__CPROVER_isnand()

__CPROVER_bool __CPROVER_isnand

(

double

f

)

__CPROVER_isnanf()

__CPROVER_bool __CPROVER_isnanf

(

float

f

)

__CPROVER_isnanld()

__CPROVER_bool __CPROVER_isnanld

(

long double

f

)

__CPROVER_isnormald()

__CPROVER_bool __CPROVER_isnormald

(

double

f

)

__CPROVER_isnormalf()

__CPROVER_bool __CPROVER_isnormalf

(

float

f

)

__CPROVER_isnormalld()

__CPROVER_bool __CPROVER_isnormalld

(

long double

f

)

__CPROVER_isunorderedd()

int __CPROVER_isunorderedd	(	double	f,
		double	g
	)

Definition at line 92 of file math.c.

__CPROVER_isunorderedf()

int __CPROVER_isunorderedf	(	float	f,
		float	g
	)

Definition at line 85 of file math.c.

__CPROVER_k_induction_hint()

void __CPROVER_k_induction_hint	(	unsigned	min,
		unsigned	max,
		unsigned	step,
		unsigned	loop_free
	)

__CPROVER_labs()

long int __CPROVER_labs

(

long int

x

)

__CPROVER_LIVE_OBJECT()

__CPROVER_bool __CPROVER_LIVE_OBJECT

(

const void *

)

__CPROVER_llabs()

long long int __CPROVER_llabs

(

long long int

x

)

__CPROVER_loop_entry()

void __CPROVER_loop_entry

(

const void *

)

__CPROVER_obeys_contract()

__CPROVER_bool __CPROVER_obeys_contract	(	void(*)(void)	,
		void(*)(void)
	)

__CPROVER_object_from()

void __CPROVER_object_from

(

void *

ptr

)

__CPROVER_OBJECT_SIZE()

__CPROVER_size_t __CPROVER_OBJECT_SIZE

(

const void *

)

__CPROVER_object_upto()

void __CPROVER_object_upto	(	void *	ptr,
		__CPROVER_size_t	size
	)

__CPROVER_object_whole()

void __CPROVER_object_whole

(

void *

ptr

)

__CPROVER_old()

void __CPROVER_old

(

const void *

)

__CPROVER_output()

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

__CPROVER_pointer_equals()

__CPROVER_bool __CPROVER_pointer_equals	(	void *	p,
		void *	q
	)

__CPROVER_pointer_in_range()

__CPROVER_bool __CPROVER_pointer_in_range	(	const void *	,
		const void *	,
		const void *
	)

__CPROVER_pointer_in_range_dfcc()

__CPROVER_bool __CPROVER_pointer_in_range_dfcc	(	void *	lb,
		void *	ptr,
		void *	ub
	)

__CPROVER_POINTER_OBJECT()

__CPROVER_size_t __CPROVER_POINTER_OBJECT

(

const void *

)

__CPROVER_POINTER_OFFSET()

__CPROVER_size_t __CPROVER_POINTER_OFFSET

(

const void *

)

__CPROVER_postcondition()

void __CPROVER_postcondition	(	__CPROVER_bool	assertion,
		const char *	description
	)

__CPROVER_precondition()

void __CPROVER_precondition	(	__CPROVER_bool	precondition,
		const char *	description
	)

__CPROVER_printf()

void __CPROVER_printf	(	const char *	format,
			...
	)

__CPROVER_remainder()

double __CPROVER_remainder	(	double	,
		double
	)

__CPROVER_remainderf()

float __CPROVER_remainderf	(	float	,
		float
	)

__CPROVER_remainderl()

long double __CPROVER_remainderl	(	long double	,
		long double
	)

__CPROVER_round_to_integrald()

double __CPROVER_round_to_integrald	(	double	,
		int
	)

__CPROVER_round_to_integralf()

float __CPROVER_round_to_integralf	(	float	,
		int
	)

__CPROVER_round_to_integralld()

long double __CPROVER_round_to_integralld	(	long double	,
		int
	)

__CPROVER_same_object()

__CPROVER_bool __CPROVER_same_object	(	const void *	,
		const void *
	)

__CPROVER_scanf()

int __CPROVER_scanf	(	const char *	,
			...
	)

__CPROVER_separate()

__CPROVER_bool __CPROVER_separate	(	const void *	,
		const void *	,
			...
	)

__CPROVER_set_may()

void __CPROVER_set_may	(	const void *	,
		const char *
	)

__CPROVER_set_must()

void __CPROVER_set_must	(	const void *	,
		const char *
	)

__CPROVER_signd()

__CPROVER_bool __CPROVER_signd

(

double

f

)

__CPROVER_signf()

__CPROVER_bool __CPROVER_signf

(

float

f

)

__CPROVER_signld()

__CPROVER_bool __CPROVER_signld

(

long double

f

)

__CPROVER_was_freed()

__CPROVER_bool __CPROVER_was_freed

(

const void *

mem

)

__CPROVER_WRITEABLE_OBJECT()

__CPROVER_bool __CPROVER_WRITEABLE_OBJECT

(

const void *

)

__CPROVER_zero_string_length()

__CPROVER_size_t __CPROVER_zero_string_length

(

const void *

)

__VERIFIER_assume()

void __VERIFIER_assume

(

__CPROVER_bool

assumption

)