cprover.h File Reference

#include "../cprover_builtin_headers.h"

Include dependency graph for cprover.h:

Go to the source code of this file.

Classes
struct	__CPROVER_pipet

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 *)

Variables
const void *	__CPROVER_deallocated
const void *	__CPROVER_new_object
__CPROVER_bool	__CPROVER_malloc_is_new_array
const void *	__CPROVER_memory_leak
int	__CPROVER_malloc_failure_mode
__CPROVER_size_t	__CPROVER_max_malloc_size
__CPROVER_bool	__CPROVER_malloc_may_fail
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.

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 *

)

__typeof__()

typedef __typeof__

(

sizeof(int)

)

Variable Documentation

__CPROVER_deallocated

const void* __CPROVER_deallocated

__CPROVER_malloc_failure_mode

int __CPROVER_malloc_failure_mode

__CPROVER_malloc_failure_mode_assert_then_assume

int __CPROVER_malloc_failure_mode_assert_then_assume

__CPROVER_malloc_failure_mode_return_null

int __CPROVER_malloc_failure_mode_return_null

__CPROVER_malloc_is_new_array

__CPROVER_bool __CPROVER_malloc_is_new_array

__CPROVER_malloc_may_fail

__CPROVER_bool __CPROVER_malloc_may_fail

__CPROVER_max_malloc_size

__CPROVER_size_t __CPROVER_max_malloc_size

__CPROVER_memory_leak

const void* __CPROVER_memory_leak

__CPROVER_new_object

const void* __CPROVER_new_object