stdlib.c File Reference

#include <limits.h>
#include <inttypes.h>
#include <errno.h>
#include <stddef.h>

Include dependency graph for stdlib.c:

Go to the source code of this file.

Macros
#define	__CPROVER_LIMITS_H_INCLUDED
#define	__CPROVER_INTTYPES_H_INCLUDED
#define	__CPROVER_ERRNO_H_INCLUDED
#define	__CPROVER_STDDEF_H_INCLUDED

Functions
int	abs (int i)
long int	labs (long int i)
long long int	llabs (long long int i)
intmax_t	__CPROVER_imaxabs (intmax_t)
intmax_t	imaxabs (intmax_t i)
int	__builtin_abs (int i)
long int	__builtin_labs (long int i)
long long int	__builtin_llabs (long long int i)
void	exit (int status)
void	_Exit (int status)
void	abort (void)
__CPROVER_bool	__VERIFIER_nondet___CPROVER_bool (void)
_Bool	__builtin_mul_overflow ()
void *	calloc (__CPROVER_size_t nmemb, __CPROVER_size_t size)
void *	malloc (__CPROVER_size_t malloc_size)
void *	__builtin_alloca (__CPROVER_size_t alloca_size)
void *	alloca (__CPROVER_size_t alloca_size)
void	__CPROVER_deallocate (void *)
void	free (void *ptr)
int	isspace (int)
int	isdigit (int)
_Bool	__builtin_add_overflow ()
long	strtol (const char *nptr, char **endptr, int base)
int	atoi (const char *nptr)
long	atol (const char *nptr)
ptrdiff_t	__VERIFIER_nondet_ptrdiff_t (void)
char *	getenv (const char *name)
void *	realloc (void *ptr, __CPROVER_size_t malloc_size)
void *	valloc (__CPROVER_size_t malloc_size)
int	posix_memalign (void **ptr, __CPROVER_size_t alignment, __CPROVER_size_t size)
long	__VERIFIER_nondet_long (void)
long	random (void)
int	__VERIFIER_nondet_int (void)
int	rand (void)
int	rand_r (unsigned int *seed)

Variables
__CPROVER_bool	__CPROVER_malloc_is_new_array = 0
const void *	__CPROVER_alloca_object = 0
const void *	__CPROVER_new_object = 0

Macro Definition Documentation

__CPROVER_ERRNO_H_INCLUDED

#define __CPROVER_ERRNO_H_INCLUDED

Definition at line 358 of file stdlib.c.

__CPROVER_INTTYPES_H_INCLUDED

#define __CPROVER_INTTYPES_H_INCLUDED

Definition at line 58 of file stdlib.c.

__CPROVER_LIMITS_H_INCLUDED

#define __CPROVER_LIMITS_H_INCLUDED

Definition at line 5 of file stdlib.c.

__CPROVER_STDDEF_H_INCLUDED

#define __CPROVER_STDDEF_H_INCLUDED

Definition at line 490 of file stdlib.c.

Function Documentation

__builtin_abs()

int __builtin_abs

(

int

i

)

Definition at line 79 of file stdlib.c.

__builtin_add_overflow()

_Bool __builtin_add_overflow

(

)

__builtin_alloca()

void* __builtin_alloca

(

__CPROVER_size_t

alloca_size

)

Definition at line 270 of file stdlib.c.

__builtin_labs()

long int __builtin_labs

(

long int

i

)

Definition at line 86 of file stdlib.c.

__builtin_llabs()

long long int __builtin_llabs

(

long long int

i

)

Definition at line 93 of file stdlib.c.

__builtin_mul_overflow()

_Bool __builtin_mul_overflow

(

)

__CPROVER_deallocate()

void __CPROVER_deallocate

(

void *

ptr

)

Definition at line 670 of file stdlib.c.

__CPROVER_imaxabs()

intmax_t __CPROVER_imaxabs

(

intmax_t

)

__VERIFIER_nondet___CPROVER_bool()

__CPROVER_bool __VERIFIER_nondet___CPROVER_bool

(

void

)

__VERIFIER_nondet_int()

int __VERIFIER_nondet_int

(

void

)

__VERIFIER_nondet_long()

long __VERIFIER_nondet_long

(

void

)

__VERIFIER_nondet_ptrdiff_t()

ptrdiff_t __VERIFIER_nondet_ptrdiff_t

(

void

)

_Exit()

void _Exit

(

int

status

)

Definition at line 115 of file stdlib.c.

abort()

void abort

(

void

)

Definition at line 128 of file stdlib.c.

abs()

int abs

(

int

i

)

Definition at line 10 of file stdlib.c.

alloca()

void* alloca

(

__CPROVER_size_t

alloca_size

)

Definition at line 297 of file stdlib.c.

atoi()

int atoi

(

const char *

nptr

)

Definition at line 465 of file stdlib.c.

atol()

long atol

(

const char *

nptr

)

Definition at line 478 of file stdlib.c.

calloc()

void* calloc	(	__CPROVER_size_t	nmemb,
		__CPROVER_size_t	size
	)

Definition at line 146 of file stdlib.c.

exit()

void exit

(

int

status

)

Definition at line 102 of file stdlib.c.

free()

void free

(

void *

ptr

)

Definition at line 317 of file stdlib.c.

getenv()

char* getenv

(

const char *

name

)

Definition at line 496 of file stdlib.c.

imaxabs()

intmax_t imaxabs

(

intmax_t

i

)

Definition at line 70 of file stdlib.c.

isdigit()

int isdigit

(

int

c

)

Definition at line 24 of file ctype.c.

isspace()

int isspace

(

int

c

)

Definition at line 80 of file ctype.c.

labs()

long int labs

(

long int

i

)

Definition at line 27 of file stdlib.c.

llabs()

long long int llabs

(

long long int

i

)

Definition at line 45 of file stdlib.c.

malloc()

void * malloc ( __CPROVER_size_t  malloc_size )

inline

Definition at line 212 of file stdlib.c.

posix_memalign()

int posix_memalign	(	void **	ptr,
		__CPROVER_size_t	alignment,
		__CPROVER_size_t	size
	)

Definition at line 596 of file stdlib.c.

rand()

int rand

(

void

)

Definition at line 643 of file stdlib.c.

rand_r()

int rand_r

(

unsigned int *

seed

)

Definition at line 656 of file stdlib.c.

random()

long random

(

void

)

Definition at line 630 of file stdlib.c.

realloc()

void* realloc	(	void *	ptr,
		__CPROVER_size_t	malloc_size
	)

Definition at line 542 of file stdlib.c.

strtol()

long strtol	(	const char *	nptr,
		char **	endptr,
		int	base
	)

Definition at line 378 of file stdlib.c.

valloc()

void* valloc

(

__CPROVER_size_t

malloc_size

)

Definition at line 577 of file stdlib.c.

Variable Documentation

__CPROVER_alloca_object

const void* __CPROVER_alloca_object = 0

Definition at line 265 of file stdlib.c.

__CPROVER_malloc_is_new_array

__CPROVER_bool __CPROVER_malloc_is_new_array = 0

Definition at line 144 of file stdlib.c.

__CPROVER_new_object

const void* __CPROVER_new_object = 0

Definition at line 312 of file stdlib.c.