cprover.h File Reference

CPROVER built-in declarations to perform library checks. More...

#include "../cprover_builtin_headers.h"

Include dependency graph for cprover.h:

Go to the source code of this file.

Classes
struct	__CPROVER_pipet

Macros
#define	__CPROVER_constant_infinity_uint   1

Typedefs
typedef signed long long	__CPROVER_ssize_t

Functions
typedef	__typeof__ (sizeof(int)) __CPROVER_size_t
void *	__CPROVER_allocate (__CPROVER_size_t size, __CPROVER_bool zero)
void	__CPROVER_deallocate (void *)
__CPROVER_bool	__CPROVER_equal (unsigned long long, unsigned long long)
__CPROVER_bool	__CPROVER_overflow_minus (unsigned long long, unsigned long long)
__CPROVER_bool	__CPROVER_overflow_mult (unsigned long long, unsigned long long)
__CPROVER_bool	__CPROVER_overflow_plus (unsigned long long, unsigned long long)
__CPROVER_bool	__CPROVER_overflow_shl (unsigned long long, unsigned long long)
__CPROVER_bool	__CPROVER_overflow_unary_minus (unsigned long long)
__CPROVER_bool	__CPROVER_enum_is_in_range (unsigned long long)
__CPROVER_bool	__CPROVER_r_ok (const void *,...)
__CPROVER_bool	__CPROVER_w_ok (const void *,...)
__CPROVER_bool	__CPROVER_rw_ok (const void *,...)

Variables
const void *	__CPROVER_deallocated
const void *	__CPROVER_memory_leak
int	__CPROVER_malloc_failure_mode
__CPROVER_bool	__CPROVER_malloc_may_fail
__CPROVER_thread_local __CPROVER_size_t	__CPROVER_max_malloc_size
int	__CPROVER_malloc_failure_mode_return_null
int	__CPROVER_malloc_failure_mode_assert_then_assume

Detailed Description

CPROVER built-in declarations to perform library checks.

This file is only used by library_check.sh.

Definition in file cprover.h.

Macro Definition Documentation

__CPROVER_constant_infinity_uint

#define __CPROVER_constant_infinity_uint   1

Definition at line 21 of file cprover.h.

Typedef Documentation

__CPROVER_ssize_t

typedef signed long long __CPROVER_ssize_t

Definition at line 19 of file cprover.h.

Function Documentation

__CPROVER_allocate()

void * __CPROVER_allocate	(	__CPROVER_size_t	size,
		__CPROVER_bool	zero
	)

__CPROVER_deallocate()

void __CPROVER_deallocate

(

void *

ptr

)

Definition at line 670 of file stdlib.c.

__CPROVER_enum_is_in_range()

__CPROVER_bool __CPROVER_enum_is_in_range

(

unsigned long long

)

__CPROVER_equal()

__CPROVER_bool __CPROVER_equal	(	unsigned long long	,
		unsigned long long
	)

__CPROVER_overflow_minus()

__CPROVER_bool __CPROVER_overflow_minus	(	unsigned long long	,
		unsigned long long
	)

__CPROVER_overflow_mult()

__CPROVER_bool __CPROVER_overflow_mult	(	unsigned long long	,
		unsigned long long
	)

__CPROVER_overflow_plus()

__CPROVER_bool __CPROVER_overflow_plus	(	unsigned long long	,
		unsigned long long
	)

__CPROVER_overflow_shl()

__CPROVER_bool __CPROVER_overflow_shl	(	unsigned long long	,
		unsigned long long
	)

__CPROVER_overflow_unary_minus()

__CPROVER_bool __CPROVER_overflow_unary_minus

(

unsigned long long

)

__CPROVER_r_ok()

__CPROVER_bool __CPROVER_r_ok	(	const void *	,
			...
	)

__CPROVER_rw_ok()

__CPROVER_bool __CPROVER_rw_ok	(	const void *	,
			...
	)

__CPROVER_w_ok()

__CPROVER_bool __CPROVER_w_ok	(	const void *	,
			...
	)

__typeof__()

typedef __typeof__

(

sizeof(int)

)

Variable Documentation

__CPROVER_deallocated

const void* __CPROVER_deallocated

extern

__CPROVER_malloc_failure_mode

int __CPROVER_malloc_failure_mode

extern

__CPROVER_malloc_failure_mode_assert_then_assume

int __CPROVER_malloc_failure_mode_assert_then_assume

extern

__CPROVER_malloc_failure_mode_return_null

int __CPROVER_malloc_failure_mode_return_null

extern

__CPROVER_malloc_may_fail

__CPROVER_bool __CPROVER_malloc_may_fail

extern

__CPROVER_max_malloc_size

__CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size

extern

__CPROVER_memory_leak

const void* __CPROVER_memory_leak

extern