CBMC
cprover.h File Reference

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

+ 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_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.

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_size_t __CPROVER_max_malloc_size
extern

◆ __CPROVER_memory_leak

const void* __CPROVER_memory_leak
extern